From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Sep 2012 20:08:46 +0000 (-0700)
Subject: model: check_current_action returns its 'nextThread'
X-Git-Tag: pldi2013~241
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=10676ed8e2c04c76d410efc9ffe4cb49b9462f57

model: check_current_action returns its 'nextThread'

To begin some code structure rearrangements, I make check_current_action()
return the 'nextThread' value as a true return value. Eventually, the
nextThread field might not be needed, and the model-checker behavior might make
more sense...
---

diff --git a/model.cc b/model.cc
index c306f0e..866bc94 100644
--- a/model.cc
+++ b/model.cc
@@ -244,15 +244,11 @@ ModelAction * ModelChecker::get_next_backtrack()
 	return next;
 }
 
-void ModelChecker::check_current_action(void)
+Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
-	ModelAction *curr = this->current_action;
 	bool already_added = false;
-	this->current_action = NULL;
-	if (!curr) {
-		DEBUG("trying to push NULL action...\n");
-		return;
-	}
+
+	ASSERT(curr);
 
 	if (curr->is_rmwc() || curr->is_rmw()) {
 		ModelAction *tmp = process_rmw(curr);
@@ -332,16 +328,6 @@ void ModelChecker::check_current_action(void)
 	if (!already_added)
 		add_action_to_lists(curr);
 
-	/** @todo Is there a better interface for setting the next thread rather
-		 than this field/convoluted approach?  Perhaps like just returning
-		 it or something? */
-
-	/* Do not split atomic actions. */
-	if (curr->is_rmwr())
-		nextThread = thread_current();
-	else
-		nextThread = get_next_replay_thread();
-
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
@@ -351,6 +337,12 @@ void ModelChecker::check_current_action(void)
 			next_backtrack = curr;
 
 	set_backtracking(curr);
+
+	/* Do not split atomic actions. */
+	if (curr->is_rmwr())
+		return thread_current();
+	else
+		return get_next_replay_thread();
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -962,7 +954,10 @@ bool ModelChecker::take_step() {
 	curr = thread_current();
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
-			check_current_action();
+			if (current_action) {
+				nextThread = check_current_action(current_action);
+				current_action = NULL;
+			}
 			scheduler->add_thread(curr);
 		} else if (curr->get_state() == THREAD_RUNNING) {
 			/* Stopped while running; i.e., completed */
diff --git a/model.h b/model.h
index bc827fa..e55863d 100644
--- a/model.h
+++ b/model.h
@@ -82,7 +82,7 @@ private:
 	 * @param act The ModelAction created by the user-thread action
 	 */
 	void set_current_action(ModelAction *act) { current_action = act; }
-	void check_current_action();
+	Thread * check_current_action(ModelAction *curr);
 
 	bool take_step();