From c36dd97a0b4924e1c906f7931d7ed515d5d7dc61 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 10 Aug 2012 15:15:24 -0700 Subject: [PATCH] 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()). --- main.cc | 6 ------ model.cc | 4 ++-- model.h | 10 ++-------- 3 files changed, 4 insertions(+), 16 deletions(-) diff --git a/main.cc b/main.cc index 6f1483b7..75efafed 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(¶ms, 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 a4f7e90f..44c7e353 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 723ca43f..dbf0654f 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 *thread_map; -- 2.34.1