X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=f0763cbfca28971b9dfd36a0fe5e76dcae41f8aa;hp=2aa94cfd84b4da470277f0ea81f6118d880e9f3e;hb=c29b803ac6dce04a6531d33e36341eb662124835;hpb=a635c5cdf004963a948dfb40e0fa27ce258bbccf diff --git a/model.cc b/model.cc index 2aa94cfd..f0763cbf 100644 --- a/model.cc +++ b/model.cc @@ -1082,14 +1082,15 @@ bool ModelChecker::process_write(ModelAction *curr) /* Readers to which we may send our future value */ ModelVector send_fv; - bool updated_mod_order = w_modification_order(curr, &send_fv); - int promise_idx = get_promise_to_resolve(curr); const ModelAction *earliest_promise_reader; bool updated_promises = false; - if (promise_idx >= 0) { - earliest_promise_reader = (*promises)[promise_idx]->get_reader(0); - updated_promises = resolve_promise(curr, promise_idx); + bool updated_mod_order = w_modification_order(curr, &send_fv); + Promise *promise = pop_promise_to_resolve(curr); + + if (promise) { + earliest_promise_reader = promise->get_reader(0); + updated_promises = resolve_promise(curr, promise); } else earliest_promise_reader = NULL; @@ -1100,10 +1101,10 @@ bool ModelChecker::process_write(ModelAction *curr) futurevalues->push_back(PendingFutureValue(curr, read)); } - if (promises->size() == 0) { + if (promises->empty()) { for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; - add_future_value(pfv.writer, pfv.act); + add_future_value(pfv.writer, pfv.reader); } futurevalues->clear(); } @@ -1128,6 +1129,7 @@ bool ModelChecker::process_fence(ModelAction *curr) * use in later synchronization * fence-acquire (this function): search for hypothetical release * sequences + * fence-seq-cst: MO constraints formed in {r,w}_modification_order */ bool updated = false; if (curr->is_acquire()) { @@ -1812,6 +1814,9 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) /* Last SC fence in the current thread */ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + ModelAction *last_sc_write = NULL; + if (curr->is_seqcst()) + last_sc_write = get_last_seq_cst_write(curr); /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1831,7 +1836,18 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; - if (act->is_write() && !act->equals(rf) && act != curr) { + /* Skip curr */ + if (act == curr) + continue; + /* Don't want to add reflexive edges on 'rf' */ + if (act->equals(rf)) { + if (act->happens_before(curr)) + break; + else + continue; + } + + if (act->is_write()) { /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { @@ -1852,15 +1868,19 @@ bool ModelChecker::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. Don't consider reflexively. + * before" curr */ - if (act->happens_before(curr) && act != curr) { + if (act->happens_before(curr)) { if (act->is_write()) { - if (!act->equals(rf)) { - added = mo_graph->addEdge(act, rf) || added; - } + added = mo_graph->addEdge(act, rf) || added; } else { const ModelAction *prevrf = act->get_reads_from(); const Promise *prevrf_promise = act->get_reads_from_promise(); @@ -2454,8 +2474,11 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const action_list_t *list = get_safe_ptr_action(obj_map, 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 != list->rend(); rit++) - if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr) + for (rit = list->rbegin(); (*rit) != curr; rit++) + ; + rit++; /* Skip past curr */ + for ( ; rit != list->rend(); rit++) + if ((*rit)->is_write() && (*rit)->is_seqcst()) return *rit; return NULL; } @@ -2528,29 +2551,31 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const } /** - * @brief Find the promise, if any to resolve for the current action + * @brief Find the promise (if any) to resolve for the current action and + * remove it from the pending promise vector * @param curr The current ModelAction. Should be a write. - * @return The (non-negative) index for the Promise to resolve, if any; - * otherwise -1 + * @return The Promise to resolve, if any; otherwise NULL */ -int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const +Promise * ModelChecker::pop_promise_to_resolve(const ModelAction *curr) { for (unsigned int i = 0; i < promises->size(); i++) - if (curr->get_node()->get_promise(i)) - return i; - return -1; + if (curr->get_node()->get_promise(i)) { + Promise *ret = (*promises)[i]; + promises->erase(promises->begin() + i); + return ret; + } + return NULL; } /** * Resolve a Promise with a current write. * @param write The ModelAction that is fulfilling Promises - * @param promise_idx The index corresponding to the promise + * @param promise The Promise to resolve * @return True if the Promise was successfully resolved; false otherwise */ -bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx) +bool ModelChecker::resolve_promise(ModelAction *write, Promise *promise) { ModelVector actions_to_check; - Promise *promise = (*promises)[promise_idx]; for (unsigned int i = 0; i < promise->get_num_readers(); i++) { ModelAction *read = promise->get_reader(i); @@ -2562,7 +2587,6 @@ bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx) if (!mo_graph->resolvePromise(promise, write)) priv->failed_promise = true; - promises->erase(promises->begin() + promise_idx); /** * @todo It is possible to end up in an inconsistent state, where a * "resolved" promise may still be referenced if