From: Brian Norris <banorris@uci.edu>
Date: Thu, 20 Sep 2012 17:47:31 +0000 (-0700)
Subject: model: release sequences: check last action in each thread
X-Git-Tag: pldi2013~167^2~1
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=663a0dcbf36fd68a8d5783fcf7b218d17e2f9aad

model: release sequences: check last action in each thread

Previously, release_seq_head would only examine actions on a particular, given
object to determine a release sequence. However, we can get information
regarding the possibility of future disruptive writes by checking the clock
vector of the last action of each thread, regardless of object.
---

diff --git a/model.cc b/model.cc
index a7c99af..d2fc366 100644
--- a/model.cc
+++ b/model.cc
@@ -1118,6 +1118,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 		 * the release seq? */
 		bool future_ordered = false;
 
+		ModelAction *last = get_last_action(int_to_id(i));
+		if (last && rf->happens_before(last))
+			future_ordered = true;
+
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
 			if (!act->is_write())