From 875ebf8e11b4bdd702604785837b6b91b748900d Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Mar 2013 13:11:27 -0800 Subject: [PATCH] promise: add 'same_value' helper, force value-checking in CycleGraph This fixes a potential bug, in which a write could merge with a different promised value. It's unclear whether this ever manifested itself, since I believe we had some implicit logic that would ensure that this did not happen. --- cyclegraph.cc | 3 ++- model.cc | 2 +- promise.cc | 10 ++++++++++ promise.h | 1 + 4 files changed, 14 insertions(+), 2 deletions(-) diff --git a/cyclegraph.cc b/cyclegraph.cc index 7e111b9..be7885c 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -151,7 +151,8 @@ bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node, ASSERT(p_node->is_promise()); const Promise *promise = p_node->getPromise(); - if (!promise->is_compatible(w_node->getAction())) { + if (!promise->is_compatible(w_node->getAction()) || + !promise->same_value(w_node->getAction())) { hasCycles = true; return false; } diff --git a/model.cc b/model.cc index d7ffc8e..7048096 100644 --- a/model.cc +++ b/model.cc @@ -2505,7 +2505,7 @@ void ModelChecker::compute_promises(ModelAction *curr) { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value()) + if (!promise->is_compatible(curr) || !promise->same_value(curr)) continue; bool satisfy = true; diff --git a/promise.cc b/promise.cc index c695dc0..c1f1c5c 100644 --- a/promise.cc +++ b/promise.cc @@ -141,6 +141,16 @@ bool Promise::is_compatible_exclusive(const ModelAction *act) const return get_num_available_threads() == 1 && is_compatible(act); } +/** + * @brief Check if a store's value matches this Promise + * @param write The store to check + * @return True if the store's written value matches this Promise + */ +bool Promise::same_value(const ModelAction *write) const +{ + return get_value() == write->get_write_value(); +} + /** * @brief Check if a ModelAction's location matches this Promise * @param act The ModelAction to check diff --git a/promise.h b/promise.h index 4131470..0adc3de 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_value(const ModelAction *write) const; bool same_location(const ModelAction *act) const; modelclock_t get_expiration() const { return fv.expiration; } -- 2.34.1