From eb8e9f61a400856421465d95ac52d9cffed2a491 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 19 Jun 2012 15:44:13 -0700
Subject: [PATCH] nodestack/model: refactor explore_action(), change return
 semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.
---
 model.cc     | 11 +++++++++--
 nodestack.cc | 27 +++++++++++++--------------
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/model.cc b/model.cc
index 0905285..077cc53 100644
--- a/model.cc
+++ b/model.cc
@@ -230,14 +230,21 @@ void ModelChecker::check_current_action(void)
 	Node *currnode;
 
 	ModelAction *curr = this->current_action;
+	ModelAction *tmp;
 	current_action = NULL;
 	if (!curr) {
 		DEBUG("trying to push NULL action...\n");
 		return;
 	}
 
-	curr = node_stack->explore_action(curr);
-	curr->create_cv(get_parent_action(curr->get_tid()));
+	tmp = node_stack->explore_action(curr);
+	if (tmp) {
+		/* Discard duplicate ModelAction */
+		delete curr;
+		curr = tmp;
+	} else {
+		curr->create_cv(get_parent_action(curr->get_tid()));
+	}
 
 	/* Assign 'creation' parent */
 	if (curr->get_type() == THREAD_CREATE) {
diff --git a/nodestack.cc b/nodestack.cc
index e342456..c9878a3 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -150,22 +150,21 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 	ASSERT(!node_list.empty());
 
 	if (get_head()->has_been_explored(act->get_tid())) {
-		/* Discard duplicate ModelAction */
-		delete act;
-		iter++;
-	} else { /* Diverging from previous execution */
-		/* Clear out remainder of list */
-		node_list_t::iterator it = iter;
-		it++;
-		clear_node_list(&node_list, it, node_list.end());
-
-		/* Record action */
-		get_head()->explore_child(act);
-		node_list.push_back(new Node(act, model->get_num_threads()));
-		total_nodes++;
 		iter++;
+		return (*iter)->get_action();
 	}
-	return (*iter)->get_action();
+
+	/* Diverging from previous execution; clear out remainder of list */
+	node_list_t::iterator it = iter;
+	it++;
+	clear_node_list(&node_list, it, node_list.end());
+
+	/* Record action */
+	get_head()->explore_child(act);
+	node_list.push_back(new Node(act, model->get_num_threads()));
+	total_nodes++;
+	iter++;
+	return NULL;
 }
 
 Node * NodeStack::get_head()
-- 
2.34.1