From: Brian Norris <banorris@uci.edu>
Date: Wed, 27 Feb 2013 00:39:09 +0000 (-0800)
Subject: model: bugfix - correct RR coherence for Promises
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=963f325c5b5df37487e17c3a05f4d15efabb8870

model: bugfix - correct RR coherence for Promises

We should not skip a read just because it has an unresolved promises;
the CycleGraph can now support read-read coherence edges between any
combination of Promise and ModelAction.
---

diff --git a/model.cc b/model.cc
index 44613792..bfb63e48 100644
--- a/model.cc
+++ b/model.cc
@@ -1765,13 +1765,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
-					const ModelAction *prevreadfrom = act->get_reads_from();
-					//if the previous read is unresolved, keep going...
-					if (prevreadfrom == NULL)
-						continue;
-
-					if (!prevreadfrom->equals(rf)) {
-						added = mo_graph->addEdge(prevreadfrom, rf) || added;
+					const ModelAction *prevrf = act->get_reads_from();
+					const Promise *prevrf_promise = act->get_reads_from_promise();
+					if (prevrf) {
+						if (!prevrf->equals(rf))
+							added = mo_graph->addEdge(prevrf, rf) || added;
+					} else if (!prevrf->equals(rf)) {
+						added = mo_graph->addEdge(prevrf_promise, rf) || added;
 					}
 				}
 				break;
diff --git a/promise.h b/promise.h
index 5b0e356b..c131d743 100644
--- a/promise.h
+++ b/promise.h
@@ -41,6 +41,9 @@ class Promise {
 
 	void print() const;
 
+	bool equals(const Promise *x) const { return this == x; }
+	bool equals(const ModelAction *x) const { return false; }
+
 	SNAPSHOTALLOC
  private:
 	/** @brief Thread ID(s) for thread(s) that potentially can satisfy this