From: Brian Norris <banorris@uci.edu>
Date: Wed, 13 Feb 2013 01:24:31 +0000 (-0800)
Subject: model: pull 'has_asserted()' check out of take_step()
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=54e338c739b2aa1f222ca378f1f98b857870a0fa

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 c832b037..e21806a1 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);