model: bugfix - release sequences - handle Thread completion
authorBrian Norris <banorris@uci.edu>
Tue, 25 Sep 2012 23:39:07 +0000 (16:39 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 25 Sep 2012 23:52:52 +0000 (16:52 -0700)
A completed Thread cannot generate any new writes that would break release
sequences.

model.cc

index 66ca8be..a9d9477 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1161,7 +1161,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                bool future_ordered = false;
 
                ModelAction *last = get_last_action(int_to_id(i));
                bool future_ordered = false;
 
                ModelAction *last = get_last_action(int_to_id(i));
-               if (last && rf->happens_before(last))
+               if (last && (rf->happens_before(last) ||
+                               last->get_type() == THREAD_FINISH))
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {