From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 20 Jul 2012 19:42:42 +0000 (-0700)
Subject: rmw example works
X-Git-Tag: pldi2013~318
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=84e24d516d4e9dbd30f1fff7e9a185d1540d20eb

rmw example works
---

diff --git a/model.cc b/model.cc
index 59f148e..e18fda1 100644
--- a/model.cc
+++ b/model.cc
@@ -118,7 +118,6 @@ Thread * ModelChecker::schedule_next_thread()
  */
 thread_id_t ModelChecker::get_next_replay_thread()
 {
-	ModelAction *next;
 	thread_id_t tid;
 
 	/* Have we completed exploring the preselected path? */
@@ -126,7 +125,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
 		return THREAD_ID_T_NONE;
 
 	/* Else, we are trying to replay an execution */
-	next = node_stack->get_next()->get_action();
+	ModelAction * next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
 		Node *nextnode = next->get_node();
@@ -308,17 +307,16 @@ void ModelChecker::check_current_action(void)
 	if (!already_added)
 		add_action_to_lists(curr);
 
-	/* Do not split atomic actions. */
-	if (curr->is_rmwr()) {
-		nextThread = thread_current()->get_id();
-		return;
-	}
-
 	/* Is there a better interface for setting the next thread rather
 		 than this field/convoluted approach?  Perhaps like just returning
 		 it or something? */
 
-	nextThread = get_next_replay_thread();
+	/* Do not split atomic actions. */
+	if (curr->is_rmwr()) {
+		nextThread = thread_current()->get_id();
+	} else {
+		nextThread = get_next_replay_thread();
+	}
 
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();