From: Brian Norris <banorris@uci.edu>
Date: Mon, 28 May 2012 19:20:01 +0000 (-0700)
Subject: nodestack: compute parent ModelAction externally
X-Git-Tag: pldi2013~392^2~12
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e725e347266a91be41447dba497f57f3b6d5413c;p=model-checker.git

nodestack: compute parent ModelAction externally

For a particular ModelAction, the 'parent' may be the last action in the
current thread, or otherwise, the action in the parent thread that created the
current thread. This calculation is not suitable for within the NodeStack (and
the current implementation is wrong, taking the last action performed by *any*
thread as the parent). Thus, I set up the method calls to pass the 'parent' to
explore_action() and leave the details to further work.
---

diff --git a/model.cc b/model.cc
index 86d28ec..42f412f 100644
--- a/model.cc
+++ b/model.cc
@@ -209,7 +209,7 @@ void ModelChecker::check_current_action(void)
 		return;
 	}
 
-	curr = node_stack->explore_action(curr);
+	curr = node_stack->explore_action(curr, NULL);
 	nextThread = get_next_replay_thread();
 
 	currnode = curr->get_node();
diff --git a/nodestack.cc b/nodestack.cc
index 1d2bc96..2eba02c 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -117,7 +117,7 @@ void NodeStack::print()
 	printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act)
+ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
 {
 	DBG();
 
@@ -135,7 +135,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
 		/* Record action */
 		get_head()->explore_child(act);
-		act->create_cv(get_head()->get_action());
+		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 cf3c6db..af78082 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -45,7 +45,7 @@ class NodeStack {
 public:
 	NodeStack();
 	~NodeStack();
-	ModelAction * explore_action(ModelAction *act);
+	ModelAction * explore_action(ModelAction *act, ModelAction *parent);
 	Node * get_head();
 	Node * get_next();
 	void reset_execution();