allow ModelHistory to process non-atomic actions when they are created

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 50e052a14ebd147d1739d5ca2735c5d500122502..c6962bc07aeeea50c693c02c78a3aaf5ed3fbe84 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -66,7 +66,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer()),
        thrd_func_list(),
-       thrd_func_inst_lists(),
+       thrd_func_act_lists(),
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
@@ -153,6 +153,11 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
                if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
                        return true;
        }
+       if (asleep->is_sleep()) {
+               if (fuzzer->shouldWake(asleep))
+                       return true;
+       }
+
        return false;
 }
 
@@ -275,6 +280,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        add_normal_write_to_lists(act);
        add_write_to_lists(act);
        w_modification_order(act);
+       model->get_history()->process_action(act, act->get_tid());
        return act;
 }
 
@@ -650,6 +656,9 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
                if (!blocking->is_complete()) {
                        return false;
                }
+       } else if (curr->is_sleep()) {
+               if (!fuzzer->shouldSleep(curr))
+                       return false;
        }
 
        return true;
@@ -1105,7 +1114,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                        int oldsize = (int) vec->size();
                        vec->resize(uninit_id + 1);
                        for(int i=oldsize;i<uninit_id+1;i++) {
-                         new(&(*vec)[i]) action_list_t();
+                               new(&(*vec)[i]) action_list_t();
                        }
                }
                (*vec)[uninit_id].push_front(uninit);
@@ -1123,7 +1132,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                uint oldsize =vec->size();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
-                 new (&(*vec)[i]) action_list_t();
+                       new (&(*vec)[i]) action_list_t();
        }
        (*vec)[tid].push_back(act);
        if (uninit)
@@ -1152,7 +1161,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                        uint oldsize = vec->size();
                        vec->resize(priv->next_thread_id);
                        for(uint i=oldsize;i<priv->next_thread_id;i++)
-                         new (&(*vec)[i]) action_list_t();
+                               new (&(*vec)[i]) action_list_t();
                }
                (*vec)[tid].push_back(act);
        }
@@ -1161,11 +1170,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 void insertIntoActionList(action_list_t *list, ModelAction *act) {
        sllnode<ModelAction*> * rit = list->end();
        modelclock_t next_seq = act->get_seq_number();
-       if (rit == NULL || (rit->getVal())->get_seq_number() == next_seq)
+       if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
                list->push_back(act);
        else {
                for(;rit != NULL;rit=rit->getPrev()) {
-                       if ((rit->getVal())->get_seq_number() == next_seq) {
+                       if (rit->getVal()->get_seq_number() == next_seq) {
                                list->insertAfter(rit, act);
                                break;
                        }
@@ -1214,7 +1223,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
                uint oldsize =vec->size();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
-                 new (&(*vec)[i]) action_list_t();
+                       new (&(*vec)[i]) action_list_t();
        }
        insertIntoActionList(&(*vec)[tid],act);
 
@@ -1231,7 +1240,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) {
                uint oldsize =vec->size();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
-                 new (&(*vec)[i]) action_list_t();
+                       new (&(*vec)[i]) action_list_t();
        }
        (*vec)[tid].push_back(write);
 }
@@ -1653,7 +1662,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        curr = check_current_action(curr);
        ASSERT(curr);
 
-       /* Process this action in ModelHistory for records*/
+       /* Process this action in ModelHistory for records */
        model->get_history()->process_action( curr, curr->get_tid() );
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())