Merge

diff --git a/action.cc b/action.cc
index 881072948096add52df9eb4d202ff4dc33614dd7..ec7332dc696dc6221628e9139e004b59e8ac8d4d 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -39,6 +39,9 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        uninitaction(NULL),
        cv(NULL),
        rf_cv(NULL),
+       trace_ref(NULL),
+       thrdmap_ref(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -71,6 +74,9 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        uninitaction(NULL),
        cv(NULL),
        rf_cv(NULL),
+       trace_ref(NULL),
+       thrdmap_ref(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -102,6 +108,9 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        uninitaction(NULL),
        cv(NULL),
        rf_cv(NULL),
+       trace_ref(NULL),
+       thrdmap_ref(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -137,6 +146,9 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        uninitaction(NULL),
        cv(NULL),
        rf_cv(NULL),
+       trace_ref(NULL),
+       thrdmap_ref(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -173,6 +185,9 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        uninitaction(NULL),
        cv(NULL),
        rf_cv(NULL),
+       trace_ref(NULL),
+       thrdmap_ref(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),

diff --git a/action.h b/action.h
index 8a7743ff7f2c5cac90413d5e96ff137a2817f1c5..15bb02ea5dec0a686570bffd8d13e552a37248d5 100644 (file)
--- a/action.h
+++ b/action.h
@@ -189,6 +189,9 @@ public:
        void set_thread_operand(Thread *th) { thread_operand = th; }
        void set_uninit_action(ModelAction *act) { uninitaction = act; }
        ModelAction * get_uninit_action() { return uninitaction; }
+       void setTraceRef(sllnode<ModelAction *> *ref) { trace_ref = ref; }
+       void setThrdMapRef(sllnode<ModelAction *> *ref) { thrdmap_ref = ref; }
+       void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;
@@ -224,6 +227,10 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
+       sllnode<ModelAction *> * trace_ref;
+       sllnode<ModelAction *> * thrdmap_ref;
+       sllnode<ModelAction *> * action_ref;
+
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;

diff --git a/execution.cc b/execution.cc
index 39abc039377504405fd9e7417684317b53d3450a..185874ee7f07e560e35be0e4a301725609c87a39 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -316,6 +316,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        if (canprune && curr->get_type() == ATOMIC_READ) {
                                int tid = id_to_int(curr->get_tid());
                                (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+                               curr->setThrdMapRef(NULL);
                        }
                        return true;
                }
@@ -1120,13 +1121,13 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
                                new (&(*vec)[i]) action_list_t();
                        }
                }
-               (*vec)[uninit_id].push_front(uninit);
+               uninit->setActionRef((*vec)[uninit_id].add_front(uninit));
        }
 
        // Update action trace, a total order of all actions
-       if (uninit)
-               action_trace.push_front(uninit);
-
+       if (uninit) {
+               uninit->setTraceRef(action_trace.add_front(uninit));
+       }
        // 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 ((int)vec->size() <= tid) {
@@ -1136,7 +1137,7 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
                        new (&(*vec)[i]) action_list_t();
        }
        if (uninit)
-               (*vec)[uninit_id].push_front(uninit);
+               uninit->setThrdMapRef((*vec)[uninit_id].add_front(uninit));
 
        // Update thrd_last_action, the last action taken by each thrad
        if ((int)thrd_last_action.size() <= tid)
@@ -1157,12 +1158,13 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
        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);
+               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+               act->setActionRef(list->add_back(act));
        }
 
        // Update action trace, a total order of all actions
-       action_trace.push_back(act);
+       act->setTraceRef(action_trace.add_back(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());
@@ -1172,9 +1174,9 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       (*vec)[tid].push_back(act);
+       act->setThrdMapRef((*vec)[tid].add_back(act));
 
-       // Update thrd_last_action, the last action taken by each thrad
+       // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)
                thrd_last_action.resize(get_num_threads());
        thrd_last_action[tid] = act;
@@ -1188,7 +1190,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
-               get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
+               act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
 
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
                if ((int)vec->size() <= tid) {
@@ -1197,41 +1199,42 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                        for(uint i = oldsize;i < priv->next_thread_id;i++)
                                new (&(*vec)[i]) action_list_t();
                }
-               (*vec)[tid].push_back(act);
+               act->setThrdMapRef((*vec)[tid].add_back(act));
        }
 }
 
-void insertIntoActionList(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* 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))
-               list->push_back(act);
+               return list->add_back(act);
        else {
                for(;rit != NULL;rit=rit->getPrev()) {
                        if (rit->getVal()->get_seq_number() == next_seq) {
-                               list->insertAfter(rit, act);
-                               break;
+                               return list->insertAfter(rit, act);
                        }
                }
+               return NULL;
        }
 }
 
-void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
        sllnode<ModelAction*> * rit = list->end();
        modelclock_t next_seq = act->get_seq_number();
        if (rit == NULL) {
                act->create_cv(NULL);
+               return NULL;
        } else if (rit->getVal()->get_seq_number() == next_seq) {
                act->create_cv(rit->getVal());
-               list->push_back(act);
+               return list->add_back(act);
        } else {
                for(;rit != NULL;rit=rit->getPrev()) {
                        if (rit->getVal()->get_seq_number() == next_seq) {
                                act->create_cv(rit->getVal());
-                               list->insertAfter(rit, act);
-                               break;
+                               return list->insertAfter(rit, act);
                        }
                }
+               return NULL;
        }
 }
 
@@ -1246,7 +1249,7 @@ void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
-       insertIntoActionListAndSetCV(&action_trace, act);
+       act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, 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());
@@ -1256,7 +1259,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       insertIntoActionList(&(*vec)[tid],act);
+       act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
 
        // Update thrd_last_action, the last action taken by each thrad
        if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
@@ -1273,7 +1276,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) {
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       (*vec)[tid].push_back(write);
+       write->setActionRef((*vec)[tid].add_back(write));
 }
 
 /**

diff --git a/execution.h b/execution.h
index e25a72e9b697401b60dd5951aa7ef96cc0e390b6..421781272c0aa3ae8743bac1b2b85d23460102ff 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -132,15 +132,16 @@ private:
 
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler * const scheduler;
+       action_list_t action_trace;
+
 
        SnapVector<Thread *> thread_map;
        SnapVector<Thread *> pthread_map;
        uint32_t pthread_counter;
 
-       action_list_t action_trace;
 
        /** Per-object list of actions. Maps an object (i.e., memory location)
-        * to a trace of all actions performed on the object. 
+        * to a trace of all actions performed on the object.
         * Used only for SC fences, unlocks, & wait.
         */
        HashTable<const void *, action_list_t *, uintptr_t, 2> obj_map;

diff --git a/history.cc b/history.cc
index 7e5166fdf1294352f2e942963db3fa8ebbee8f64..d334cb7de10cc3141cd86d5942107155d70ffb9e 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -385,7 +385,7 @@ WaitObj * ModelHistory::getWaitObj(thread_id_t tid)
 }
 
 void ModelHistory::add_waiting_thread(thread_id_t self_id,
-thread_id_t waiting_for_id, FuncNode * target_node, int dist)
+                                                                                                                                                       thread_id_t waiting_for_id, FuncNode * target_node, int dist)
 {
        WaitObj * self_wait_obj = getWaitObj(self_id);
        self_wait_obj->add_waiting_for(waiting_for_id, target_node, dist);
@@ -413,7 +413,7 @@ void ModelHistory::remove_waiting_thread(thread_id_t tid)
 }
 
 void ModelHistory::stop_waiting_for_node(thread_id_t self_id,
-thread_id_t waiting_for_id, FuncNode * target_node)
+                                                                                                                                                                thread_id_t waiting_for_id, FuncNode * target_node)
 {
        WaitObj * self_wait_obj = getWaitObj(self_id);
        bool thread_removed = self_wait_obj->remove_waiting_for_node(waiting_for_id, target_node);

diff --git a/newfuzzer.cc b/newfuzzer.cc
index c9d3f1773419d424524bf0554145d17122cd7bcc..9898ea59441381ad032d100843eda47e68368e38 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -93,7 +93,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
  * @return False if no child matches read_inst
  */
 bool NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_inst,
-inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
+                                                                                                                                                        inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
 {
        available_branches_tmp_storage.clear();
 
@@ -191,7 +191,7 @@ Predicate * NewFuzzer::get_selected_child_branch(thread_id_t tid)
  * @return true if rf_set is pruned
  */
 bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
-SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map)
+                                                                                                                SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map)
 {
        if (pred == NULL)
                return false;
@@ -376,7 +376,7 @@ bool NewFuzzer::find_threads(ModelAction * pending_read)
 }
 
 bool NewFuzzer::check_predicate_expressions(PredExprSet * pred_expressions,
-inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate)
+                                                                                                                                                                               inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate)
 {
        bool satisfy_predicate = true;
 
@@ -386,31 +386,31 @@ inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate)
                bool equality;
 
                switch (expression->token) {
-                       case NOPREDICATE:
-                               *no_predicate = true;
-                               break;
-                       case EQUALITY:
-                               FuncInst * to_be_compared;
-                               ModelAction * last_act;
-                               uint64_t last_read;
-
-                               to_be_compared = expression->func_inst;
-                               last_act = inst_act_map->get(to_be_compared);
-                               last_read = last_act->get_reads_from_value();
-
-                               equality = (write_val == last_read);
-                               if (equality != expression->value)
-                                       satisfy_predicate = false;
-                               break;
-                       case NULLITY:
-                               // TODO: implement likely to be null
-                               equality = ((void*) (write_val & 0xffffffff) == NULL);
-                               if (equality != expression->value)
-                                       satisfy_predicate = false;
-                               break;
-                       default:
-                               model_print("unknown predicate token\n");
-                               break;
+               case NOPREDICATE:
+                       *no_predicate = true;
+                       break;
+               case EQUALITY:
+                       FuncInst * to_be_compared;
+                       ModelAction * last_act;
+                       uint64_t last_read;
+
+                       to_be_compared = expression->func_inst;
+                       last_act = inst_act_map->get(to_be_compared);
+                       last_read = last_act->get_reads_from_value();
+
+                       equality = (write_val == last_read);
+                       if (equality != expression->value)
+                               satisfy_predicate = false;
+                       break;
+               case NULLITY:
+                       // TODO: implement likely to be null
+                       equality = ((void*) (write_val & 0xffffffff) == NULL);
+                       if (equality != expression->value)
+                               satisfy_predicate = false;
+                       break;
+               default:
+                       model_print("unknown predicate token\n");
+                       break;
                }
 
                if (!satisfy_predicate)

diff --git a/stl-model.h b/stl-model.h
index cbcae7c04162f979cebb3d338cced3ad5d97e15e..d787a2d7951d1cb0589f219a2678a7a4060f7ccd 100644 (file)
--- a/stl-model.h
+++ b/stl-model.h
@@ -214,6 +214,33 @@ public:
                _size++;
        }
 
+       sllnode<_Tp>* add_front(_Tp val) {
+               sllnode<_Tp> * tmp = new sllnode<_Tp>();
+               tmp->prev = NULL;
+               tmp->next = head;
+               tmp->val = val;
+               if (head == NULL)
+                       tail = tmp;
+               else
+                       head->prev = tmp;
+               head = tmp;
+               _size++;
+               return tmp;
+       }
+
+       sllnode<_Tp> * add_back(_Tp val) {
+               sllnode<_Tp> * tmp = new sllnode<_Tp>();
+               tmp->prev = tail;
+               tmp->next = NULL;
+               tmp->val = val;
+               if (tail == NULL)
+                       head = tmp;
+               else tail->next = tmp;
+               tail = tmp;
+               _size++;
+               return tmp;
+       }
+
        void pop_front() {
                sllnode<_Tp> *tmp = head;
                head = head->next;
@@ -246,7 +273,7 @@ public:
                _size=0;
        }
 
-       void insertAfter(sllnode<_Tp> * node, _Tp val) {
+       sllnode<_Tp> * insertAfter(sllnode<_Tp> * node, _Tp val) {
                sllnode<_Tp> *tmp = new sllnode<_Tp>();
                tmp->val = val;
                tmp->prev = node;
@@ -258,6 +285,7 @@ public:
                        tmp->next->prev = tmp;
                }
                _size++;
+               return tmp;
        }
 
        void insertBefore(sllnode<_Tp> * node, _Tp val) {