Add references to lists

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 b1687a75069609aaf88961059c39433cc0cb3c91..80fc7b3c949e5e732608e05e677d582d98a46180 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -318,6 +318,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;
                }
@@ -1122,13 +1123,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) {
@@ -1138,7 +1139,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)
@@ -1160,11 +1161,12 @@ 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);
+               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());
@@ -1174,9 +1176,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;
@@ -1190,7 +1192,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) {
@@ -1199,41 +1201,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;
        }
 }
 
@@ -1248,7 +1251,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());
@@ -1258,7 +1261,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())
@@ -1275,7 +1278,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 2dc3333bb3deb8a3d804d6369658dcdfa771337d..356c59a27f604fcbb5c618495f33ec47ca148ba8 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -137,7 +137,7 @@ private:
        Scheduler * const scheduler;
        action_list_t action_trace;
 
-  
+
        SnapVector<Thread *> thread_map;
        SnapVector<Thread *> pthread_map;
        uint32_t pthread_counter;

diff --git a/stl-model.h b/stl-model.h
index a334c27276d572581aa72b34b7d06515c91dc3ce..d787a2d7951d1cb0589f219a2678a7a4060f7ccd 100644 (file)
--- a/stl-model.h
+++ b/stl-model.h
@@ -214,7 +214,7 @@ public:
                _size++;
        }
 
-       sllnode<_Tp>add_front(_Tp val) {
+       sllnode<_Tp>* add_front(_Tp val) {
                sllnode<_Tp> * tmp = new sllnode<_Tp>();
                tmp->prev = NULL;
                tmp->next = head;
@@ -273,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;
@@ -285,6 +285,7 @@ public:
                        tmp->next->prev = tmp;
                }
                _size++;
+               return tmp;
        }
 
        void insertBefore(sllnode<_Tp> * node, _Tp val) {