X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=887e2efa03df0f31832ff6ee260a1a8b1ed9794d;hp=0006c66c70a3acf89433bfd4013e03ad3f5b3e1c;hb=e4b59e52989269c529e94bea1cd1b9dfe418a0ce;hpb=a22d12cff31e5309eb0033324d3dd0258de53cb5 diff --git a/execution.cc b/execution.cc index 0006c66c..887e2efa 100644 --- a/execution.cc +++ b/execution.cc @@ -4,21 +4,21 @@ #include #include -#include "execution.h" #include "model.h" +#include "execution.h" #include "action.h" #include "nodestack.h" #include "schedule.h" -#include "snapshot-interface.h" #include "common.h" #include "clockvector.h" #include "cyclegraph.h" #include "promise.h" #include "datarace.h" #include "threads-model.h" -#include "output.h" #include "bugmessage.h" +#include + #define INITIAL_THREAD_ID 0 /** @@ -31,11 +31,12 @@ struct model_snapshot_members { used_sequence_numbers(0), next_backtrack(NULL), bugs(), - stats(), failed_promise(false), + hard_failed_promise(false), too_many_reads(false), no_valid_reads(false), bad_synchronization(false), + bad_sc_read(false), asserted(false) { } @@ -49,65 +50,65 @@ struct model_snapshot_members { modelclock_t used_sequence_numbers; ModelAction *next_backtrack; SnapVector bugs; - struct execution_stats stats; bool failed_promise; + bool hard_failed_promise; bool too_many_reads; bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; + bool bad_sc_read; bool asserted; SNAPSHOTALLOC }; /** @brief Constructor */ -ModelExecution::ModelExecution(struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) : +ModelExecution::ModelExecution(ModelChecker *m, + const struct model_params *params, + Scheduler *scheduler, + NodeStack *node_stack) : + model(m), params(params), scheduler(scheduler), - action_trace(new action_list_t()), - thread_map(new HashTable()), - obj_map(new HashTable()), - condvar_waiters_map(new HashTable()), - obj_thrd_map(new HashTable *, uintptr_t, 4 >()), - promises(new SnapVector()), - futurevalues(new SnapVector()), - pending_rel_seqs(new SnapVector()), - thrd_last_action(new SnapVector(1)), - thrd_last_fence_release(new SnapVector()), + action_trace(), + thread_map(2), /* We'll always need at least 2 threads */ + obj_map(), + condvar_waiters_map(), + obj_thrd_map(), + promises(), + futurevalues(), + pending_rel_seqs(), + thrd_last_action(1), + thrd_last_fence_release(), node_stack(node_stack), priv(new struct model_snapshot_members()), - mo_graph(new CycleGraph()), - execution_number(1) + mo_graph(new CycleGraph()) { /* Initialize a model-checker thread, for special ModelActions */ - model_thread = new Thread(get_next_id()); - thread_map->put(id_to_int(model_thread->get_id()), model_thread); + model_thread = new Thread(get_next_id()); // L: Create model thread + add_thread(model_thread); // L: Add model thread to scheduler + scheduler->register_engine(this); + node_stack->register_engine(this); } /** @brief Destructor */ ModelExecution::~ModelExecution() { for (unsigned int i = 0; i < get_num_threads(); i++) - delete thread_map->get(i); - delete thread_map; - - delete obj_thrd_map; - delete obj_map; - delete condvar_waiters_map; - delete action_trace; + delete get_thread(int_to_id(i)); - for (unsigned int i = 0; i < promises->size(); i++) - delete (*promises)[i]; - delete promises; + for (unsigned int i = 0; i < promises.size(); i++) + delete promises[i]; - delete pending_rel_seqs; - - delete thrd_last_action; - delete thrd_last_fence_release; delete mo_graph; delete priv; } +int ModelExecution::get_execution_number() const +{ + return model->get_execution_number(); +} + static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { action_list_t *tmp = hash->get(ptr); @@ -128,8 +129,9 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv=obj_thrd_map->get(obj); +action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const +{ + SnapVector *wrv = obj_thrd_map.get(obj); if (wrv==NULL) return NULL; unsigned int thread=id_to_int(tid); @@ -204,6 +206,13 @@ void ModelExecution::set_bad_synchronization() priv->bad_synchronization = true; } +/** @brief Alert the model-checker that an incorrectly-ordered + * synchronization was made */ +void ModelExecution::set_bad_sc_read() +{ + priv->bad_sc_read = true; +} + bool ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); @@ -268,6 +277,28 @@ bool ModelExecution::is_deadlocked() const return blocking_threads; } +/** + * @brief Check if we are yield-blocked + * + * A program can be "yield-blocked" if all threads are ready to execute a + * yield. + * + * @return True if the program is yield-blocked; false otherwise + */ +bool ModelExecution::is_yieldblocked() const +{ + if (!params->yieldblock) + return false; + + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + Thread *t = get_thread(tid); + if (t->get_pending() && t->get_pending()->is_yield()) + return true; + } + return false; +} + /** * Check if this is a complete execution. That is, have all thread completed * execution (rather than exiting because sleep sets have forced a redundant @@ -277,6 +308,8 @@ bool ModelExecution::is_deadlocked() const */ bool ModelExecution::is_complete_execution() const { + if (is_yieldblocked()) + return false; for (unsigned int i = 0; i < get_num_threads(); i++) if (is_enabled(int_to_id(i))) return false; @@ -311,8 +344,8 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const return NULL; /* Skip past the release */ - action_list_t *list = action_trace; - action_list_t::reverse_iterator rit; + const action_list_t *list = &action_trace; + action_list_t::const_reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) if (*rit == last_release) break; @@ -370,17 +403,22 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const { switch (act->get_type()) { - /* case ATOMIC_FENCE: fences don't directly cause backtracking */ + case ATOMIC_FENCE: + /* Only seq-cst fences can (directly) cause backtracking */ + if (!act->is_seqcst()) + break; case ATOMIC_READ: case ATOMIC_WRITE: case ATOMIC_RMW: { ModelAction *ret = NULL; /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; + if (prev == act) + continue; if (prev->could_synchronize_with(act)) { ret = prev; break; @@ -399,7 +437,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -410,7 +448,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -421,7 +459,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_WAIT: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -436,7 +474,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_NOTIFY_ALL: case ATOMIC_NOTIFY_ONE: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -615,9 +653,9 @@ bool ModelExecution::process_read(ModelAction *curr) case READ_FROM_FUTURE: { /* Read from future value */ struct future_value fv = node->get_future_value(); - Promise *promise = new Promise(curr, fv); + Promise *promise = new Promise(this, curr, fv); curr->set_read_from_promise(promise); - promises->push_back(promise); + promises.push_back(promise); mo_graph->startChanges(); updated = r_modification_order(curr, promise); mo_graph->commitChanges(); @@ -696,14 +734,14 @@ bool ModelExecution::process_mutex(ModelAction *curr) /* Should we go to sleep? (simulate spurious failures) */ if (curr->get_node()->get_misc() == 0) { - get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr); + get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr); /* disable us */ scheduler->sleep(get_thread(curr)); } break; } case ATOMIC_NOTIFY_ALL: { - action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -712,7 +750,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) break; } case ATOMIC_NOTIFY_ONE: { - action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); int wakeupthread = curr->get_node()->get_misc(); action_list_t::iterator it = waiters->begin(); advance(it, wakeupthread); @@ -730,12 +768,13 @@ bool ModelExecution::process_mutex(ModelAction *curr) /** * @brief Check if the current pending promises allow a future value to be sent * - * If one of the following is true: - * (a) there are no pending promises - * (b) the reader and writer do not cross any promises - * Then, it is safe to pass a future value back now. + * It is unsafe to pass a future value back if there exists a pending promise Pr + * such that: + * + * reader --exec-> Pr --exec-> writer * - * Otherwise, we must save the pending future value until (a) or (b) is true + * If such Pr exists, we must save the pending future value until Pr is + * resolved. * * @param writer The operation which sends the future value. Must be a write. * @param reader The operation which will observe the value. Must be a read. @@ -744,10 +783,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) bool ModelExecution::promises_may_allow(const ModelAction *writer, const ModelAction *reader) const { - if (promises->empty()) - return true; - for(int i=promises->size()-1;i>=0;i--) { - ModelAction *pr=(*promises)[i]->get_reader(0); + for (int i = promises.size() - 1; i >= 0; i--) { + ModelAction *pr = promises[i]->get_reader(0); //reader is after promise...doesn't cross any promise if (*reader > *pr) return true; @@ -792,9 +829,10 @@ void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *re /** * Process a write ModelAction * @param curr The ModelAction to process + * @param work The work queue, for adding fixup work * @return True if the mo_graph was updated or promises were resolved */ -bool ModelExecution::process_write(ModelAction *curr) +bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work) { /* Readers to which we may send our future value */ ModelVector send_fv; @@ -807,7 +845,7 @@ bool ModelExecution::process_write(ModelAction *curr) if (promise) { earliest_promise_reader = promise->get_reader(0); - updated_promises = resolve_promise(curr, promise); + updated_promises = resolve_promise(curr, promise, work); } else earliest_promise_reader = NULL; @@ -820,17 +858,17 @@ bool ModelExecution::process_write(ModelAction *curr) if (promises_may_allow(curr, read)) { add_future_value(curr, read); } else { - futurevalues->push_back(PendingFutureValue(curr, read)); + futurevalues.push_back(PendingFutureValue(curr, read)); } } } /* Check the pending future values */ - for (int i = (int)futurevalues->size() - 1; i >= 0; i--) { - struct PendingFutureValue pfv = (*futurevalues)[i]; + for (int i = (int)futurevalues.size() - 1; i >= 0; i--) { + struct PendingFutureValue pfv = futurevalues[i]; if (promises_may_allow(pfv.writer, pfv.reader)) { add_future_value(pfv.writer, pfv.reader); - futurevalues->erase(futurevalues->begin() + i); + futurevalues.erase(futurevalues.begin() + i); } } @@ -858,7 +896,7 @@ bool ModelExecution::process_fence(ModelAction *curr) */ bool updated = false; if (curr->is_acquire()) { - action_list_t *list = action_trace; + action_list_t *list = &action_trace; action_list_t::reverse_iterator rit; /* Find X : is_read(X) && X --sb-> curr */ for (rit = list->rbegin(); rit != list->rend(); rit++) { @@ -910,12 +948,28 @@ bool ModelExecution::process_thread_action(ModelAction *curr) case THREAD_CREATE: { thrd_t *thrd = (thrd_t *)curr->get_location(); struct thread_params *params = (struct thread_params *)curr->get_value(); - Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr)); + Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr)); + curr->set_thread_operand(th); add_thread(th); th->set_creation(curr); /* Promises can be satisfied by children */ - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } + break; + } + case PTHREAD_CREATE: { + thrd_t *thrd = (thrd_t *)curr->get_location(); + struct pthread_params *params = (struct pthread_params *)curr->get_value(); + Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr)); + curr->set_thread_operand(th); + add_thread(th); + th->set_creation(curr); + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (promise->thread_is_available(curr->get_tid())) promise->add_thread(th->get_id()); } @@ -928,6 +982,14 @@ bool ModelExecution::process_thread_action(ModelAction *curr) updated = true; /* trigger rel-seq checks */ break; } + case PTHREAD_JOIN: { + Thread *blocking = curr->get_thread_operand(); + ModelAction *act = get_last_action(blocking->get_id()); + synchronize(act, curr); + updated = true; /* trigger rel-seq checks */ + break; // WL: to be add (modified) + } + case THREAD_FINISH: { Thread *th = get_thread(curr); /* Wake up any joining threads */ @@ -939,8 +1001,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr) } th->complete(); /* Completed thread can't satisfy promises */ - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (promise->thread_is_available(th->get_id())) if (promise->eliminate_thread(th->get_id())) priv->failed_promise = true; @@ -975,8 +1037,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr) void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue) { const ModelAction *write = curr->get_node()->get_relseq_break(); - struct release_seq *sequence = pending_rel_seqs->back(); - pending_rel_seqs->pop_back(); + struct release_seq *sequence = pending_rel_seqs.back(); + pending_rel_seqs.pop_back(); ASSERT(sequence); ModelAction *acquire = sequence->acquire; const ModelAction *rf = sequence->rf; @@ -1000,21 +1062,9 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_ /* Must synchronize */ if (!synchronize(release, acquire)) return; - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check act for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(acquire)); - - /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); - for (; (*rit) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } else { /* Break release sequence with new edges: * release --mo--> write --mo--> rf */ @@ -1091,7 +1141,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) else if (newcurr->is_wait()) newcurr->get_node()->set_misc_max(2); else if (newcurr->is_notify_one()) { - newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size()); + newcurr->get_node()->set_misc_max(get_safe_ptr_action(&condvar_waiters_map, newcurr->get_location())->size()); } return true; /* This was a new ModelAction */ } @@ -1108,6 +1158,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * * @return True if this read established synchronization */ + bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) { ASSERT(rf); @@ -1158,8 +1209,8 @@ bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second) */ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *waiting) { - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (!promise->thread_is_available(waiting->get_id())) continue; for (unsigned int j = 0; j < promise->get_num_readers(); j++) { @@ -1180,9 +1231,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai /** * @brief Check whether a model action is enabled. * - * Checks whether a lock or join operation would be successful (i.e., is the - * lock already locked, or is the joined thread already complete). If not, put - * the action in a waiter list. + * Checks whether an operation would be successful (i.e., is a lock already + * locked, or is the joined thread already complete). + * + * For yield-blocking, yields are never enabled. * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. @@ -1199,6 +1251,8 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { thread_blocking_check_promises(blocking, get_thread(curr)); return false; } + } else if (params->yieldblock && curr->is_yield()) { + return false; } return true; @@ -1213,7 +1267,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { * * @param curr The current action to process * @return The ModelAction that is actually executed; may be different than - * curr; may be NULL, if the current action is not enabled to run + * curr */ ModelAction * ModelExecution::check_current_action(ModelAction *curr) { @@ -1256,7 +1310,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (act->is_read() && !second_part_of_rmw && process_read(act)) update = true; - if (act->is_write() && process_write(act)) + if (act->is_write() && process_write(act, &work_queue)) update = true; if (act->is_fence() && process_fence(act)) @@ -1288,6 +1342,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (rf) { if (r_modification_order(act, rf)) updated = true; + if (act->is_seqcst()) { + ModelAction *last_sc_write = get_last_seq_cst_write(act); + if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { + set_bad_sc_read(); + } + } } else if (promise) { if (r_modification_order(act, promise)) updated = true; @@ -1330,8 +1390,8 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr) bool ModelExecution::promises_expired() const { - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (promise->get_expiration() < priv->used_sequence_numbers) return true; } @@ -1345,7 +1405,7 @@ bool ModelExecution::promises_expired() const */ bool ModelExecution::isfeasibleprefix() const { - return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); + return pending_rel_seqs.size() == 0 && is_feasible_prefix_ignore_relseq(); } /** @@ -1359,7 +1419,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const char *ptr = buf; if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); - if (priv->failed_promise) + if (priv->failed_promise || priv->hard_failed_promise) ptr += sprintf(ptr, "[failed promise]"); if (priv->too_many_reads) ptr += sprintf(ptr, "[too many reads]"); @@ -1367,12 +1427,14 @@ void ModelExecution::print_infeasibility(const char *prefix) const ptr += sprintf(ptr, "[no valid reads-from]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); + if (priv->bad_sc_read) + ptr += sprintf(ptr, "[bad sc read]"); if (promises_expired()) ptr += sprintf(ptr, "[promise expired]"); - if (promises->size() != 0) + if (promises.size() != 0) ptr += sprintf(ptr, "[unresolved promise]"); if (ptr != buf) - model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf); + model_print("%s: %s", prefix ? prefix : "Infeasible", buf); } /** @@ -1381,7 +1443,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_feasible_prefix_ignore_relseq() const { - return !is_infeasible() && promises->size() == 0; + return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise; + } /** @@ -1394,9 +1457,10 @@ bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || priv->no_valid_reads || - priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || + priv->bad_sc_read || + priv->hard_failed_promise || promises_expired(); } @@ -1436,7 +1500,7 @@ bool ModelExecution::should_read_instead(const ModelAction *curr, const T *rf, c if (!mo_graph->checkReachable(rf, other_rf)) return false; - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())]; action_list_t::reverse_iterator rit = list->rbegin(); ASSERT((*rit) == curr); @@ -1479,7 +1543,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const curr->get_node()->get_read_from_promise_size() <= 1) return true; - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); int tid = id_to_int(curr->get_tid()); ASSERT(tid < (int)thrd_lists->size()); action_list_t *list = &(*thrd_lists)[tid]; @@ -1536,7 +1600,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const template bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_read()); @@ -1597,12 +1661,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) } } - /* C++, Section 29.3 statement 3 (second subpoint) */ - if (curr->is_seqcst() && last_sc_write && act == last_sc_write) { - added = mo_graph->addEdge(act, rf) || added; - break; - } - /* * Include at most one act per-thread that "happens * before" curr @@ -1629,9 +1687,9 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) * All compatible, thread-exclusive promises must be ordered after any * concrete loads from the same thread */ - for (unsigned int i = 0; i < promises->size(); i++) - if ((*promises)[i]->is_compatible_exclusive(curr)) - added = mo_graph->addEdge(rf, (*promises)[i]) || added; + for (unsigned int i = 0; i < promises.size(); i++) + if (promises[i]->is_compatible_exclusive(curr)) + added = mo_graph->addEdge(rf, promises[i]) || added; return added; } @@ -1662,7 +1720,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) */ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector *send_fv) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -1734,9 +1792,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) - continue; - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + if (act->get_reads_from() == NULL) { + added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; + } else + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && @@ -1753,7 +1812,8 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorpush_back(act); else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) @@ -1768,13 +1828,57 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorsize(); i++) - if ((*promises)[i]->is_compatible_exclusive(curr)) - added = mo_graph->addEdge(curr, (*promises)[i]) || added; + for (unsigned int i = 0; i < promises.size(); i++) + if (promises[i]->is_compatible_exclusive(curr)) + added = mo_graph->addEdge(curr, promises[i]) || added; return added; } +//This procedure uses cohere to prune future values that are +//guaranteed to generate a coherence violation. +// +//need to see if there is (1) a promise for thread write, (2) +//the promise is sb before write, (3) the promise can only be +//resolved by the thread read, and (4) the promise has same +//location as read/write + +bool ModelExecution::check_coherence_promise(const ModelAction * write, const ModelAction *read) { + thread_id_t write_tid=write->get_tid(); + for(unsigned int i = promises.size(); i>0; i--) { + Promise *pr=promises[i-1]; + if (!pr->same_location(write)) + continue; + //the reading thread is the only thread that can resolve the promise + if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) { + for(unsigned int j=0;jget_num_readers();j++) { + ModelAction *prreader=pr->get_reader(j); + //the writing thread reads from the promise before the write + if (prreader->get_tid()==write_tid && + (*prreader)<(*write)) { + if ((*read)>(*prreader)) { + //check that we don't have a read between the read and promise + //from the same thread as read + bool okay=false; + for(const ModelAction *tmp=read;tmp!=prreader;) { + tmp=tmp->get_node()->get_parent()->get_action(); + if (tmp->is_read() && tmp->same_thread(read)) { + okay=true; + break; + } + } + if (okay) + continue; + } + return false; + } + } + } + } + return true; +} + + /** Arbitrary reads from the future are not allowed. Section 29.3 * part 9 places some constraints. This method checks one result of constraint * constraint. Others require compiler support. */ @@ -1803,10 +1907,11 @@ bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, co * require compiler support): * * If X --hb-> Y --mo-> Z, then X should not read from Z. + * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z. */ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(reader->get_location()); unsigned int i; /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1907,7 +2012,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, release_heads->push_back(fence_release); int tid = id_to_int(rf->get_tid()); - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -2028,12 +2133,43 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire, if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ - pending_rel_seqs->push_back(sequence); + pending_rel_seqs.push_back(sequence); } else { snapshot_free(sequence); } } +/** + * @brief Propagate a modified clock vector to actions later in the execution + * order + * + * After an acquire operation lazily completes a release-sequence + * synchronization, we must update all clock vectors for operations later than + * the acquire in the execution order. + * + * @param acquire The ModelAction whose clock vector must be propagated + * @param work The work queue to which we can add work items, if this + * propagation triggers more updates (e.g., to the modification order) + */ +void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work) +{ + /* Re-check all pending release sequences */ + work->push_back(CheckRelSeqWorkEntry(NULL)); + /* Re-check read-acquire for mo_graph edges */ + work->push_back(MOEdgeWorkEntry(acquire)); + + /* propagate synchronization to later actions */ + action_list_t::reverse_iterator rit = action_trace.rbegin(); + for (; (*rit) != acquire; rit++) { + ModelAction *propagate = *rit; + if (acquire->happens_before(propagate)) { + synchronize(acquire, propagate); + /* Re-check 'propagate' for mo_graph edges */ + work->push_back(MOEdgeWorkEntry(propagate)); + } + } +} + /** * Attempt to resolve all stashed operations that might synchronize with a * release sequence for a given location. This implements the "lazy" portion of @@ -2050,8 +2186,8 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire, bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *work_queue) { bool updated = false; - SnapVector::iterator it = pending_rel_seqs->begin(); - while (it != pending_rel_seqs->end()) { + SnapVector::iterator it = pending_rel_seqs.begin(); + while (it != pending_rel_seqs.end()) { struct release_seq *pending = *it; ModelAction *acquire = pending->acquire; const ModelAction *read = pending->read; @@ -2072,25 +2208,11 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor updated = true; if (updated) { - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check read-acquire for mo_graph edges */ - if (acquire->is_read()) - work_queue->push_back(MOEdgeWorkEntry(acquire)); - - /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); - for (; (*rit) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } if (complete) { - it = pending_rel_seqs->erase(it); + it = pending_rel_seqs.erase(it); snapshot_free(pending); } else { it++; @@ -2115,7 +2237,7 @@ void ModelExecution::add_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()); + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); if (list->empty() && act->is_atomic_var()) { uninit = get_uninitialized_action(act); uninit_id = id_to_int(uninit->get_tid()); @@ -2123,34 +2245,34 @@ void ModelExecution::add_action_to_lists(ModelAction *act) } list->push_back(act); - action_trace->push_back(act); + action_trace.push_back(act); if (uninit) - action_trace->push_front(uninit); + action_trace.push_front(uninit); - SnapVector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); if (uninit) (*vec)[uninit_id].push_front(uninit); - if ((int)thrd_last_action->size() <= tid) - thrd_last_action->resize(get_num_threads()); - (*thrd_last_action)[tid] = act; + if ((int)thrd_last_action.size() <= tid) + thrd_last_action.resize(get_num_threads()); + thrd_last_action[tid] = act; if (uninit) - (*thrd_last_action)[uninit_id] = uninit; + thrd_last_action[uninit_id] = uninit; if (act->is_fence() && act->is_release()) { - if ((int)thrd_last_fence_release->size() <= tid) - thrd_last_fence_release->resize(get_num_threads()); - (*thrd_last_fence_release)[tid] = act; + if ((int)thrd_last_fence_release.size() <= tid) + thrd_last_fence_release.resize(get_num_threads()); + thrd_last_fence_release[tid] = act; } if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); + get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); - SnapVector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -2165,8 +2287,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act) ModelAction * ModelExecution::get_last_action(thread_id_t tid) const { int threadid = id_to_int(tid); - if (threadid < (int)thrd_last_action->size()) - return (*thrd_last_action)[id_to_int(tid)]; + if (threadid < (int)thrd_last_action.size()) + return thrd_last_action[id_to_int(tid)]; else return NULL; } @@ -2179,8 +2301,8 @@ ModelAction * ModelExecution::get_last_action(thread_id_t tid) const ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const { int threadid = id_to_int(tid); - if (threadid < (int)thrd_last_fence_release->size()) - return (*thrd_last_fence_release)[id_to_int(tid)]; + if (threadid < (int)thrd_last_fence_release.size()) + return thrd_last_fence_release[id_to_int(tid)]; else return NULL; } @@ -2196,7 +2318,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); (*rit) != curr; rit++) @@ -2218,8 +2340,12 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const */ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const { - /* All fences should have NULL location */ - action_list_t *list = get_safe_ptr_action(obj_map, NULL); + /* All fences should have location FENCE_LOCATION */ + action_list_t *list = obj_map.get(FENCE_LOCATION); + + if (!list) + return NULL; + action_list_t::reverse_iterator rit = list->rbegin(); if (before_fence) { @@ -2248,7 +2374,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -2283,10 +2409,10 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const */ Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr) { - for (unsigned int i = 0; i < promises->size(); i++) + for (unsigned int i = 0; i < promises.size(); i++) if (curr->get_node()->get_promise(i)) { - Promise *ret = (*promises)[i]; - promises->erase(promises->begin() + i); + Promise *ret = promises[i]; + promises.erase(promises.begin() + i); return ret; } return NULL; @@ -2296,21 +2422,26 @@ Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr) * Resolve a Promise with a current write. * @param write The ModelAction that is fulfilling Promises * @param promise The Promise to resolve + * @param work The work queue, for adding new fixup work * @return True if the Promise was successfully resolved; false otherwise */ -bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise) +bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, + work_queue_t *work) { ModelVector actions_to_check; for (unsigned int i = 0; i < promise->get_num_readers(); i++) { ModelAction *read = promise->get_reader(i); - read_from(read, write); + if (read_from(read, write)) { + /* Propagate the changed clock vector */ + propagate_clockvector(read, work); + } actions_to_check.push_back(read); } /* Make sure the promise's value matches the write's value */ ASSERT(promise->is_compatible(write) && promise->same_value(write)); if (!mo_graph->resolvePromise(promise, write)) - priv->failed_promise = true; + priv->hard_failed_promise = true; /** * @todo It is possible to end up in an inconsistent state, where a @@ -2341,8 +2472,8 @@ bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise) */ void ModelExecution::compute_promises(ModelAction *curr) { - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (!promise->is_compatible(curr) || !promise->same_value(curr)) continue; @@ -2363,8 +2494,8 @@ void ModelExecution::compute_promises(ModelAction *curr) /** Checks promises in response to change in ClockVector Threads. */ void ModelExecution::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv) { - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (!promise->thread_is_available(tid)) continue; for (unsigned int j = 0; j < promise->get_num_readers(); j++) { @@ -2383,8 +2514,8 @@ void ModelExecution::check_promises(thread_id_t tid, ClockVector *old_cv, ClockV void ModelExecution::check_promises_thread_disabled() { - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; if (promise->has_failed()) { priv->failed_promise = true; return; @@ -2410,8 +2541,8 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec { const ModelAction *write = is_read_check ? act->get_reads_from() : act; - for (unsigned int i = 0; i < promises->size(); i++) { - Promise *promise = (*promises)[i]; + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; // Is this promise on the same location? if (!promise->same_location(write)) @@ -2422,7 +2553,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (!pread->happens_before(act)) continue; if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } break; @@ -2434,7 +2565,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (mo_graph->checkReachable(promise, write)) { if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } } @@ -2451,10 +2582,10 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec */ void ModelExecution::compute_relseq_breakwrites(ModelAction *curr) { - if (pending_rel_seqs->empty()) + if (pending_rel_seqs.empty()) return; - struct release_seq *pending = pending_rel_seqs->back(); + struct release_seq *pending = pending_rel_seqs.back(); for (unsigned int i = 0; i < pending->writes.size(); i++) { const ModelAction *write = pending->writes[i]; curr->get_node()->add_relseq_break(write); @@ -2473,7 +2604,7 @@ void ModelExecution::compute_relseq_breakwrites(ModelAction *curr) */ void ModelExecution::build_may_read_from(ModelAction *curr) { - SnapVector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -2518,8 +2649,8 @@ void ModelExecution::build_may_read_from(ModelAction *curr) } /* Inherit existing, promised future values */ - for (i = 0; i < promises->size(); i++) { - const Promise *promise = (*promises)[i]; + for (i = 0; i < promises.size(); i++) { + const Promise *promise = promises[i]; const ModelAction *promise_read = promise->get_reader(0); if (promise_read->same_var(curr)) { /* Only add feasible future-values */ @@ -2583,11 +2714,13 @@ ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) return act; } -static void print_list(action_list_t *list) +static void print_list(const action_list_t *list) { - action_list_t::iterator it; + action_list_t::const_iterator it; - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); + model_print("# t Action type MO Location Value Rf CV\n"); + model_print("------------------------------------------------------------------------------------\n"); unsigned int hash = 0; @@ -2598,7 +2731,7 @@ static void print_list(action_list_t *list) hash = hash^(hash<<3)^((*it)->hash()); } model_print("HASH %u\n", hash); - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); } #if SUPPORT_MOD_ORDER_DUMP @@ -2611,7 +2744,7 @@ void ModelExecution::dumpGraph(char *filename) const mo_graph->dumpNodes(file); ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads()); - for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) { + for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) { ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); @@ -2646,26 +2779,32 @@ void ModelExecution::print_summary() const { #if SUPPORT_MOD_ORDER_DUMP char buffername[100]; - sprintf(buffername, "exec%04u", execution_number); + sprintf(buffername, "exec%04u", get_execution_number()); mo_graph->dumpGraphToFile(buffername); - sprintf(buffername, "graph%04u", execution_number); + sprintf(buffername, "graph%04u", get_execution_number()); dumpGraph(buffername); #endif - model_print("Execution %d:", execution_number); + model_print("Execution trace %d:", get_execution_number()); if (isfeasibleprefix()) { + if (is_yieldblocked()) + model_print(" YIELD BLOCKED"); if (scheduler->all_threads_sleeping()) model_print(" SLEEP-SET REDUNDANT"); - model_print("\n"); + if (have_bug_reports()) + model_print(" DETECTED BUG(S)"); } else print_infeasibility(" INFEASIBLE"); - print_list(action_trace); model_print("\n"); - if (!promises->empty()) { + + print_list(&action_trace); + model_print("\n"); + + if (!promises.empty()) { model_print("Pending promises:\n"); - for (unsigned int i = 0; i < promises->size(); i++) { + for (unsigned int i = 0; i < promises.size(); i++) { model_print(" [P%u] ", i); - (*promises)[i]->print(); + promises[i]->print(); } model_print("\n"); } @@ -2678,7 +2817,10 @@ void ModelExecution::print_summary() const */ void ModelExecution::add_thread(Thread *t) { - thread_map->put(id_to_int(t->get_id()), t); + unsigned int i = id_to_int(t->get_id()); + if (i >= thread_map.size()) + thread_map.resize(i + 1); + thread_map[i] = t; if (!t->is_model_thread()) scheduler->add_thread(t); } @@ -2690,7 +2832,10 @@ void ModelExecution::add_thread(Thread *t) */ Thread * ModelExecution::get_thread(thread_id_t tid) const { - return thread_map->get(id_to_int(tid)); + unsigned int i = id_to_int(tid); + if (i < thread_map.size()) + return thread_map[i]; + return NULL; } /** @@ -2716,8 +2861,8 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const */ int ModelExecution::get_promise_number(const Promise *promise) const { - for (unsigned int i = 0; i < promises->size(); i++) - if ((*promises)[i] == promise) + for (unsigned int i = 0; i < promises.size(); i++) + if (promises[i] == promise) return i; /* Not found */ return -1; @@ -2759,9 +2904,26 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons /* Do not split atomic RMW */ if (curr->is_rmwr()) return get_thread(curr); + if (curr->is_write()) { +// std::memory_order order = curr->get_mo(); +// switch(order) { +// case std::memory_order_relaxed: +// return get_thread(curr); +// case std::memory_order_release: +// return get_thread(curr); +// defalut: +// return NULL; +// } + return NULL; + } + /* Follow CREATE with the created thread */ + /* which is not needed, because model.cc takes care of this */ if (curr->get_type() == THREAD_CREATE) + return curr->get_thread_operand(); + if (curr->get_type() == PTHREAD_CREATE) { return curr->get_thread_operand(); + } return NULL; } @@ -2803,12 +2965,12 @@ Thread * ModelExecution::take_step(ModelAction *curr) */ void ModelExecution::fixup_release_sequences() { - while (!pending_rel_seqs->empty() && + while (!pending_rel_seqs.empty() && is_feasible_prefix_ignore_relseq() && - !unrealizedraces.empty()) { + haveUnrealizedRaces()) { model_print("*** WARNING: release sequence fixup action " "(%zu pending release seuqence(s)) ***\n", - pending_rel_seqs->size()); + pending_rel_seqs.size()); ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ, std::memory_order_seq_cst, NULL, VALUE_NONE, model_thread);