From: Brian Norris <banorris@uci.edu>
Date: Tue, 25 Sep 2012 23:56:02 +0000 (-0700)
Subject: model: re-check release sequences after THREAD_JOIN
X-Git-Tag: pldi2013~153
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=5236350c6c02c09a167a461fce69c581768f9c03;ds=sidebyside

model: re-check release sequences after THREAD_JOIN

If a THREAD-specific operation (from process_thread_action()) added any
synchronization, we should re-check all release sequences.
---

diff --git a/model.cc b/model.cc
index 2b902ba..3593cef 100644
--- a/model.cc
+++ b/model.cc
@@ -626,7 +626,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			bool update = false; /* update this location's release seq's */
 			bool update_all = false; /* update all release seq's */
 
-			process_thread_action(curr);
+			if (process_thread_action(curr))
+				update_all = true;
 
 			if (act->is_read() && process_read(act, second_part_of_rmw))
 				update = true;