From 92c453e0b51244839270e67528e7a18ba6af82b0 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sun, 7 Oct 2012 23:16:03 -0700 Subject: [PATCH] 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. --- model.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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, -- 2.34.1