From: Brian Norris <banorris@uci.edu>
Date: Thu, 7 Feb 2013 00:39:52 +0000 (-0800)
Subject: model: add read-write coherence for promise nodes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e08fe0c24bc8d577e1487a3368c56d5a5244d66b;p=cdsspec-compiler.git

model: add read-write coherence for promise nodes

Promises must be ordered after any other loads from the same thread.
---

diff --git a/model.cc b/model.cc
index 15718e1..3d89dc3 100644
--- a/model.cc
+++ b/model.cc
@@ -1619,6 +1619,14 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 		}
 	}
 
+	/*
+	 * All compatible, thread-exclusive promises must be ordered after any
+	 * concrete loads from the same thread
+	 */
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i]->is_compatible_exclusive(curr))
+			added = mo_graph->addEdge(rf, (*promises)[i]) || added;
+
 	return added;
 }