revamp scheduler so we can start threads early

diff --git a/cmodelint.cc b/cmodelint.cc
index 9ea1b681c32d20c7adb9f62aff78f9aab21d480d..b1a8eb43d3258add2ff3d8af5f821ab566669105 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -14,29 +14,13 @@ memory_order orders[6] = {
        memory_order_release, memory_order_acq_rel, memory_order_seq_cst
 };
 
-#define ensureModel(action) \
-       if (!modelchecker_started) {                  \
-               if (!model) { \
-                       snapshot_system_init(10000, 1024, 1024, 40000); \
-                       model = new ModelChecker(); \
-               } \
-               model->get_execution()->check_current_action(action); \
-       }else { \
-               model->switch_to_master(action); \
-       }
-
-
-#define ensureModelValue(action, type)          \
-       if (!modelchecker_started) { \
-               if (!model) { \
-                       snapshot_system_init(10000, 1024, 1024, 40000); \
-                       model = new ModelChecker(); \
-               } \
-               model->get_execution()->check_current_action(action); \
-               return (type) thread_current()->get_return_value();   \
-       } else { \
-               return (type) model->switch_to_master(action);        \
+static void ensureModel() {
+       if (!model) {
+               snapshot_system_init(10000, 1024, 1024, 40000);
+               model = new ModelChecker();
+               model->startChecker();
        }
+}
 
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
@@ -89,85 +73,83 @@ void model_fence_action(memory_order ord) {
 
 /* ---  helper functions --- */
 uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
-       ensureModelValue(
-               new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t
-               );
+       ensureModel();
+       return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size));
 }
 
 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
-       ensureModelValue(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj), uint64_t);
+       ensureModel();
+       return model->switch_to_master(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj));
 }
 
 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
-       ensureModel(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
 }
 
 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
-       ensureModel(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
 }
 
 // cds atomic inits
 void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val));
 }
 void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val));
 }
 void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val));
 }
 void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val));
 }
 
 
 // cds atomic loads
 uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
-       ensureModelValue(
-               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t);
+       ensureModel();
+       return (uint8_t) model->switch_to_master(
+               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj));
 }
 uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
-       ensureModelValue(
-               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t);
+       ensureModel();
+       return (uint16_t) model->switch_to_master(
+               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj));
 }
 uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
-       ensureModelValue(
-               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t
+       ensureModel();
+       return (uint32_t) model->switch_to_master(
+               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)
                );
 }
 uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
-       ensureModelValue(
-               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t);
+       ensureModel();
+       return model->switch_to_master(
+               new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj));
 }
 
 // cds atomic stores
 void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val));
 }
 void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val));
 }
 void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val));
 }
 void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
-       ensureModel(
-               new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
-               );
+       ensureModel();
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val));
 }
 
 #define _ATOMIC_RMW_(__op__, size, addr, val, atomic_index, position)            \

diff --git a/execution.cc b/execution.cc
index 2e7442515b4cf47556817f727ba3bd8a7e65b466..2c08711eee0d1a655272bd56f1adf0d900ef599d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
        thrd_last_fence_release(),
        node_stack(node_stack),
        priv(new struct model_snapshot_members ()),
-       mo_graph(new CycleGraph()),
+                        mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */

diff --git a/main.cc b/main.cc
index df6fff6856ad484013f6386950a869b4727e8607..a484f497458ee078270aa2cd52ccc2a20c551c1a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -161,16 +161,6 @@ static void install_trace_analyses(ModelExecution *execution)
        }
 }
 
-/** The model_main function contains the main model checking loop. */
-static void model_main()
-{
-       snapshot_record(0);
-       model->run();
-       delete model;
-
-       DEBUG("Exiting\n");
-}
-
 /**
  * Main function.  Just initializes snapshotting library and the
  * snapshotting library calls the model_main function.
@@ -199,6 +189,7 @@ int main(int argc, char **argv)
        if (!model) {
                snapshot_system_init(10000, 1024, 1024, 40000);
                model = new ModelChecker();
+               model->startChecker();
        }
 
        register_plugins();
@@ -213,7 +204,7 @@ int main(int argc, char **argv)
        snapshot_stack_init();
        install_trace_analyses(model->get_execution());
 
-       //Start everything up
-       modelchecker_started = true;
-       startExecution(&model_main);
+       snapshot_record(0);
+       model->startMainThread();
+       DEBUG("Exiting\n");
 }

diff --git a/model.cc b/model.cc
index 0a7913bfd5571163364f8de9b30055e03b9df0b5..7f38adc37e149403828d993676e366fb70bc653d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -21,7 +21,6 @@
 #include "params.h"
 
 ModelChecker *model = NULL;
-bool modelchecker_started = false;
 
 /** Wrapper to run the user's main function, with appropriate arguments */
 void user_main_wrapper(void *)
@@ -163,7 +162,7 @@ void ModelChecker::print_bugs() const
                                                        bugs->size(),
                                                        bugs->size() > 1 ? "s" : "");
        for (unsigned int i = 0;i < bugs->size();i++)
-               (*bugs)[i] -> print();
+               (*bugs)[i]->print();
 }
 
 /**
@@ -174,15 +173,15 @@ void ModelChecker::print_bugs() const
  */
 void ModelChecker::record_stats()
 {
-       stats.num_total ++;
+       stats.num_total++;
        if (!execution->isfeasibleprefix())
-               stats.num_infeasible ++;
+               stats.num_infeasible++;
        else if (execution->have_bug_reports())
-               stats.num_buggy_executions ++;
+               stats.num_buggy_executions++;
        else if (execution->is_complete_execution())
-               stats.num_complete ++;
+               stats.num_complete++;
        else {
-               stats.num_redundant ++;
+               stats.num_redundant++;
 
                /**
                 * @todo We can violate this ASSERT() when fairness/sleep sets
@@ -263,15 +262,15 @@ bool ModelChecker::next_execution()
                return true;
        }
 // test code
-       execution_number ++;
+       execution_number++;
        reset_to_initial_state();
        return false;
 }
 
 /** @brief Run trace analyses on complete trace */
 void ModelChecker::run_trace_analyses() {
-       for (unsigned int i = 0;i < trace_analyses.size();i ++)
-               trace_analyses[i] -> analyze(execution->get_action_trace());
+       for (unsigned int i = 0;i < trace_analyses.size();i++)
+               trace_analyses[i]->analyze(execution->get_action_trace());
 }
 
 /**
@@ -337,6 +336,15 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        return old->get_return_value();
 }
 
+static void runChecker() {
+       model->run();
+       delete model;
+}
+
+void ModelChecker::startChecker() {
+       startExecution(get_system_context(), runChecker);
+}
+
 bool ModelChecker::should_terminate_execution()
 {
        /* Infeasible -> don't take any more steps */
@@ -364,6 +372,10 @@ void ModelChecker::do_restart()
        execution_number = 1;
 }
 
+void ModelChecker::startMainThread() {
+       init_thread->setContext();
+}
+
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
@@ -371,7 +383,7 @@ void ModelChecker::run()
        char random_state[256];
        initstate(423121, random_state, sizeof(random_state));
 
-       for(int exec = 0;exec < params.maxexecutions;exec ++) {
+       for(int exec = 0;exec < params.maxexecutions;exec++) {
                Thread * t = init_thread;
 
                do {

diff --git a/model.h b/model.h
index 8983d017f80fa1c5a17d53bd03edb49cedea102b..1269e76e1edf00d47951bc3c60001fee8658fe33 100644 (file)
--- a/model.h
+++ b/model.h
@@ -64,7 +64,8 @@ public:
        model_params params;
        void add_trace_analysis(TraceAnalysis *a) {     trace_analyses.push_back(a); }
        void set_inspect_plugin(TraceAnalysis *a) {     inspect_plugin=a;       }
-
+       void startMainThread();
+       void startChecker();
        MEMALLOC
 private:
        /** Flag indicates whether to restart the model checker. */
@@ -107,5 +108,4 @@ private:
 };
 
 extern ModelChecker *model;
-extern bool modelchecker_started;
 #endif /* __MODEL_H__ */

diff --git a/pthread.cc b/pthread.cc
index 808aa207cd72338806932b3afd86c2d5abe367c6..9a222b9d85a24bccb70d04a92d549bebf5f9a33c 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -53,6 +53,7 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        if (!model) {
                snapshot_system_init(10000, 1024, 1024, 40000);
                model = new ModelChecker();
+               model->startChecker();
        }
 
        ModelExecution *execution = model->get_execution();

diff --git a/snapshot-interface.h b/snapshot-interface.h
index 3e3ad71e02388ff1130d3da357f8321c77543a01..4d27ae04cecfcd679b8d81d64061579391a25075 100644 (file)
--- a/snapshot-interface.h
+++ b/snapshot-interface.h
@@ -5,14 +5,15 @@
 
 #ifndef __SNAPINTERFACE_H
 #define __SNAPINTERFACE_H
+#include <ucontext.h>
 
 typedef unsigned int snapshot_id;
-
 typedef void (*VoidFuncPtr)();
+
 void snapshot_system_init(unsigned int numbackingpages,
                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
                                                                                                        unsigned int numheappages);
-void startExecution(VoidFuncPtr entryPoint);
+void startExecution(ucontext_t * context, VoidFuncPtr entryPoint);
 void snapshot_stack_init();
 void snapshot_record(int seq_index);
 int snapshot_backtrack_before(int seq_index);

diff --git a/snapshot.cc b/snapshot.cc
index 5c1c1e25fd0599922da93a9100c9eb41f16385f7..2901be3c385db322689a3b8793c340c613921920 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -181,9 +181,9 @@ static void mprot_snapshot_init(unsigned int numbackingpages,
        snapshot_add_memory_region(pagealignedbase, numheappages);
 }
 
-
-static void mprot_startExecution(VoidFuncPtr entryPoint) {
-       entryPoint();
+static void mprot_startExecution(ucontext_t * context, VoidFuncPtr entryPoint) {
+       /* setup the shared-stack context */
+       create_context(context, fork_snap->mStackBase, model_calloc(STACK_SIZE_DEFAULT, 1), STACK_SIZE_DEFAULT, entryPoint);
 }
 
 static void mprot_add_to_snapshot(void *addr, unsigned int numPages)
@@ -323,6 +323,7 @@ static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize,
        getcontext(ctxt);
        ctxt->uc_stack.ss_sp = stack;
        ctxt->uc_stack.ss_size = stacksize;
+       ctxt->uc_link = NULL;
        makecontext(ctxt, func, 0);
 }
 
@@ -330,7 +331,7 @@ static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize,
  *  process */
 static void fork_exit()
 {
-       /* Intentionally empty */
+       _Exit(EXIT_SUCCESS);
 }
 
 static void createSharedMemory()
@@ -376,17 +377,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
        model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1);
 }
 
-static void fork_startExecution(VoidFuncPtr entryPoint) {
-       /* setup an "exiting" context */
-       char stack[128];
-       create_context(&exit_ctxt, stack, sizeof(stack), fork_exit);
-
-       /* setup the shared-stack context */
-       create_context(&fork_snap->shared_ctxt, fork_snap->mStackBase,
-                                                                STACK_SIZE_DEFAULT, entryPoint);
-       /* switch to a new entryPoint context, on a new stack */
-       model_swapcontext(&private_ctxt, &fork_snap->shared_ctxt);
-
+static void fork_loop() {
        /* switch back here when takesnapshot is called */
        snapshotid = fork_snap->currSnapShotID;
        if (model->params.nofork) {
@@ -419,8 +410,18 @@ static void fork_startExecution(VoidFuncPtr entryPoint) {
        }
 }
 
-static snapshot_id fork_take_snapshot()
-{
+static void fork_startExecution(ucontext_t *context, VoidFuncPtr entryPoint) {
+       /* setup an "exiting" context */
+       char stack[128];
+       create_context(&exit_ctxt, stack, sizeof(stack), fork_exit);
+
+       /* setup the system context */
+       create_context(context, fork_snap->mStackBase, STACK_SIZE_DEFAULT, entryPoint);
+       /* switch to a new entryPoint context, on a new stack */
+       create_context(&private_ctxt, snapshot_calloc(STACK_SIZE_DEFAULT, 1), STACK_SIZE_DEFAULT, fork_loop);
+}
+
+static snapshot_id fork_take_snapshot() {
        model_swapcontext(&fork_snap->shared_ctxt, &private_ctxt);
        DEBUG("TAKESNAPSHOT RETURN\n");
        return snapshotid;
@@ -451,12 +452,12 @@ void snapshot_system_init(unsigned int numbackingpages,
 #endif
 }
 
-void startExecution(VoidFuncPtr entryPoint)
+void startExecution(ucontext_t *context, VoidFuncPtr entryPoint)
 {
 #if USE_MPROTECT_SNAPSHOT
-       mprot_startExecution(entryPoint);
+       mprot_startExecution(context, entryPoint);
 #else
-       fork_startExecution(entryPoint);
+       fork_startExecution(context, entryPoint);
 #endif
 }
 

diff --git a/threads-model.h b/threads-model.h
index 61e3569bbdfe8a9f09efb8e354eacc119257d8ab..513142b53c41734832c1110f3d5dff4ae5baf1f0 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -50,6 +50,7 @@ public:
        static int swap(ucontext_t *ctxt, Thread *t);
        static int swap(Thread *t, ucontext_t *ctxt);
 
+       void setContext();
        thread_state get_state() const { return state; }
        void set_state(thread_state s);
        thread_id_t get_id() const;

diff --git a/threads.cc b/threads.cc
index 67f681ca7052538afb794ff87bb9708ff3655daa..56942f5f7d277ac12c00dc17ba4bc9ff3e31aa75 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -86,6 +86,11 @@ int Thread::create_context()
        return 0;
 }
 
+void Thread::setContext() {
+       set_state(THREAD_RUNNING);
+       setcontext(&context);
+}
+
 /**
  * Swaps the current context to another thread of execution. This form switches
  * from a user Thread to a system context.