From: Brian Norris <banorris@uci.edu>
Date: Sat, 8 Sep 2012 06:36:00 +0000 (-0700)
Subject: model: fix release sequence with RMW, acq vs. acq/rel
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=46bea910632f80a1565e50060b0d0444637dfe14

model: fix release sequence with RMW, acq vs. acq/rel

Check in a bugfix from Brian D
---

diff --git a/model.cc b/model.cc
index 36b7b449..c8af6cc4 100644
--- a/model.cc
+++ b/model.cc
@@ -566,7 +566,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
 	if (rf->is_release())
 		release_heads->push_back(rf);
 	if (rf->is_rmw()) {
-		if (rf->is_acquire())
+		/* We need a RMW action that is both an acquire and release to stop */
+		/** @todo Need to be smarter here...  In the linux lock
+		 * example, this will run to the beginning of the program for
+		 * every acquire. */
+		if (rf->is_acquire() && rf->is_release())
 			return true; /* complete */
 		return release_seq_head(rf->get_reads_from(), release_heads);
 	}