From: Brian Norris <banorris@uci.edu>
Date: Mon, 8 Oct 2012 06:16:03 +0000 (-0700)
Subject: model: be sure trace is "final feasible" before continuing to fixup
X-Git-Tag: pldi2013~97^2~1^2~1
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=92c453e0b51244839270e67528e7a18ba6af82b0

model: be sure trace is "final feasible" before continuing to fixup

Release sequences fixup can break pretty badly if there are outstanding
promises. Solution: check for final-feasible traces before continuing to
fixup.
---

diff --git a/model.cc b/model.cc
index 08ea329..e23e9ec 100644
--- a/model.cc
+++ b/model.cc
@@ -1984,9 +1984,10 @@ bool ModelChecker::take_step() {
 	 *     the 'model_thread')
 	 * (2) pending release sequences
 	 * (3) pending assertions (i.e., data races)
+	 * (4) no pending promises
 	 */
 	if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
-			!unrealizedraces.empty()) {
+			isfinalfeasible() && !unrealizedraces.empty()) {
 		printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
 				pending_rel_seqs->size());
 		ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,