From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Sep 2012 17:38:58 +0000 (-0700)
Subject: model: fix release_seq for open-ended synchronization
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=86e0aa7f0ea574f58afb0109b1e02a578a429eb1

model: fix release_seq for open-ended synchronization

This fix handles the case where a thread may not yet have synchronized in a way
that ensures no future writes may break a release sequence. If we encounter
such a thread, we can return false (uncertain) and re-check this potential
release sequence later in the execution.
---

diff --git a/model.cc b/model.cc
index 37bddaf9..e71947dd 100644
--- a/model.cc
+++ b/model.cc
@@ -604,6 +604,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
 		if (id_to_int(rf->get_tid()) == (int)i)
 			continue;
 		list = &(*thrd_lists)[i];
+
+		/* Can we ensure no future writes from this thread may break
+		 * the release seq? */
+		bool future_ordered = false;
+
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
 			if (!act->is_write())
@@ -611,13 +616,17 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
 			/* Reach synchronization -> this thread is complete */
 			if (act->happens_before(release))
 				break;
-			if (rf->happens_before(act))
+			if (rf->happens_before(act)) {
+				future_ordered = true;
 				continue;
+			}
 
 			/* Check modification order */
-			if (mo_graph->checkReachable(rf, act))
+			if (mo_graph->checkReachable(rf, act)) {
 				/* rf --mo--> act */
+				future_ordered = true;
 				continue;
+			}
 			if (mo_graph->checkReachable(act, release))
 				/* act --mo--> release */
 				break;
@@ -628,6 +637,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
 			}
 			certain = false;
 		}
+		if (!future_ordered)
+			return false; /* This thread is uncertain */
 	}
 
 	if (certain)