Move data structures from execution.h to history.h

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 21207fefcb273a0bc0e4ab4a7b5fa4272691d71a..7b8461226a8860d60a0311c2fa2538607c9b1363 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -64,8 +64,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
        fuzzer(new NewFuzzer()),
-       thrd_func_list(),
-       thrd_func_act_lists(),
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
@@ -73,6 +71,9 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        add_thread(model_thread);
        fuzzer->register_engine(m->get_history(), this);
        scheduler->register_engine(this);
+#ifdef TLS
+       pthread_key_create(&pthreadkey, tlsdestructor);
+#endif
 }
 
 /** @brief Destructor */
@@ -288,18 +289,18 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        }
 
        // Remove writes that violate read modification order
-       for (uint i = 0; i < rf_set->size(); i++) {
+       uint i = 0;
+       while (i < rf_set->size()) {
                ModelAction * rf = (*rf_set)[i];
                if (!r_modification_order(curr, rf, NULL, NULL, true)) {
                        (*rf_set)[i] = rf_set->back();
                        rf_set->pop_back();
-               }
+               } else
+                       i++;
        }
 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
-               if (index == -1)// no feasible write exists
-                       return false;
 
                ModelAction *rf = (*rf_set)[index];
 
@@ -318,6 +319,9 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        }
                        return true;
                }
+
+               ASSERT(false);
+               /* TODO: Following code not needed anymore */
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
                rf_set->pop_back();
@@ -718,12 +722,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (curr->is_read() && !second_part_of_rmw) {
                process_read(curr, rf_set);
                delete rf_set;
-
-/*             bool success = process_read(curr, rf_set);
-                delete rf_set;
-                if (!success)
-                        return curr;   // Do not add action to lists
- */
        } else
                ASSERT(rf_set == NULL);
 
@@ -1110,11 +1108,10 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        ModelAction *uninit = NULL;
        int uninit_id = -1;
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       if (list->empty() && act->is_atomic_var()) {
+       SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+       if (objvec->empty() && act->is_atomic_var()) {
                uninit = get_uninitialized_action(act);
                uninit_id = id_to_int(uninit->get_tid());
-               list->push_front(uninit);
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
                if ((int)vec->size() <= uninit_id) {
                        int oldsize = (int) vec->size();
@@ -1159,8 +1156,10 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
 void ModelExecution::add_action_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       list->push_back(act);
+       if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+         list->push_back(act);
+       }
 
        // Update action trace, a total order of all actions
        action_trace.push_back(act);
@@ -1249,9 +1248,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        insertIntoActionListAndSetCV(&action_trace, act);
 
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       insertIntoActionList(list, act);
-
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
        if (tid >= (int)vec->size()) {