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 08ea3294b3b963b63ec8d63f3d1a88a39dc7b728..e23e9ec0a990b38e962b249f4d32c666f9885689 100644 (file)
--- 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)
         *     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()) &&
         */
        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,
                printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
                                pending_rel_seqs->size());
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,