model: pull 'has_asserted()' check out of take_step()

Checks for mid-execution assertions should occur before take_step().
This can catch a mid-step bug (e.g., data race or user-assertion) that
happens between ModelAction steps.

diff --git a/model.cc b/model.cc
index c832b03710fc360ab17bcb5b3afe7a5920c1cfa6..e21806a18a82fd37c2fd3ccfdbe312929a071d99 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2681,9 +2681,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
  */
 Thread * ModelChecker::take_step(ModelAction *curr)
 {
-       if (has_asserted())
-               return NULL;
-
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
 
@@ -2754,6 +2751,11 @@ void ModelChecker::run()
                        scheduler->next_thread(t);
                        Thread::swap(&system_context, t);
 
+                       /* Catch assertions from prior take_step or from
+                        * between-ModelAction bugs (e.g., data races) */
+                       if (has_asserted())
+                               break;
+
                        /* Consume the next action for a Thread */
                        ModelAction *curr = t->get_pending();
                        t->set_pending(NULL);