model: pull 'has_asserted()' check out of take_step()
authorBrian Norris <banorris@uci.edu>
Wed, 13 Feb 2013 01:24:31 +0000 (17:24 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 15 Feb 2013 22:55:02 +0000 (14:55 -0800)
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.

model.cc

index c832b03..e21806a 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);