Eliminate system context
authorBrian Demsky <bdemsky@uci.edu>
Sat, 29 Aug 2020 07:33:30 +0000 (00:33 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Sat, 29 Aug 2020 07:33:30 +0000 (00:33 -0700)
19 files changed:
actionlist.cc
cmodelint.cc
funcinst.cc
funcnode.cc
history.cc
impatomic.cc
include/mypthread.h
libannotate.cc
libthreads.cc
model.cc
model.h
newfuzzer.cc
predicate.cc
pthread.cc
sleeps.cc
snapshot-interface.h
snapshot.cc
threads-model.h
threads.cc

index 4a24ba9..f97e667 100644 (file)
@@ -253,7 +253,7 @@ bool actionlist::isEmpty() {
  */
 void actionlist::fixupParent()
 {
-       for (int i = 0; i < ALLNODESIZE; i++) {
+       for (int i = 0;i < ALLNODESIZE;i++) {
                allnode * child = root.children[i];
                if (child != NULL && child->parent != &root)
                        child->parent = &root;
index a80e386..b7ff591 100644 (file)
@@ -25,17 +25,17 @@ static void ensureModel() {
 
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
-       return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
+       return model->switch_thread(new ModelAction(ATOMIC_READ, ord, obj));
 }
 
 /** Performs a write action.*/
 void model_write_action(void * obj, memory_order ord, uint64_t val) {
-       model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
+       model->switch_thread(new ModelAction(ATOMIC_WRITE, ord, obj, val));
 }
 
 /** Performs an init action. */
 void model_init_action(void * obj, uint64_t val) {
-       model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
+       model->switch_thread(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
 }
 
 /**
@@ -44,7 +44,7 @@ void model_init_action(void * obj, uint64_t val) {
  * a write.
  */
 uint64_t model_rmwr_action(void *obj, memory_order ord) {
-       return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
+       return model->switch_thread(new ModelAction(ATOMIC_RMWR, ord, obj));
 }
 
 /**
@@ -53,23 +53,23 @@ uint64_t model_rmwr_action(void *obj, memory_order ord) {
  * of the RMW action w/o a write.
  */
 uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) {
-       return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
+       return model->switch_thread(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size));
 }
 
 
 /** Performs the write part of a RMW action. */
 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
-       model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
+       model->switch_thread(new ModelAction(ATOMIC_RMW, ord, obj, val));
 }
 
 /** Closes out a RMW action without doing a write. */
 void model_rmwc_action(void *obj, memory_order ord) {
-       model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
+       model->switch_thread(new ModelAction(ATOMIC_RMWC, ord, obj));
 }
 
 /** Issues a fence operation. */
 void model_fence_action(memory_order ord) {
-       model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
+       model->switch_thread(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
 }
 
 /* ---  helper functions --- */
index 30c92d2..037f5f4 100644 (file)
@@ -59,7 +59,7 @@ void FuncInst::set_associated_read(thread_id_t tid, int index, uint32_t marker,
                associated_reads.resize(new_size);
                thrd_markers.resize(new_size);
 
-               for (int i = old_size; i < new_size; i++ ) {
+               for (int i = old_size;i < new_size;i++ ) {
                        associated_reads[i] = new ModelVector<uint64_t>();
                        thrd_markers[i] = new ModelVector<uint32_t>();
                }
@@ -70,7 +70,7 @@ void FuncInst::set_associated_read(thread_id_t tid, int index, uint32_t marker,
        if (read_values->size() < (uint) index + 1) {
                int old_size = read_values->size();
 
-               for (int i = old_size; i < index + 1; i++) {
+               for (int i = old_size;i < index + 1;i++) {
                        read_values->push_back(VALUE_NONE);
                        markers->push_back(0);
                }
index 6b6993d..55785fa 100644 (file)
@@ -693,7 +693,7 @@ void FuncNode::init_marker(thread_id_t tid)
        if (old_size < thread_id + 1) {
                thrd_markers.resize(thread_id + 1);
 
-               for (int i = old_size; i < thread_id + 1; i++) {
+               for (int i = old_size;i < thread_id + 1;i++) {
                        thrd_markers[i] = new ModelVector<uint32_t>();
                        thrd_recursion_depth.push_back(-1);
                }
@@ -725,7 +725,7 @@ void FuncNode::init_local_maps(thread_id_t tid)
                thrd_inst_id_maps.resize(new_size);
                thrd_inst_pred_maps.resize(new_size);
 
-               for (int i = old_size; i < new_size; i++) {
+               for (int i = old_size;i < new_size;i++) {
                        thrd_loc_inst_maps[i] = new ModelVector<loc_inst_map_t *>;
                        thrd_inst_id_maps[i] = new ModelVector<inst_id_map_t *>;
                        thrd_inst_pred_maps[i] = new ModelVector<inst_pred_map_t *>;
@@ -776,7 +776,7 @@ void FuncNode::init_predicate_tree_data_structure(thread_id_t tid)
                thrd_predicate_tree_position.resize(thread_id + 1);
                thrd_predicate_trace.resize(thread_id + 1);
 
-               for (int i = old_size; i < thread_id + 1; i++) {
+               for (int i = old_size;i < thread_id + 1;i++) {
                        thrd_predicate_tree_position[i] = new ModelVector<Predicate *>();
                        thrd_predicate_trace[i] = new ModelVector<predicate_trace_t *>();
                }
@@ -863,7 +863,7 @@ void FuncNode::update_predicate_tree_weight(thread_id_t tid)
        predicate_trace_t * trace = thrd_predicate_trace[id_to_int(tid)]->back();
 
        // Update predicate weights based on prediate trace
-       for (int i = trace->size() - 1; i >= 0; i--) {
+       for (int i = trace->size() - 1;i >= 0;i--) {
                Predicate * node = (*trace)[i];
                ModelVector<Predicate *> * children = node->get_children();
 
index c9c6ff6..f84af3f 100644 (file)
@@ -502,15 +502,15 @@ void ModelHistory::print_func_node()
                func_node->print_predicate_tree();
 
 /*
-               func_inst_list_mt * entry_insts = func_node->get_entry_insts();
-               model_print("function %s has entry actions\n", func_node->get_func_name());
-
-               mllnode<FuncInst*>* it;
-               for (it = entry_insts->begin();it != NULL;it=it->getNext()) {
-                       FuncInst *inst = it->getVal();
-                       model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
-               }
-*/
+                func_inst_list_mt * entry_insts = func_node->get_entry_insts();
+                model_print("function %s has entry actions\n", func_node->get_func_name());
+
+                mllnode<FuncInst*>* it;
+                for (it = entry_insts->begin();it != NULL;it=it->getNext()) {
+                        FuncInst *inst = it->getVal();
+                        model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
+                }
+ */
        }
 }
 
index a255180..391ce2a 100644 (file)
@@ -8,8 +8,8 @@ namespace std {
 
 bool atomic_flag_test_and_set_explicit ( volatile atomic_flag * __a__, memory_order __x__ ) {
        volatile bool * __p__ = &((__a__)->__f__);
-       bool result = (bool) model->switch_to_master(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
-       model->switch_to_master(new ModelAction(ATOMIC_RMW, __x__, (void *) __p__, true));
+       bool result = (bool) model->switch_thread(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
+       model->switch_thread(new ModelAction(ATOMIC_RMW, __x__, (void *) __p__, true));
        return result;
 }
 
@@ -20,7 +20,7 @@ void atomic_flag_clear_explicit
        ( volatile atomic_flag* __a__, memory_order __x__ )
 {
        volatile bool * __p__ = &((__a__)->__f__);
-       model->switch_to_master(new ModelAction(ATOMIC_WRITE, __x__, (void *) __p__, false));
+       model->switch_thread(new ModelAction(ATOMIC_WRITE, __x__, (void *) __p__, false));
 }
 
 void atomic_flag_clear( volatile atomic_flag* __a__ )
index 660a819..a781c40 100644 (file)
 #include <pthread.h>
 
 /* pthread mutex types
-enum
-{
-  PTHREAD_MUTEX_NORMAL
-  PTHREAD_MUTEX_RECURSIVE
-  PTHREAD_MUTEX_ERRORCHECK
-  PTHREAD_MUTEX_DEFAULT
-};*/
+   enum
+   {
+   PTHREAD_MUTEX_NORMAL
+   PTHREAD_MUTEX_RECURSIVE
+   PTHREAD_MUTEX_ERRORCHECK
+   PTHREAD_MUTEX_DEFAULT
+   };*/
 
 typedef void *(*pthread_start_t)(void *);
 
index b1fad8a..e58da19 100644 (file)
@@ -10,5 +10,5 @@
 
 void cdsannotate(uint64_t analysistype, void *annotation) {
        /* seq_cst is just a 'don't care' parameter */
-       model->switch_to_master(new ModelAction(ATOMIC_ANNOTATION, std::memory_order_seq_cst, annotation, analysistype));
+       model->switch_thread(new ModelAction(ATOMIC_ANNOTATION, std::memory_order_seq_cst, annotation, analysistype));
 }
index c06a9be..4d61e53 100644 (file)
@@ -14,14 +14,14 @@ int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
 {
        struct thread_params params = { start_routine, arg };
        /* seq_cst is just a 'don't care' parameter */
-       model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params));
+       model->switch_thread(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params));
        return 0;
 }
 
 int thrd_join(thrd_t t)
 {
        Thread *th = t.priv;
-       model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
+       model->switch_thread(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
        return 0;
 }
 
index c258944..33d8e15 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -188,7 +188,7 @@ void ModelChecker::assert_user_bug(const char *msg)
 {
        /* If feasible bug, bail out now */
        assert_bug(msg);
-       switch_to_master(NULL);
+       switch_thread(NULL);
 }
 
 /** @brief Print bug report listing for this execution (if any bugs exist) */
@@ -288,12 +288,11 @@ void ModelChecker::finish_execution(bool more_executions)
        else
                clear_program_output();
 
-// test code
        execution_number ++;
+       history->set_new_exec_flag();
+
        if (more_executions)
                reset_to_initial_state();
-
-       history->set_new_exec_flag();
 }
 
 /** @brief Run trace analyses on complete trace */
@@ -322,61 +321,7 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const
        return execution->get_thread(act);
 }
 
-/**
- * Switch from a model-checker context to a user-thread context. This is the
- * complement of ModelChecker::switch_to_master and must be called from the
- * model-checker context
- *
- * @param thread The user-thread to switch to
- */
-void ModelChecker::switch_from_master(Thread *thread)
-{
-       scheduler->set_current_thread(thread);
-       Thread::swap(&system_context, thread);
-}
-
-/**
- * Switch from a user-context to the "master thread" context (a.k.a. system
- * context). This switch is made with the intention of exploring a particular
- * model-checking action (described by a ModelAction object). Must be called
- * from a user-thread context.
- *
- * @param act The current action that will be explored. May be NULL only if
- * trace is exiting via an assertion (see ModelExecution::set_assert and
- * ModelExecution::has_asserted).
- * @return Return the value returned by the current action
- */
-uint64_t ModelChecker::switch_to_master(ModelAction *act)
-{
-       if (modellock) {
-               static bool fork_message_printed = false;
-
-               if (!fork_message_printed) {
-                       model_print("Fork handler or dead thread trying to call into model checker...\n");
-                       fork_message_printed = true;
-               }
-               delete act;
-               return 0;
-       }
-       DBG();
-       Thread *old = thread_current();
-       scheduler->set_current_thread(NULL);
-       ASSERT(!old->get_pending());
-
-       if (inspect_plugin != NULL) {
-               inspect_plugin->inspectModelAction(act);
-       }
-
-       old->set_pending(act);
-       if (Thread::swap(old, &system_context) < 0) {
-               perror("swap threads");
-               exit(EXIT_FAILURE);
-       }
-       return old->get_return_value();
-}
-
-void ModelChecker::startRunExecution(Thread *old) 
-{
+void ModelChecker::startRunExecution(Thread *old) {
        while (true) {
                if (params.traceminsize != 0 &&
                                execution->get_curr_seq_num() > checkfree) {
@@ -391,14 +336,11 @@ void ModelChecker::startRunExecution(Thread *old)
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);
 
-                       if (old == thr)
-                               return;
-
                        if (Thread::swap(old, thr) < 0) {
                                perror("swap threads");
                                exit(EXIT_FAILURE);
                        }
-                       continue;
+                       return;
                }
 
                if (execution->has_asserted()) {
@@ -432,7 +374,7 @@ void ModelChecker::startRunExecution(Thread *old)
 Thread* ModelChecker::getNextThread()
 {
        Thread *nextThread = nullptr;
-       for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
+       for (unsigned int i = curr_thread_num;i < get_num_threads();i++) {
                thread_id_t tid = int_to_id(i);
                Thread *thr = get_thread(tid);
 
@@ -453,31 +395,37 @@ Thread* ModelChecker::getNextThread()
 }
 
 /* Swap back to system_context and terminate this execution */
-void ModelChecker::finishRunExecution(Thread *old) 
+void ModelChecker::finishRunExecution(Thread *old)
 {
        scheduler->set_current_thread(NULL);
-       if (Thread::swap(old, &system_context) < 0) {
-               perror("swap threads");
-               exit(EXIT_FAILURE);
-       }
-       break_execution = true;
+
+       /** If we have more executions, we won't make it past this call. */
+       finish_execution(execution_number < params.maxexecutions);
+
+
+       /** We finished the final execution.  Print stuff and exit. */
+       model_print("******* Model-checking complete: *******\n");
+       print_stats();
+
+       /* Have the trace analyses dump their output. */
+       for (unsigned int i = 0;i < trace_analyses.size();i++)
+               trace_analyses[i]->finish();
+
+       /* unlink tmp file created by last child process */
+       char filename[256];
+       snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
+       unlink(filename);
+
+       /* Exit. */
+       _Exit(0);
 }
 
 void ModelChecker::consumeAction()
 {
        ModelAction *curr = chosen_thread->get_pending();
        Thread * th = thread_current();
-       if (curr->get_type() == THREAD_FINISH && th != NULL)  {
-               // Thread finish must be consumed in the master context
-               scheduler->set_current_thread(NULL);
-               if (Thread::swap(th, &system_context) < 0) {
-                       perror("swap threads");
-                       exit(EXIT_FAILURE);
-               }
-       } else {
-               chosen_thread->set_pending(NULL);
-               chosen_thread = execution->take_step(curr);
-       }
+       chosen_thread->set_pending(NULL);
+       chosen_thread = execution->take_step(curr);
 }
 
 /* Allow pending relaxed/release stores or thread actions to perform first */
@@ -492,9 +440,9 @@ void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
                                thread_chosen = true;
                        }
                } else if (act->get_type() == THREAD_CREATE || \
-                                                       act->get_type() == PTHREAD_CREATE || \
-                                                       act->get_type() == THREAD_START || \
-                                                       act->get_type() == THREAD_FINISH) {
+                                                        act->get_type() == PTHREAD_CREATE || \
+                                                        act->get_type() == THREAD_START || \
+                                                        act->get_type() == THREAD_FINISH) {
                        chosen_thread = thr;
                        thread_chosen = true;
                }
@@ -522,7 +470,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        }
 
        old->set_pending(act);
-       
+
        if (old->is_waiting_on(old))
                assert_bug("Deadlock detected (thread %u)", curr_thread_num);
 
@@ -576,15 +524,16 @@ void ModelChecker::handleChosenThread(Thread *old)
                startRunExecution(old);
 }
 
-static void runChecker() {
-       model->run();
-       delete model;
-}
-
 void ModelChecker::startChecker() {
-       startExecution(get_system_context(), runChecker);
+       startExecution();
+       //Need to initial random number generator state to avoid resets on rollback
+       initstate(423121, random_state, sizeof(random_state));
+
        snapshot = take_snapshot();
 
+       //reset random number generator state
+       setstate(random_state);
+
        install_trace_analyses(get_execution());
        redirect_output();
        initMainThread();
@@ -600,67 +549,3 @@ bool ModelChecker::should_terminate_execution()
        }
        return false;
 }
-
-/** @brief Run ModelChecker for the user program */
-void ModelChecker::run()
-{
-       //Need to initial random number generator state to avoid resets on rollback
-       char random_state[256];
-       initstate(423121, random_state, sizeof(random_state));
-       checkfree = params.checkthreshold;
-       for(int exec = 0;exec < params.maxexecutions;exec++) {
-               chosen_thread = init_thread;
-               break_execution = false;
-               do {
-                       if (params.traceminsize != 0 &&
-                                       execution->get_curr_seq_num() > checkfree) {
-                               checkfree += params.checkthreshold;
-                               execution->collectActions();
-                       }
-
-                       thread_chosen = false;
-                       curr_thread_num = 1;
-                       Thread *thr = getNextThread();
-                       if (thr != nullptr) {
-                               switch_from_master(thr);
-                               continue;
-                       }
-
-                       if (break_execution)
-                               break;
-                       if (execution->has_asserted())
-                               break;
-                       if (!chosen_thread)
-                               chosen_thread = get_next_thread();
-                       if (!chosen_thread || chosen_thread->is_model_thread())
-                               break;
-                       if (chosen_thread->just_woken_up()) {
-                               chosen_thread->set_wakeup_state(false);
-                               chosen_thread->set_pending(NULL);
-                               chosen_thread = NULL;
-                               continue;
-                       }
-
-                       /* Consume the next action for a Thread */
-                       ModelAction *curr = chosen_thread->get_pending();
-                       chosen_thread->set_pending(NULL);
-                       chosen_thread = execution->take_step(curr);
-               } while (!should_terminate_execution());
-
-               finish_execution((exec+1) < params.maxexecutions);
-               //restore random number generator state after rollback
-               setstate(random_state);
-       }
-
-       model_print("******* Model-checking complete: *******\n");
-       print_stats();
-
-       /* Have the trace analyses dump their output. */
-       for (unsigned int i = 0;i < trace_analyses.size();i++)
-               trace_analyses[i]->finish();
-
-       /* unlink tmp file created by last child process */
-       char filename[256];
-       snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
-       unlink(filename);
-}
diff --git a/model.h b/model.h
index 19497c0..44ed858 100644 (file)
--- a/model.h
+++ b/model.h
@@ -31,14 +31,10 @@ public:
        ModelChecker();
        ~ModelChecker();
        model_params * getParams();
-       void run();
 
        /** Exit the model checker, intended for pluggins. */
        void exit_model_checker();
 
-       /** @returns the context for the main model-checking system thread */
-       ucontext_t * get_system_context() { return &system_context; }
-
        ModelExecution * get_execution() const { return execution; }
        ModelHistory * get_history() const { return history; }
 
@@ -49,8 +45,6 @@ public:
 
        Thread * get_current_thread() const;
 
-       void switch_from_master(Thread *thread);
-       uint64_t switch_to_master(ModelAction *act);
        uint64_t switch_thread(ModelAction *act);
 
        void assert_bug(const char *msg, ...);
@@ -98,9 +92,8 @@ private:
        Thread * get_next_thread();
        void reset_to_initial_state();
 
-       ucontext_t system_context;
-
        ModelVector<TraceAnalysis *> trace_analyses;
+       char random_state[256];
 
        /** @bref Plugin that can inspect new actions. */
        TraceAnalysis *inspect_plugin;
index 01eed86..7d4e8b1 100644 (file)
@@ -310,27 +310,27 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred, SnapVector<Model
 void NewFuzzer::conditional_sleep(Thread * thread)
 {
 /*
-       int index = paused_thread_list.size();
+        int index = paused_thread_list.size();
 
-       model->getScheduler()->add_sleep(thread);
-       paused_thread_list.push_back(thread);
-       paused_thread_table.put(thread, index); // Update table
+        model->getScheduler()->add_sleep(thread);
+        paused_thread_list.push_back(thread);
+        paused_thread_table.put(thread, index);        // Update table
 
-       // Add the waiting condition to ModelHistory
-       ModelAction * read = thread->get_pending();
-       thread_id_t tid = thread->get_id();
-       FuncNode * func_node = history->get_curr_func_node(tid);
-//     inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
+        // Add the waiting condition to ModelHistory
+        ModelAction * read = thread->get_pending();
+        thread_id_t tid = thread->get_id();
+        FuncNode * func_node = history->get_curr_func_node(tid);
+   //  inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
 
-       Predicate * selected_branch = get_selected_child_branch(tid);
-//     ConcretePredicate * concrete = selected_branch->evaluate(inst_act_map, tid);
-       concrete->set_location(read->get_location());
+        Predicate * selected_branch = get_selected_child_branch(tid);
+   //  ConcretePredicate * concrete = selected_branch->evaluate(inst_act_map, tid);
+        concrete->set_location(read->get_location());
 
-       ASSERT(false);
+        ASSERT(false);
 
-//     history->add_waiting_write(concrete);
-       // history->add_waiting_thread is already called in find_threads
-*/
+   //  history->add_waiting_write(concrete);
+        // history->add_waiting_thread is already called in find_threads
+ */
 }
 
 bool NewFuzzer::has_paused_threads()
index 0028cf1..9b8060a 100644 (file)
@@ -84,36 +84,36 @@ void Predicate::copy_predicate_expr(Predicate * other)
 ConcretePredicate * Predicate::evaluate(thread_id_t tid)
 {
        /*
-       ConcretePredicate * concrete = new ConcretePredicate(tid);
-       PredExprSetIter * it = pred_expressions.iterator();
-
-       while (it->hasNext()) {
-               struct pred_expr * ptr = it->next();
-               uint64_t value = 0;
-
-               switch(ptr->token) {
-               case NOPREDICATE:
-                       break;
-               case EQUALITY:
-                       FuncInst * to_be_compared;
-                       ModelAction * last_act;
-
-                       to_be_compared = ptr->func_inst;
-                       last_act = inst_act_map->get(to_be_compared);
-                       value = last_act->get_reads_from_value();
-                       break;
-               case NULLITY:
-                       break;
-               default:
-                       break;
-               }
-
-               concrete->add_expression(ptr->token, value, ptr->value);
-       }
-
-       delete it;
-       return concrete;
-       */
+          ConcretePredicate * concrete = new ConcretePredicate(tid);
+          PredExprSetIter * it = pred_expressions.iterator();
+
+          while (it->hasNext()) {
+               struct pred_expr * ptr = it->next();
+               uint64_t value = 0;
+
+               switch(ptr->token) {
+               case NOPREDICATE:
+                       break;
+               case EQUALITY:
+                       FuncInst * to_be_compared;
+                       ModelAction * last_act;
+
+                       to_be_compared = ptr->func_inst;
+                       last_act = inst_act_map->get(to_be_compared);
+                       value = last_act->get_reads_from_value();
+                       break;
+               case NULLITY:
+                       break;
+               default:
+                       break;
+               }
+
+               concrete->add_expression(ptr->token, value, ptr->value);
+          }
+
+          delete it;
+          return concrete;
+        */
 
        return NULL;
 }
index f5ce1bc..e95fb37 100644 (file)
@@ -25,7 +25,7 @@ int pthread_create(pthread_t *t, const pthread_attr_t * attr,
        struct pthread_params params = { start_routine, arg };
 
        /* seq_cst is just a 'don't care' parameter */
-       model->switch_to_master(new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params));
+       model->switch_thread(new ModelAction(PTHREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)&params));
 
        return 0;
 }
@@ -34,7 +34,7 @@ int pthread_join(pthread_t t, void **value_ptr) {
        ModelExecution *execution = model->get_execution();
        Thread *th = execution->get_pthread(t);
 
-       model->switch_to_master(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id())));
+       model->switch_thread(new ModelAction(PTHREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(th->get_id())));
 
        if ( value_ptr ) {
                // store return value
@@ -59,7 +59,7 @@ int sched_yield() {
 void pthread_exit(void *value_ptr) {
        Thread * th = thread_current();
        th->set_pthread_return(value_ptr);
-       model->switch_to_master(new ModelAction(THREADONLY_FINISH, std::memory_order_seq_cst, th));
+       model->switch_thread(new ModelAction(THREADONLY_FINISH, std::memory_order_seq_cst, th));
        //Need to exit so we don't return to the program
        real_pthread_exit(NULL);
 }
index 789a101..2b70582 100644 (file)
--- a/sleeps.cc
+++ b/sleeps.cc
@@ -50,7 +50,7 @@ int nanosleep(const struct timespec *rqtp, struct timespec *rmtp)
                struct timespec currtime;
                clock_gettime(CLOCK_MONOTONIC, &currtime);
                uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
-               model->switch_to_master(new ModelAction(THREAD_SLEEP, std::memory_order_seq_cst, time, lcurrtime));
+               model->switch_thread(new ModelAction(THREAD_SLEEP, std::memory_order_seq_cst, time, lcurrtime));
                if (rmtp != NULL) {
                        clock_gettime(CLOCK_MONOTONIC, &currtime);
                        uint64_t lendtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
index 7a5030b..548ae05 100644 (file)
@@ -13,7 +13,7 @@ typedef void (*VoidFuncPtr)();
 void snapshot_system_init(unsigned int numbackingpages,
                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
                                                                                                        unsigned int numheappages);
-void startExecution(ucontext_t * context, VoidFuncPtr entryPoint);
+void startExecution();
 snapshot_id take_snapshot();
 void snapshot_roll_back(snapshot_id theSnapShot);
 
index c049167..0d38edc 100644 (file)
@@ -64,7 +64,6 @@ ucontext_t shared_ctxt;
  *   snapshotid. it is incremented and set in a persistently shared record
  */
 static ucontext_t private_ctxt;
-static ucontext_t exit_ctxt;
 static snapshot_id snapshotid = 0;
 
 /**
@@ -170,13 +169,7 @@ static void fork_loop() {
        }
 }
 
-static void fork_startExecution(ucontext_t *context, VoidFuncPtr entryPoint) {
-       /* setup an "exiting" context */
-       int exit_stack_size = 256;
-       create_context(&exit_ctxt, snapshot_calloc(exit_stack_size, 1), exit_stack_size, fork_exit);
-
-       /* setup the system context */
-       create_context(context, fork_snap->mStackBase, STACK_SIZE_DEFAULT, entryPoint);
+static void fork_startExecution() {
        /* 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);
 }
@@ -184,6 +177,7 @@ static void fork_startExecution(ucontext_t *context, VoidFuncPtr entryPoint) {
 static snapshot_id fork_take_snapshot() {
        model_swapcontext(&shared_ctxt, &private_ctxt);
        DEBUG("TAKESNAPSHOT RETURN\n");
+       fork_snap->mIDToRollback = -1;
        return snapshotid;
 }
 
@@ -191,8 +185,7 @@ static void fork_roll_back(snapshot_id theID)
 {
        DEBUG("Rollback\n");
        fork_snap->mIDToRollback = theID;
-       model_swapcontext(model->get_system_context(), &exit_ctxt);
-       fork_snap->mIDToRollback = -1;
+       fork_exit();
 }
 
 /**
@@ -206,9 +199,8 @@ void snapshot_system_init(unsigned int numbackingpages,
        fork_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages);
 }
 
-void startExecution(ucontext_t *context, VoidFuncPtr entryPoint)
-{
-       fork_startExecution(context, entryPoint);
+void startExecution() {
+       fork_startExecution();
 }
 
 /** Takes a snapshot of memory.
index 8047e1f..73c1d8f 100644 (file)
@@ -46,6 +46,7 @@ public:
 
        ~Thread();
        void complete();
+       void freeResources();
 
        static int swap(ucontext_t *ctxt, Thread *t);
        static int swap(Thread *t, ucontext_t *ctxt);
index 23041b2..9316031 100644 (file)
@@ -61,13 +61,13 @@ Thread * thread_current(void)
 }
 
 void modelexit() {
-       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+       model->switch_thread(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
 }
 
 void initMainThread() {
        atexit(modelexit);
        Thread * curr_thread = thread_current();
-       model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
+       model->switch_thread(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
 }
 
 /**
@@ -80,7 +80,7 @@ void thread_startup()
        Thread * curr_thread = thread_current();
 #ifndef TLS
        /* Add dummy "start" action, just to create a first clock vector */
-       model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
+       model->switch_thread(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
 #endif
 
        /* Call the actual thread function */
@@ -93,7 +93,7 @@ void thread_startup()
        }
 #ifndef TLS
        /* Finish thread properly */
-       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
+       model->switch_thread(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
 #endif
 }
 
@@ -212,7 +212,7 @@ void * helper_thread(void * ptr) {
        curr_thread->helpercontext.uc_stack.ss_sp = curr_thread->helper_stack;
        curr_thread->helpercontext.uc_stack.ss_size = STACK_SIZE;
        curr_thread->helpercontext.uc_stack.ss_flags = 0;
-       curr_thread->helpercontext.uc_link = model->get_system_context();
+       curr_thread->helpercontext.uc_link = NULL;
        makecontext(&curr_thread->helpercontext, finalize_helper_thread, 0);
 
        model_swapcontext(&curr_thread->context, &curr_thread->helpercontext);
@@ -235,7 +235,7 @@ void tlsdestructor(void *v) {
                return;
        }
        /* Finish thread properly */
-       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+       model->switch_thread(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
 }
 #endif
 
@@ -285,7 +285,7 @@ int Thread::create_context()
        context.uc_stack.ss_sp = stack;
        context.uc_stack.ss_size = STACK_SIZE;
        context.uc_stack.ss_flags = 0;
-       context.uc_link = model->get_system_context();
+       context.uc_link = NULL;
 #ifdef TLS
        makecontext(&context, setup_context, 0);
 #else
@@ -335,6 +335,9 @@ int Thread::swap(Thread *t, Thread *t2)
 {
        t->set_state(THREAD_READY);
        t2->set_state(THREAD_RUNNING);
+       if (t == t2)
+               return 0;
+
 #ifdef TLS
        if (t2->tls != NULL)
                set_tls_addr((uintptr_t)t2->tls);
@@ -342,12 +345,15 @@ int Thread::swap(Thread *t, Thread *t2)
        return model_swapcontext(&t->context, &t2->context);
 }
 
-/** Terminate a thread and free its stack. */
+/** Terminate a thread. */
 void Thread::complete()
 {
        ASSERT(!is_complete());
        DEBUG("completed thread %d\n", id_to_int(get_id()));
        state = THREAD_COMPLETED;
+}
+
+void Thread::freeResources() {
        if (stack)
                stack_free(stack);
 #ifdef TLS