From: Brian Norris <banorris@uci.edu>
Date: Tue, 5 Feb 2013 22:10:06 +0000 (-0800)
Subject: model: add write-to-promise edges
X-Git-Tag: oopsla2013~287
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=90342c146c207107ec0bf05cb70b2d7defbeaa3e;p=model-checker.git

model: add write-to-promise edges

Assume that any time a promise exists, is compatible with a store, and
is exclusive to the same thread as the store, that it is mod-ordered
after that store. This should never produce cycles, until we decide to
begin satisfying promises. At that point, if there's a cycle, then we
must either merge nodes (i.e., the store must satisfy that promise) or
else we discard the execution for the moment and perform the
satisfaction at a later point in the search space.
---

diff --git a/model.cc b/model.cc
index 6739d2c..691ab83 100644
--- a/model.cc
+++ b/model.cc
@@ -1808,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 		}
 	}
 
+	/*
+	 * All compatible, thread-exclusive promises must be ordered after any
+	 * concrete stores to the same thread, or else they can be merged with
+	 * this store later
+	 */
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i]->is_compatible_exclusive(curr))
+			added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
 	return added;
 }