From 54e338c739b2aa1f222ca378f1f98b857870a0fa Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
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