model: fix release sequence with RMW, acq vs. acq/rel
authorBrian Norris <banorris@uci.edu>
Sat, 8 Sep 2012 06:36:00 +0000 (23:36 -0700)
committerBrian Norris <banorris@uci.edu>
Sat, 8 Sep 2012 06:36:00 +0000 (23:36 -0700)
Check in a bugfix from Brian D

model.cc

index 36b7b44..c8af6cc 100644 (file)
--- 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);
        }