From: Brian Demsky Date: Thu, 12 Dec 2019 07:19:11 +0000 (-0800) Subject: Add references to lists X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=01ffef59b0692d6f43f4094372f0d70b71b0abd4;ds=sidebyside Add references to lists --- diff --git a/action.cc b/action.cc index 88107294..ec7332dc 100644 --- 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 8a7743ff..15bb02ea 100644 --- 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 *ref) { trace_ref = ref; } + void setThrdMapRef(sllnode *ref) { thrdmap_ref = ref; } + void setActionRef(sllnode *ref) { action_ref = ref; } SNAPSHOTALLOC private: const char * get_type_str() const; @@ -224,6 +227,10 @@ private: */ ClockVector *cv; ClockVector *rf_cv; + sllnode * trace_ref; + sllnode * thrdmap_ref; + sllnode * 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 b1687a75..80fc7b3c 100644 --- a/execution.cc +++ b/execution.cc @@ -318,6 +318,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * 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 *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 *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 *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* insertIntoActionList(action_list_t *list, ModelAction *act) { sllnode * 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* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { sllnode * 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 *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;inext_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;inext_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 2dc3333b..356c59a2 100644 --- a/execution.h +++ b/execution.h @@ -137,7 +137,7 @@ private: Scheduler * const scheduler; action_list_t action_trace; - + SnapVector thread_map; SnapVector pthread_map; uint32_t pthread_counter; diff --git a/stl-model.h b/stl-model.h index a334c272..d787a2d7 100644 --- 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) {