model: rework the release sequence fixups

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index cc035084b036015b94181ef7c61b17d2bbf77f65..906416cd90a1aadf8c13eb6cb48c17882d5002d9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2719,31 +2719,14 @@ Thread * ModelChecker::take_step(ModelAction *curr)
                scheduler->remove_thread(curr_thrd);
 
        Thread *next_thrd = get_next_thread(curr);
                scheduler->remove_thread(curr_thrd);
 
        Thread *next_thrd = get_next_thread(curr);

-       next_thrd = scheduler->next_thread(next_thrd);
+       /* Only ask for the next thread from Scheduler if we haven't chosen one
+        * already */
+       if (!next_thrd)
+               next_thrd = scheduler->next_thread(next_thrd);

 
        DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
                        next_thrd ? id_to_int(next_thrd->get_id()) : -1);
 
 
        DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
                        next_thrd ? id_to_int(next_thrd->get_id()) : -1);
 

-       /*
-        * Launch end-of-execution release sequence fixups only when there are:
-        *
-        * (1) no more user threads to run (or when execution replay chooses
-        *     the 'model_thread')
-        * (2) pending release sequences
-        * (3) pending assertions (i.e., data races)
-        * (4) no pending promises
-        */
-       if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
-                       is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
-               model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
-                               pending_rel_seqs->size());
-               ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
-                               std::memory_order_seq_cst, NULL, VALUE_NONE,
-                               model_thread);
-               model_thread->set_pending(fixup);
-               return model_thread;
-       }
-

        return next_thrd;
 }
 
        return next_thrd;
 }
 


@@ -2787,7 +2770,27 @@ void ModelChecker::run()
                        t->set_pending(NULL);
                        t = take_step(curr);
                } while (t && !t->is_model_thread());
                        t->set_pending(NULL);
                        t = take_step(curr);
                } while (t && !t->is_model_thread());

-               /** @TODO Re-write release sequence fixups here */
+
+               /*
+                * Launch end-of-execution release sequence fixups only when
+                * the execution is otherwise feasible AND there are:
+                *
+                * (1) pending release sequences
+                * (2) pending assertions that could be invalidated by a change
+                * in clock vectors (i.e., data races)
+                * (3) no pending promises
+                */
+               while (!pending_rel_seqs->empty() &&
+                               is_feasible_prefix_ignore_relseq() &&
+                               !unrealizedraces.empty()) {
+                       model_print("*** WARNING: release sequence fixup action "
+                                       "(%zu pending release seuqence(s)) ***\n",
+                                       pending_rel_seqs->size());
+                       ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
+                                       std::memory_order_seq_cst, NULL, VALUE_NONE,
+                                       model_thread);
+                       take_step(fixup);
+               };

        } while (next_execution());
 
        print_stats();
        } while (next_execution());
 
        print_stats();