From: Brian Norris <banorris@uci.edu>
Date: Thu, 27 Sep 2012 17:53:59 +0000 (-0700)
Subject: model: push mo_graph cycle check into release_seq code
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=3323cca9507640ddc9e38cf93c2e737ca2df9fd7;ds=sidebyside

model: push mo_graph cycle check into release_seq code

Release sequences traveral should only be undertaken if the mo_graph has
no cycles. Instead of just making this check a hack within
resolve_promises(), make it part of every release sequence exploration.
---

diff --git a/model.cc b/model.cc
index fd906858..cf58e9c0 100644
--- a/model.cc
+++ b/model.cc
@@ -1111,6 +1111,10 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  */
 bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
+	/* Only check for release sequences if there are no cycles */
+	if (mo_graph->checkForCycles())
+		return false;
+
 	while (rf) {
 		ASSERT(rf->is_write());
 
@@ -1419,12 +1423,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
-
-			/* Only read (and check for release sequences) if this
-			 * write (esp. RMW) doesn't create cycles */
-			if (!mo_graph->checkForCycles())
-				read->read_from(write);
-
+			read->read_from(write);
 			//First fix up the modification order for actions that happened
 			//before the read
 			r_modification_order(read, write);