From 54e338c739b2aa1f222ca378f1f98b857870a0fa Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 12 Feb 2013 17:24:31 -0800 Subject: [PATCH] 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. --- model.cc | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index c832b03..e21806a 100644 --- 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); -- 2.34.1