From: Brian Norris <banorris@uci.edu>
Date: Thu, 26 Apr 2012 18:38:36 +0000 (-0700)
Subject: model: bugfix - reset the "current_action" after it has been processed
X-Git-Tag: pldi2013~496
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a42f201a4e0553616e34433972b7b719e6c8f24a;p=model-checker.git

model: bugfix - reset the "current_action" after it has been processed

There are executions under which we may call ModelChecker::check_current_action()
twice in a row without an acutal ModelAction (curren_action) being set in
between. This causes the previous action to be queued twice in our trace
listing.

This can be solved 2 ways:
(1) set current_action to NULL after processing it
(2) move all calls to check_current_action() under the THREAD_READY codepath,
    so that we guarantee that some Thread pushed an Action back to the
    model-checking system

I do both.
---

diff --git a/model.cc b/model.cc
index 9d23788..82e6520 100644
--- a/model.cc
+++ b/model.cc
@@ -197,6 +197,7 @@ void ModelChecker::check_current_action(void)
 		DEBUG("trying to push NULL action...\n");
 		return;
 	}
+	current_action = NULL;
 	nextThread = advance_backtracking_state();
 	next->set_node(currentNode);
 	set_backtracking(next);
diff --git a/threads.cc b/threads.cc
index 47a211c..917090f 100644
--- a/threads.cc
+++ b/threads.cc
@@ -121,11 +121,11 @@ static int thread_system_next(void)
 	Thread *curr, *next;
 
 	curr = thread_current();
-	model->check_current_action();
 	if (curr) {
-		if (curr->get_state() == THREAD_READY)
+		if (curr->get_state() == THREAD_READY) {
+			model->check_current_action();
 			model->scheduler->add_thread(curr);
-		else if (curr->get_state() == THREAD_RUNNING)
+		} else if (curr->get_state() == THREAD_RUNNING)
 			/* Stopped while running; i.e., completed */
 			curr->complete();
 		else