From: Brian Norris <banorris@uci.edu>
Date: Fri, 1 Mar 2013 21:11:27 +0000 (-0800)
Subject: promise: add 'same_value' helper, force value-checking in CycleGraph
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=875ebf8e11b4bdd702604785837b6b91b748900d;p=cdsspec-compiler.git

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 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; }