From: Brian Norris <banorris@uci.edu>
Date: Thu, 20 Sep 2012 17:59:14 +0000 (-0700)
Subject: model: release_seq_head: improve ordering of tests
X-Git-Tag: pldi2013~167^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=05f82cd6ab941db2d63ca83e778a430752de1900;p=model-checker.git

model: release_seq_head: improve ordering of tests

We can get useful information from a non-write action, as long as we aren't
checking it for modification order or breaking of the release sequence.
---

diff --git a/model.cc b/model.cc
index d2fc366..508f3b9 100644
--- a/model.cc
+++ b/model.cc
@@ -1124,8 +1124,6 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
-			if (!act->is_write())
-				continue;
 			/* Reach synchronization -> this thread is complete */
 			if (act->happens_before(release))
 				break;
@@ -1134,6 +1132,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 				continue;
 			}
 
+			/* Only writes can break release sequences */
+			if (!act->is_write())
+				continue;
+
 			/* Check modification order */
 			if (mo_graph->checkReachable(rf, act)) {
 				/* rf --mo--> act */