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.

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7e111b95a3a4bc43334d7037260fdc85ccbfc9c7..be7885c5c1d66a71837f16f07433a913b8c209c1 100644 (file)
--- 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 d7ffc8e972d7466c7611b393d03afd5a96d5cce0..7048096ca25e0cbe0ad9928504802de4231c5a18 100644 (file)
--- 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 c695dc0ea21a4657cc04fd8601a28c77752f579b..c1f1c5c07782ffd74374d7f8cbe52613d2099fdc 100644 (file)
--- 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 4131470457cc7e4eb2ed2520ed2489aa8f3de66e..0adc3de1aabb47d9d8df7a007d59eb09f391a257 100644 (file)
--- 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; }