From: Brian Norris <banorris@uci.edu>
Date: Tue, 26 Feb 2013 00:11:54 +0000 (-0800)
Subject: model: bugfix - only allow promise satisfaction for "compatible" threads
X-Git-Tag: oopsla2013~220
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8799a4707e5cb3fe4418a963beef330089511d03;p=model-checker.git

model: bugfix - only allow promise satisfaction for "compatible" threads

I overlooked updating the 'compute_promises()' function when modifying
promises such that they are only resolved by a limited set of threads.
This allows compute_promises() to properly prune out those promises
which are not satisfiable by the current thread.

At the same time, move the act->is_read() check to be an ASSERT(), since
we should never see a promise generated by a non-read ModelAction.
---

diff --git a/model.cc b/model.cc
index 436c337..9e064ea 100644
--- a/model.cc
+++ b/model.cc
@@ -2462,11 +2462,10 @@ void ModelChecker::compute_promises(ModelAction *curr)
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
 		const ModelAction *act = promise->get_action();
+		ASSERT(act->is_read());
 		if (!act->happens_before(curr) &&
-				act->is_read() &&
 				!act->could_synchronize_with(curr) &&
-				!act->same_thread(curr) &&
-				act->get_location() == curr->get_location() &&
+				promise->is_compatible(curr) &&
 				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i, act->is_rmw());
 		}