From: Brian Norris Date: Fri, 1 Mar 2013 21:07:56 +0000 (-0800) Subject: promise: bugfix - don't check value, check location X-Git-Tag: oopsla2013~194 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d7ef8a452c36e2ab3e56a8c43639006dc64d5d18 promise: bugfix - don't check value, check location I changed a line previously and didn't even notice that I wasn't matching the comment anymore! Of course, the comment was correct, and my code was wrong. --- diff --git a/model.cc b/model.cc index a66648b..d7ffc8e 100644 --- a/model.cc +++ b/model.cc @@ -2576,7 +2576,7 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check) Promise *promise = (*promises)[i]; // Is this promise on the same location? - if (promise->get_value() != write->get_value()) + if (!promise->same_location(write)) continue; for (unsigned int j = 0; j < promise->get_num_readers(); j++) { diff --git a/promise.cc b/promise.cc index 23b92cd..c695dc0 100644 --- a/promise.cc +++ b/promise.cc @@ -140,3 +140,13 @@ bool Promise::is_compatible_exclusive(const ModelAction *act) const { return get_num_available_threads() == 1 && is_compatible(act); } + +/** + * @brief Check if a ModelAction's location matches this Promise + * @param act The ModelAction to check + * @return True if the action's location matches this Promise + */ +bool Promise::same_location(const ModelAction *act) const +{ + return get_reader(0)->same_var(act); +} diff --git a/promise.h b/promise.h index 5ea7dc5..4131470 100644 --- a/promise.h +++ b/promise.h @@ -36,6 +36,7 @@ class Promise { int get_num_available_threads() const { return num_available_threads; } bool is_compatible(const ModelAction *act) const; bool is_compatible_exclusive(const ModelAction *act) const; + bool same_location(const ModelAction *act) const; modelclock_t get_expiration() const { return fv.expiration; } uint64_t get_value() const { return fv.value; }