From: Brian Norris <banorris@uci.edu>
Date: Tue, 25 Sep 2012 23:39:07 +0000 (-0700)
Subject: model: bugfix - release sequences - handle Thread completion
X-Git-Tag: pldi2013~157
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=cf29a02731b7257e13cd9f666a920339fe581040

model: bugfix - release sequences - handle Thread completion

A completed Thread cannot generate any new writes that would break release
sequences.
---

diff --git a/model.cc b/model.cc
index 66ca8be..a9d9477 100644
--- 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));
-		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++) {