From: Brian Norris <banorris@uci.edu>
Date: Tue, 29 May 2012 17:46:42 +0000 (-0700)
Subject: nodestack: push 'create_cv' functionality responsibility back to ModelChecker
X-Git-Tag: pldi2013~392^2~5
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=9397658596cfa29f81242b5f06e80d1d9cdf6d14

nodestack: push 'create_cv' functionality responsibility back to ModelChecker

It doesn't really make sense to have NodeStack call the 'create_cv' function
for a ModelAction. This commit separates the functionality of 'explore_action'
from 'create_cv', calling each separately from the higher-level
'check_current_action' model-checking function.
---

diff --git a/action.cc b/action.cc
index d76796d..28d9527 100644
--- a/action.cc
+++ b/action.cc
@@ -84,7 +84,9 @@ bool ModelAction::is_dependent(ModelAction *act)
 
 void ModelAction::create_cv(ModelAction *parent)
 {
-	ASSERT(cv == NULL);
+	if (cv)
+		return;
+
 	if (parent)
 		cv = new ClockVector(parent->cv, this);
 	else
diff --git a/model.cc b/model.cc
index 274a2d9..2ffa22a 100644
--- a/model.cc
+++ b/model.cc
@@ -211,7 +211,8 @@ void ModelChecker::check_current_action(void)
 		return;
 	}
 
-	curr = node_stack->explore_action(curr, get_parent_action(curr->get_tid()));
+	curr = node_stack->explore_action(curr);
+	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 2eba02c..df5fc63 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -117,7 +117,7 @@ void NodeStack::print()
 	printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
+ModelAction * NodeStack::explore_action(ModelAction *act)
 {
 	DBG();
 
@@ -135,7 +135,6 @@ ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
 
 		/* Record action */
 		get_head()->explore_child(act);
-		act->create_cv(parent);
 		node_list.push_back(new Node(act, model->get_num_threads()));
 		iter++;
 	}
diff --git a/nodestack.h b/nodestack.h
index af78082..cf3c6db 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -45,7 +45,7 @@ class NodeStack {
 public:
 	NodeStack();
 	~NodeStack();
-	ModelAction * explore_action(ModelAction *act, ModelAction *parent);
+	ModelAction * explore_action(ModelAction *act);
 	Node * get_head();
 	Node * get_next();
 	void reset_execution();