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 93e06d0262de2b4c4d93bf8c9207f018b710cb3e..9be04b6956cc7ff852a012f3a5b1f98746eebf6d 100644 (file)
--- 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 e7b5f51162b485160f3b4bb20cb06f13df2dc3b6..d3b7c104316161d0268c8ae1b2db7a116fbbac74 100644 (file)
--- 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());
 }