From: Brian Norris <banorris@uci.edu>
Date: Sun, 7 Oct 2012 22:23:37 +0000 (-0700)
Subject: model: add release sequence model_thread ASSERT()
X-Git-Tag: pldi2013~97^2~1^2~4
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=04980c8b06eb8f1688876dd0989c64e4bc8bcb5b

model: add release sequence model_thread ASSERT()

This ASSERT() should ensure that model-checker threads are always
'future_ordered'.
---

diff --git a/model.cc b/model.cc
index 1fcb8fc..8e3af8a 100644
--- a/model.cc
+++ b/model.cc
@@ -1334,6 +1334,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 				th->is_complete())
 			future_ordered = true;
 
+		ASSERT(!th->is_model_thread() || future_ordered);
+
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
 			/* Reach synchronization -> this thread is complete */