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 6f1483b7decbcebb809c6469489b2815a0965516..75efafed43870f8be079fc8fcb1cb49bd8412706 100644 (file)
--- 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 a4f7e90fc332b39c8be422a8eef450f3d4368aca..44c7e353d79b5f8cd87de1f50763c1b705b6224e 100644 (file)
--- 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 723ca43fe3a4f76a667d3ca921f07ea76fdf6f5b..dbf0654fc21b22aec59cb1c1d42ec6fef094a451 100644 (file)
--- 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;