From: Brian Norris <banorris@uci.edu>
Date: Fri, 10 Aug 2012 22:15:24 +0000 (-0700)
Subject: main, model: don't 'initialize' system_context
X-Git-Tag: pldi2013~271^2~3
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=c36dd97a0b4924e1c906f7931d7ed515d5d7dc61

main, model: don't 'initialize' system_context

I was unnecessarily giving main.cc control of the system_context variable,
since I thought I needed to use getcontext() before entering the model checker.
However, the structure of the runtime scheduling is such that this
"initialization" would be obliterated by the first swapcontext() call
(switching form system-context to user-context).

So, the point is that the model-checker can just declare its own
("uninitialized") context that will be initialized as soon as the model-checker
makes a thread swap. Thus, I remove the external interface for initializing the
context (set_system_context()).
---

diff --git a/main.cc b/main.cc
index 6f1483b..75efafe 100644
--- a/main.cc
+++ b/main.cc
@@ -21,7 +21,6 @@ char **main_argv;
 /** The real_main function contains the main model checking loop. */
 static void real_main() {
 	thrd_t user_thread;
-	ucontext_t main_context;
 	struct model_params params;
 
 	parse_options(&params, main_argc, main_argv);
@@ -34,11 +33,6 @@ static void real_main() {
 
 	model = new ModelChecker(params);
 
-	if (getcontext(&main_context))
-		return;
-
-	model->set_system_context(&main_context);
-
 	snapshotObject->snapshotStep(0);
 	do {
 		/* Start user program */
diff --git a/model.cc b/model.cc
index a4f7e90..44c7e35 100644
--- a/model.cc
+++ b/model.cc
@@ -749,7 +749,7 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	Thread * old = thread_current();
 	set_current_action(act);
 	old->set_state(THREAD_READY);
-	return Thread::swap(old, get_system_context());
+	return Thread::swap(old, &system_context);
 }
 
 /**
@@ -785,7 +785,7 @@ bool ModelChecker::take_step() {
 	if (!next)
 		return false;
 	/* Return false only if swap fails with an error */
-	return (Thread::swap(get_system_context(), next) == 0);
+	return (Thread::swap(&system_context, next) == 0);
 }
 
 /** Runs the current execution until threre are no more steps to take. */
diff --git a/model.h b/model.h
index 723ca43..dbf0654 100644
--- a/model.h
+++ b/model.h
@@ -36,14 +36,8 @@ public:
 	ModelChecker(struct model_params params);
 	~ModelChecker();
 
-	/** Stores the context for the main model-checking system thread (call
-	 * once)
-	 * @param ctxt The system context structure
-	 */
-	void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
-
 	/** @returns the context for the main model-checking system thread */
-	ucontext_t * get_system_context(void) { return system_context; }
+	ucontext_t * get_system_context() { return &system_context; }
 
 	void check_current_action(void);
 
@@ -115,7 +109,7 @@ private:
 	ModelAction *diverge;
 	thread_id_t nextThread;
 
-	ucontext_t *system_context;
+	ucontext_t system_context;
 	action_list_t *action_trace;
 	HashTable<int, Thread *, int> *thread_map;