promise: add 'same_value' helper, force value-checking in CycleGraph
authorBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 21:11:27 +0000 (13:11 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 1 Mar 2013 21:19:19 +0000 (13:19 -0800)
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
model.cc
promise.cc
promise.h

index 7e111b9..be7885c 100644 (file)
@@ -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;
        }
index d7ffc8e..7048096 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;
index c695dc0..c1f1c5c 100644 (file)
@@ -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
index 4131470..0adc3de 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; }