From: Brian Norris <banorris@uci.edu>
Date: Mon, 25 Jun 2012 19:07:39 +0000 (-0700)
Subject: nodestack: re-associate ModelAction/Node relationship
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=87273fd76240454e85a233c34b93463fa681480b;p=c11tester.git

nodestack: re-associate ModelAction/Node relationship

Currently, the Node that is returned by ModelAction::get_node() actually
represents the Node that is parent to the ModelAction. This works well for
some of the backtracking computations (since the backtracking set is held
in the parent Node), but it creates confusion when performing computations
such as the following:

 Node *node;
 ...
 ModelAction *act = node->get_action();
 Node *node2 = act->get_parent();

 ASSERT(node == node2); // Fails
 ASSERT(node->get_parent() == node2); // Succeeds

So this patch changes this behavior so that the first assertion (above)
succeeds and the second one fails. This is probably more desirable in the
long run.
---

diff --git a/model.cc b/model.cc
index 93e06d02..9be04b69 100644
--- a/model.cc
+++ b/model.cc
@@ -124,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
-		Node *node = next->get_node();
+		Node *node = next->get_node()->get_parent();
 
 		/* Reached divergence point */
 		DEBUG("*** Divergence point ***\n");
@@ -196,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	if (prev == NULL)
 		return;
 
-	node = prev->get_node();
+	node = prev->get_node()->get_parent();
 
 	while (!node->is_enabled(t))
 		t = t->get_parent();
@@ -262,7 +262,7 @@ void ModelChecker::check_current_action(void)
 
 	nextThread = get_next_replay_thread();
 
-	currnode = curr->get_node();
+	currnode = curr->get_node()->get_parent();
 
 	if (!currnode->backtrack_empty())
 		if (!next_backtrack || *curr > *next_backtrack)
diff --git a/nodestack.cc b/nodestack.cc
index e7b5f511..d3b7c104 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -3,7 +3,20 @@
 #include "common.h"
 #include "model.h"
 
-/** @brief Node constructor */
+/**
+ * @brief Node constructor
+ *
+ * Constructs a single Node for use in a NodeStack. Each Node is associated
+ * with exactly one ModelAction (exception: the first Node should be created
+ * as an empty stub, to represent the first thread "choice") and up to one
+ * parent.
+ *
+ * @param act The ModelAction to associate with this Node. May be NULL.
+ * @param par The parent Node in the NodeStack. May be NULL if there is no
+ * parent.
+ * @param nthreads The number of threads which exist at this point in the
+ * execution trace.
+ */
 Node::Node(ModelAction *act, Node *par, int nthreads)
 	: action(act),
 	parent(par),
@@ -13,6 +26,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
 	numBacktracks(0),
 	may_read_from()
 {
+	if (act)
+		act->set_node(this);
 }
 
 /** @brief Node desctructor */
@@ -54,14 +69,11 @@ bool Node::backtrack_empty()
 }
 
 /**
- * Explore a child Node using a given ModelAction. This updates both the
- * Node-internal and the ModelAction data to associate the ModelAction with
- * this Node.
- * @param act is the ModelAction to explore
+ * Mark the appropriate backtracking infromation for exploring a thread choice.
+ * @param act The ModelAction to explore
  */
 void Node::explore_child(ModelAction *act)
 {
-	act->set_node(this);
 	explore(act->get_tid());
 }