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()).
/** The real_main function contains the main model checking loop. */
static void real_main() {
thrd_t user_thread;
/** 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(¶ms, main_argc, main_argv);
struct model_params params;
parse_options(¶ms, main_argc, main_argv);
model = new ModelChecker(params);
model = new ModelChecker(params);
- if (getcontext(&main_context))
- return;
-
- model->set_system_context(&main_context);
-
snapshotObject->snapshotStep(0);
do {
/* Start user program */
snapshotObject->snapshotStep(0);
do {
/* Start user program */
Thread * old = thread_current();
set_current_action(act);
old->set_state(THREAD_READY);
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);
if (!next)
return false;
/* Return false only if swap fails with an error */
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. */
}
/** Runs the current execution until threre are no more steps to take. */
ModelChecker(struct model_params params);
~ModelChecker();
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 */
/** @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);
void check_current_action(void);
ModelAction *diverge;
thread_id_t nextThread;
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;
action_list_t *action_trace;
HashTable<int, Thread *, int> *thread_map;