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 36b7b4490ffe5bb3c012e3baf3e439f719da2932..c8af6cc4f5bfb2d2c878e6aa035e2cf712d56e29 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);
        }