From: Brian Demsky Date: Tue, 7 Apr 2020 07:05:48 +0000 (-0700) Subject: Redesign actionlist and change acquire fence X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=15ea44894415d4b1150728658d65c641556e5fcf Redesign actionlist and change acquire fence --- diff --git a/Makefile b/Makefile index 4f83cd99..adb080de 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \ snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \ context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \ sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o newfuzzer.o \ - concretepredicate.o waitobj.o hashfunction.o pipe.o + concretepredicate.o waitobj.o hashfunction.o pipe.o actionlist.o CPPFLAGS += -Iinclude -I. LDFLAGS := -ldl -lrt -rdynamic -lpthread diff --git a/action.cc b/action.cc index d6569544..d90a94ee 100644 --- a/action.cc +++ b/action.cc @@ -38,9 +38,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, last_fence_release(NULL), cv(NULL), rf_cv(NULL), - trace_ref(NULL), - thrdmap_ref(NULL), - action_ref(NULL), value(value), type(type), order(order), @@ -72,9 +69,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, last_fence_release(NULL), cv(NULL), rf_cv(NULL), - trace_ref(NULL), - thrdmap_ref(NULL), - action_ref(NULL), value(value), type(type), order(order), @@ -105,9 +99,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, last_fence_release(NULL), cv(NULL), rf_cv(NULL), - trace_ref(NULL), - thrdmap_ref(NULL), - action_ref(NULL), value(value), type(type), order(order), @@ -142,9 +133,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order last_fence_release(NULL), cv(NULL), rf_cv(NULL), - trace_ref(NULL), - thrdmap_ref(NULL), - action_ref(NULL), value(value), type(type), order(order), @@ -180,9 +168,6 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order last_fence_release(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 35368ef7..c5ba6d7d 100644 --- a/action.h +++ b/action.h @@ -192,12 +192,6 @@ public: /* to accomodate pthread create and join */ Thread * thread_operand; void set_thread_operand(Thread *th) { thread_operand = th; } - void setTraceRef(sllnode *ref) { trace_ref = ref; } - void setThrdMapRef(sllnode *ref) { thrdmap_ref = ref; } - void setActionRef(sllnode *ref) { action_ref = ref; } - sllnode * getTraceRef() { return trace_ref; } - sllnode * getThrdMapRef() { return thrdmap_ref; } - sllnode * getActionRef() { return action_ref; } SNAPSHOTALLOC private: @@ -233,9 +227,6 @@ 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/actionlist.cc b/actionlist.cc new file mode 100644 index 00000000..f859746c --- /dev/null +++ b/actionlist.cc @@ -0,0 +1,248 @@ +#include "actionlist.h" +#include "action.h" +#include +#include "stl-model.h" +#include + +actionlist::actionlist() : + _size(0) +{ +} + +actionlist::~actionlist() { +} + +allnode::allnode() : + count(0) { + bzero(children, sizeof(children)); +} + +allnode::~allnode() { + if (count != 0) + for(int i=0;i * allnode::findPrev(modelclock_t index) { + allnode * ptr = this; + modelclock_t increment = 1; + modelclock_t mask = ALLMASK; + int totalshift = 0; + index -= increment; + + while(1) { + modelclock_t shiftclock = index >> totalshift; + modelclock_t currindex = shiftclock & ALLMASK; + + //See if we went negative... + if (currindex != ALLMASK) { + if (ptr->children[currindex] == NULL) { + //need to keep searching at this level + index -= increment; + continue; + } else { + //found non-null... + if (totalshift != 0) + ptr = ptr->children[currindex]; + //need to increment here... + increment = increment >> ALLBITS; + mask = mask >> ALLBITS; + totalshift -= ALLBITS; + break; + } + } + //If we get here, we already did the decrement earlier...no need to decrement again + ptr = ptr->parent; + increment = increment << ALLBITS; + mask = mask << ALLBITS; + totalshift += ALLBITS; + + if (increment == 0) { + return NULL; + } + } + + while(1) { + while(1) { + modelclock_t shiftclock = index >> totalshift; + modelclock_t currindex = shiftclock & ALLMASK; + if (ptr->children[currindex] != NULL) { + if (totalshift != 0) { + ptr = ptr->children[currindex]; + } else { + allnode * act = ptr->children[currindex]; + sllnode * node = reinterpret_cast*>(((uintptr_t)act) & ALLMASK); + return node; + } + } + index -= increment; + } + + increment = increment >> ALLBITS; + mask = mask >> ALLBITS; + totalshift -= ALLBITS; + } +} + +void actionlist::addAction(ModelAction * act) { + _size++; + int shiftbits = MODELCLOCKBITS - ALLBITS; + modelclock_t clock = act->get_seq_number(); + + allnode * ptr = &root; + do { + int index = (clock >> shiftbits) & ALLMASK; + allnode * tmp = ptr->children[index]; + if (shiftbits == 0) { + sllnode * llnode = new sllnode(); + llnode->val = act; + if (tmp == NULL) { + ptr->children[index] = reinterpret_cast(((uintptr_t) llnode) | ISACT); + sllnode * llnodeprev = ptr->findPrev(index); + if (llnodeprev != NULL) { + + llnode->next = llnodeprev->next; + llnode->prev = llnodeprev; + + //see if we are the new tail + if (llnodeprev->next == NULL) + tail = llnode; + else + llnode->next->prev = llnode; + + llnodeprev->next = llnode; + } else { + //We are the begining + llnode->next = head; + llnode->prev = NULL; + if (head != NULL) { + head->prev = llnode; + } else { + //we are the first node + tail = llnode; + } + + head = llnode; + } + //need to find next link + ptr->count++; + } else { + //handle case where something else is here + + sllnode * llnodeprev = reinterpret_cast*>(((uintptr_t) llnode) & ALLMASK); + llnode->next = llnodeprev->next; + llnode->prev = llnodeprev; + llnode->next->prev = llnode; + llnodeprev->next = llnode; + ptr->children[index] = reinterpret_cast(((uintptr_t) llnode) | ISACT); + } + return; + } else if (tmp == NULL) { + tmp = new allnode(); + ptr->children[index] = tmp; + tmp->parent=ptr; + ptr->count++; + } + shiftbits -= ALLBITS; + ptr = tmp; + } while(1); + +} + +void decrementCount(allnode * ptr) { + ptr->count--; + if (ptr->count == 0) { + if (ptr->parent != NULL) { + for(uint i=0;iparent->children[i]==ptr) { + ptr->parent->children[i] = NULL; + decrementCount(ptr->parent); + } + } + } + delete ptr; + } +} + +void actionlist::removeAction(ModelAction * act) { + int shiftbits = MODELCLOCKBITS - ALLBITS; + modelclock_t clock = act->get_seq_number(); + allnode * ptr = &root; + do { + int index = (clock >> shiftbits) & ALLMASK; + allnode * tmp = ptr->children[index]; + if (shiftbits == 0) { + if (tmp == NULL) { + //not found + return; + } else { + sllnode * llnode = reinterpret_cast *>(((uintptr_t) tmp) & ALLMASK); + bool first = true; + do { + if (llnode->val == act) { + //found node to remove + sllnode * llnodeprev = llnode->prev; + sllnode * llnodenext = llnode->next; + if (llnodeprev != NULL) { + llnodeprev->next = llnodenext; + } else { + head = llnodenext; + } + if (llnodenext != NULL) { + llnodenext->prev = llnodeprev; + } else { + tail = llnodeprev; + } + if (first) { + //see if previous node has same clock as us... + if (llnodeprev->val->get_seq_number() == clock) { + ptr->children[index] = reinterpret_cast(((uintptr_t)llnodeprev) | ISACT); + } else { + //remove ourselves and go up tree + ptr->children[index] = NULL; + decrementCount(ptr); + } + } + delete llnode; + _size--; + return; + } + llnode = llnode->prev; + first = false; + } while(llnode != NULL && llnode->val->get_seq_number() == clock); + //node not found in list... no deletion + return; + } + } else if (tmp == NULL) { + //not found + return; + } + shiftbits -= ALLBITS; + ptr = tmp; + } while(1); +} + +void actionlist::clear() { + for(uint i = 0;i < ALLNODESIZE;i++) { + if (root.children[i] != NULL) { + delete root.children[i]; + root.children[i] = NULL; + } + } + + while(head != NULL) { + sllnode *tmp=head->next; + delete head; + head = tmp; + } + tail=NULL; + + root.count = 0; + _size = 0; +} + +bool actionlist::isEmpty() { + return root.count == 0; +} diff --git a/actionlist.h b/actionlist.h new file mode 100644 index 00000000..70f90eb8 --- /dev/null +++ b/actionlist.h @@ -0,0 +1,52 @@ +#ifndef ACTIONLIST_H +#define ACTIONLIST_H + +#include "classlist.h" +#include "stl-model.h" + +#define ISACT 1 +#define ALLBITS 4 +#define ALLNODESIZE (1 << ALLBITS) +#define ALLMASK ((1 << ALLBITS)-1) +#define MODELCLOCKBITS 32 + +class allnode; +void decrementCount(allnode *); + +class allnode { +public: + allnode(); + ~allnode(); + SNAPSHOTALLOC; + +private: + allnode * parent; + allnode * children[ALLNODESIZE]; + int count; + sllnode * findPrev(modelclock_t index); + friend class actionlist; + friend void decrementCount(allnode *); +}; + +class actionlist { +public: + actionlist(); + ~actionlist(); + void addAction(ModelAction * act); + void removeAction(ModelAction * act); + void clear(); + bool isEmpty(); + uint size() {return _size;} + sllnode * begin() {return head;} + sllnode * end() {return tail;} + + SNAPSHOTALLOC; + +private: + allnode root; + sllnode * head; + sllnode * tail; + + uint _size; +}; +#endif diff --git a/classlist.h b/classlist.h index ccbbbb14..71f54512 100644 --- a/classlist.h +++ b/classlist.h @@ -22,11 +22,14 @@ class FuncInst; class Predicate; class ConcretePredicate; class WaitObj; +class actionlist; + +#include "actionlist.h" struct model_snapshot_members; struct bug_message; -typedef SnapList action_list_t; +typedef actionlist action_list_t; typedef SnapList func_id_list_t; typedef SnapList func_inst_list_t; diff --git a/config.h b/config.h index 74c0c351..f86275a7 100644 --- a/config.h +++ b/config.h @@ -54,7 +54,7 @@ #define FORK_HANDLER_HACK /** Enable smart fuzzer */ -#define NEWFUZZER +//#define NEWFUZZER /** Define semantics of volatile memory operations. */ #define memory_order_volatile_load memory_order_acquire diff --git a/execution.cc b/execution.cc index 97e58511..c37de41a 100644 --- a/execution.cc +++ b/execution.cc @@ -329,6 +329,10 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * read_from(curr, rf); get_thread(curr)->set_return_value(curr->get_return_value()); delete priorset; + //Update acquire fence clock vector + ClockVector * hbcv = get_hb_from_write(curr->get_reads_from()); + if (hbcv != NULL) + get_thread(curr)->get_acq_fence_cv()->merge(hbcv); return canprune && (curr->get_type() == ATOMIC_READ); } priorset->clear(); @@ -400,7 +404,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) state->locked = NULL; /* disable this thread */ - get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr); + get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr); scheduler->sleep(get_thread(curr)); } @@ -469,7 +473,7 @@ void ModelExecution::process_write(ModelAction *curr) * @param curr The ModelAction to process * @return True if synchronization was updated */ -bool ModelExecution::process_fence(ModelAction *curr) +void ModelExecution::process_fence(ModelAction *curr) { /* * fence-relaxed: no-op @@ -479,36 +483,9 @@ bool ModelExecution::process_fence(ModelAction *curr) * sequences * fence-seq-cst: MO constraints formed in {r,w}_modification_order */ - bool updated = false; if (curr->is_acquire()) { - action_list_t *list = &action_trace; - sllnode * rit; - /* Find X : is_read(X) && X --sb-> curr */ - for (rit = list->end();rit != NULL;rit=rit->getPrev()) { - ModelAction *act = rit->getVal(); - if (act == curr) - continue; - if (act->get_tid() != curr->get_tid()) - continue; - /* Stop at the beginning of the thread */ - if (act->is_thread_start()) - break; - /* Stop once we reach a prior fence-acquire */ - if (act->is_fence() && act->is_acquire()) - break; - if (!act->is_read()) - continue; - /* read-acquire will find its own release sequences */ - if (act->is_acquire()) - continue; - - /* Establish hypothetical release sequences */ - ClockVector *cv = get_hb_from_write(act->get_reads_from()); - if (cv != NULL && curr->get_cv()->merge(cv)) - updated = true; - } + curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv()); } - return updated; } /** @@ -1129,11 +1106,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) 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()); - act->setActionRef(list->add_back(act)); + list->addAction(act); } // Update action trace, a total order of all actions - act->setTraceRef(action_trace.add_back(act)); + action_trace.addAction(act); // Update obj_thrd_map, a per location, per thread, order of actions @@ -1145,7 +1122,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) new (&(*vec)[i]) action_list_t(); } if (!canprune && (act->is_read() || act->is_write())) - act->setThrdMapRef((*vec)[tid].add_back(act)); + (*vec)[tid].addAction(act); // Update thrd_last_action, the last action taken by each thread if ((int)thrd_last_action.size() <= tid) @@ -1161,43 +1138,17 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act)); + get_safe_ptr_action(&obj_map, mutex_loc)->addAction(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)) - return list->add_back(act); - else { - for(;rit != NULL;rit=rit->getPrev()) { - if (rit->getVal()->get_seq_number() <= next_seq) { - return list->insertAfter(rit, act); - } - } - return list->add_front(act); - } +void insertIntoActionList(action_list_t *list, ModelAction *act) { + list->addAction(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 list->add_back(act); - } else if (rit->getVal()->get_seq_number() <= next_seq) { - act->create_cv(rit->getVal()); - 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()); - return list->insertAfter(rit, act); - } - } - return list->add_front(act); - } +void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { + act->create_cv(NULL); + list->addAction(act); } /** @@ -1211,7 +1162,7 @@ sllnode* insertIntoActionListAndSetCV(action_list_t *list, ModelA void ModelExecution::add_normal_write_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act)); + 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()); @@ -1221,7 +1172,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act)); + insertIntoActionList(&(*vec)[tid],act); ModelAction * lastact = thrd_last_action[tid]; // Update thrd_last_action, the last action taken by each thrad @@ -1239,7 +1190,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) { for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - write->setActionRef((*vec)[tid].add_back(write)); + (*vec)[tid].addAction(write); } /** @@ -1542,7 +1493,7 @@ void ModelExecution::print_tail() int length = 25; int counter = 0; SnapList list; - for (it = action_trace.end(); it != NULL; it = it->getPrev()) { + for (it = action_trace.end();it != NULL;it = it->getPrev()) { if (counter > length) break; @@ -1697,36 +1648,22 @@ Thread * ModelExecution::take_step(ModelAction *curr) void ModelExecution::removeAction(ModelAction *act) { { - sllnode * listref = act->getTraceRef(); - if (listref != NULL) { - action_trace.erase(listref); - } + action_trace.removeAction(act); } { - sllnode * listref = act->getThrdMapRef(); - if (listref != NULL) { - SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); - (*vec)[act->get_tid()].erase(listref); - } + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + (*vec)[act->get_tid()].removeAction(act); } if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - list->erase(listref); - } + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + list->removeAction(act); } else if (act->is_wait()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref); - } + void *mutex_loc = (void *) act->get_value(); + get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act); } else if (act->is_free()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); - (*vec)[act->get_tid()].erase(listref); - } + SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); + (*vec)[act->get_tid()].removeAction(act); + //Clear it from last_sc_map if (obj_last_sc_map.get(act->get_location()) == act) { obj_last_sc_map.remove(act->get_location()); diff --git a/execution.h b/execution.h index 722b8647..7ca610ca 100644 --- a/execution.h +++ b/execution.h @@ -19,8 +19,6 @@ #include #include "classlist.h" -typedef SnapList action_list_t; - struct PendingFutureValue { PendingFutureValue(ModelAction *writer, ModelAction *reader) : writer(writer), reader(reader) @@ -105,7 +103,7 @@ private: bool initialize_curr_action(ModelAction **curr); bool process_read(ModelAction *curr, SnapVector * rf_set); void process_write(ModelAction *curr); - bool process_fence(ModelAction *curr); + void process_fence(ModelAction *curr); bool process_mutex(ModelAction *curr); void process_thread_action(ModelAction *curr); void read_from(ModelAction *act, ModelAction *rf); diff --git a/fuzzer.cc b/fuzzer.cc index 371838dc..c41af4a0 100644 --- a/fuzzer.cc +++ b/fuzzer.cc @@ -23,7 +23,7 @@ Thread * Fuzzer::selectNotify(action_list_t * waiters) { while(random_index--) it=it->getNext(); Thread *thread = model->get_thread(it->getVal()); - waiters->erase(it); + waiters->removeAction(it->getVal()); return thread; } diff --git a/model.h b/model.h index 62b227e4..63474813 100644 --- a/model.h +++ b/model.h @@ -18,8 +18,6 @@ #include "classlist.h" #include "snapshot-interface.h" -typedef SnapList action_list_t; - /** @brief Model checker execution stats */ struct execution_stats { int num_total; /**< @brief Total number of executions */ diff --git a/stl-model.h b/stl-model.h index d787a2d7..611520fc 100644 --- a/stl-model.h +++ b/stl-model.h @@ -5,7 +5,6 @@ #include "mymemory.h" typedef unsigned int uint; - template class mllnode { public: @@ -165,6 +164,8 @@ private: uint _size; }; +class actionlist; + template class sllnode { public: @@ -179,6 +180,7 @@ private: _Tp val; template friend class SnapList; + friend class actionlist; }; template @@ -537,6 +539,15 @@ public: array[index] = item; } + void remove(type item) { + for(uint i = 0;i < _size;i++) { + if (at(i) == item) { + removeAt(i); + return; + } + } + } + void removeAt(uint index) { for (uint i = index;(i + 1) < _size;i++) { set(i, at(i + 1)); diff --git a/threads-model.h b/threads-model.h index e159697d..f0b88bb2 100644 --- a/threads-model.h +++ b/threads-model.h @@ -102,6 +102,7 @@ public: bool is_model_thread() const { return model_thread; } void * get_stack_addr() { return stack; } + ClockVector * get_acq_fence_cv() { return acq_fence_cv; } friend void thread_startup(); #ifdef TLS @@ -137,6 +138,9 @@ private: /** @brief The parent Thread which created this Thread */ Thread * const parent; + /** @brief Acquire fence cv */ + ClockVector *acq_fence_cv; + /** @brief The THREAD_CREATE ModelAction which created this Thread */ ModelAction *creation; diff --git a/threads.cc b/threads.cc index 8b55a91b..a2d2ed16 100644 --- a/threads.cc +++ b/threads.cc @@ -14,6 +14,7 @@ #include "model.h" #include "execution.h" #include "schedule.h" +#include "clockvector.h" #ifdef TLS #include @@ -359,6 +360,7 @@ void Thread::complete() */ Thread::Thread(thread_id_t tid) : parent(NULL), + acq_fence_cv(new ClockVector()), creation(NULL), pending(NULL), start_routine(NULL), @@ -384,6 +386,7 @@ Thread::Thread(thread_id_t tid) : */ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent) : parent(parent), + acq_fence_cv(new ClockVector()), creation(NULL), pending(NULL), start_routine(func), @@ -416,6 +419,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread */ Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent) : parent(parent), + acq_fence_cv(new ClockVector()), creation(NULL), pending(NULL), start_routine(NULL), @@ -444,6 +448,8 @@ Thread::~Thread() { if (!is_complete()) complete(); + + delete acq_fence_cv; } /** @return The thread_id_t corresponding to this Thread object. */