From: Brian Norris <banorris@uci.edu>
Date: Mon, 28 May 2012 19:20:01 +0000 (-0700)
Subject: nodestack: compute parent ModelAction externally
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e725e347266a91be41447dba497f57f3b6d5413c;p=c11tester.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 86d28ec0..42f412f4 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 1d2bc964..2eba02cf 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 cf3c6db1..af780822 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();