From 46bea910632f80a1565e50060b0d0444637dfe14 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 7 Sep 2012 23:36:00 -0700
Subject: [PATCH] model: fix release sequence with RMW, acq vs. acq/rel

Check in a bugfix from Brian D
---
 model.cc | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/model.cc b/model.cc
index 36b7b44..c8af6cc 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);
 	}
-- 
2.34.1