X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=f2c50c4321c67cd83da4c905ac1bcd652307b4a0;hp=c09f74b4cbef071927c1d284c1a838e513fc7288;hb=d28d1a3b7aafbcd2caf80de26721293126830fa8;hpb=7bfea91f33595532cf618fe3d090e8021f578795 diff --git a/execution.cc b/execution.cc index c09f74b..f2c50c4 100644 --- a/execution.cc +++ b/execution.cc @@ -58,52 +58,42 @@ struct model_snapshot_members { /** @brief Constructor */ ModelExecution::ModelExecution(ModelChecker *m, - struct model_params *params, + 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()) { /* 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); + add_thread(model_thread); 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 get_thread(int_to_id(i)); - delete obj_thrd_map; - delete obj_map; - delete condvar_waiters_map; - delete action_trace; + for (unsigned int i = 0; i < promises.size(); i++) + delete promises[i]; - for (unsigned int i = 0; i < promises->size(); i++) - delete (*promises)[i]; - delete promises; - - delete pending_rel_seqs; - - delete thrd_last_action; - delete thrd_last_fence_release; delete mo_graph; delete priv; } @@ -135,7 +125,7 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv=obj_thrd_map->get(obj); + SnapVector *wrv = obj_thrd_map.get(obj); if (wrv==NULL) return NULL; unsigned int thread=id_to_int(tid); @@ -274,6 +264,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 @@ -283,6 +295,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; @@ -317,8 +331,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; @@ -376,17 +390,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; @@ -405,7 +424,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; @@ -416,7 +435,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; @@ -427,7 +446,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; @@ -442,7 +461,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; @@ -623,7 +642,7 @@ bool ModelExecution::process_read(ModelAction *curr) struct future_value fv = node->get_future_value(); 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(); @@ -702,14 +721,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)); @@ -718,7 +737,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); @@ -750,10 +769,10 @@ bool ModelExecution::process_mutex(ModelAction *curr) bool ModelExecution::promises_may_allow(const ModelAction *writer, const ModelAction *reader) const { - if (promises->empty()) + 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; @@ -826,17 +845,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); } } @@ -864,7 +883,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++) { @@ -920,8 +939,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr) 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()); } @@ -945,8 +964,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; @@ -981,8 +1000,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; @@ -1012,7 +1031,7 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_ work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); + action_list_t::reverse_iterator rit = action_trace.rbegin(); for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { @@ -1097,7 +1116,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 */ } @@ -1164,8 +1183,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++) { @@ -1186,9 +1205,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. @@ -1205,6 +1225,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; @@ -1219,7 +1241,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) { @@ -1336,8 +1358,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; } @@ -1351,7 +1373,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(); } /** @@ -1375,7 +1397,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const ptr += sprintf(ptr, "[bad sw ordering]"); 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); @@ -1387,7 +1409,7 @@ 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; } /** @@ -1442,7 +1464,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); @@ -1485,7 +1507,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]; @@ -1542,7 +1564,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()); @@ -1635,9 +1657,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; } @@ -1668,7 +1690,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()); @@ -1774,9 +1796,9 @@ 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; } @@ -1812,7 +1834,7 @@ bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, co */ 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++) { @@ -1913,7 +1935,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; @@ -2034,7 +2056,7 @@ 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); } @@ -2056,8 +2078,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; @@ -2085,7 +2107,7 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace->rbegin(); + action_list_t::reverse_iterator rit = action_trace.rbegin(); for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; if (acquire->happens_before(propagate)) { @@ -2096,7 +2118,7 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor } } if (complete) { - it = pending_rel_seqs->erase(it); + it = pending_rel_seqs.erase(it); snapshot_free(pending); } else { it++; @@ -2121,7 +2143,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()); @@ -2129,34 +2151,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); @@ -2171,8 +2193,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; } @@ -2185,8 +2207,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; } @@ -2202,7 +2224,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++) @@ -2224,8 +2246,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) { @@ -2254,7 +2280,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++) @@ -2289,10 +2315,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; @@ -2347,8 +2373,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; @@ -2369,8 +2395,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++) { @@ -2389,8 +2415,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; @@ -2416,8 +2442,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)) @@ -2457,10 +2483,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); @@ -2479,7 +2505,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()); @@ -2524,8 +2550,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 */ @@ -2589,9 +2615,9 @@ 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"); @@ -2617,7 +2643,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); @@ -2660,18 +2686,20 @@ void ModelExecution::print_summary() const model_print("Execution %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"); } else print_infeasibility(" INFEASIBLE"); - print_list(action_trace); + print_list(&action_trace); model_print("\n"); - if (!promises->empty()) { + 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"); } @@ -2684,7 +2712,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); } @@ -2696,7 +2727,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; } /** @@ -2722,8 +2756,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; @@ -2809,12 +2843,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);