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 436c337d3932f4d45a7d13ee0e8fe674d1a0ea9a..9e064ea2c76bbebbe02fb03fcdf0bbf47a57dfb3 100644 (file)
--- 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());
                }