X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=465849afa03b5a0946236528b8aea7f7703940b4;hb=63e202b2db7a90e176db54c864d2e54ec535c03f;hp=6739d2c85ee2ca51dd3963c471c811e12f0711b3;hpb=ae1340cbd7d2f75d76a4199597f454290badcc8b;p=model-checker.git diff --git a/model.cc b/model.cc index 6739d2c..465849a 100644 --- a/model.cc +++ b/model.cc @@ -1808,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr) } } + /* + * All compatible, thread-exclusive promises must be ordered after any + * concrete stores to the same thread, or else they can be merged with + * this store later + */ + 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; } @@ -2322,7 +2331,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const */ bool ModelChecker::resolve_promises(ModelAction *write) { - bool resolved = false; + bool haveResolved = false; std::vector< ModelAction *, ModelAlloc > actions_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { @@ -2340,13 +2349,13 @@ bool ModelChecker::resolve_promises(ModelAction *write) //after the read. post_r_modification_order(read, write); //Make sure the promise's value matches the write's value - ASSERT(promise->get_value() == write->get_value()); + ASSERT(promise->is_compatible(write)); delete promise; promises->erase(promises->begin() + promise_index); actions_to_check.push_back(read); - resolved = true; + haveResolved = true; } else promise_index++; } @@ -2355,11 +2364,11 @@ bool ModelChecker::resolve_promises(ModelAction *write) //resolve promises for (unsigned int i = 0; i < actions_to_check.size(); i++) { - ModelAction *read=actions_to_check[i]; + ModelAction *read = actions_to_check[i]; mo_check_promises(read->get_tid(), write, read); } - return resolved; + return haveResolved; } /**