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.
next = node_stack->get_next()->get_action();
if (next == diverge) {
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");
/* Reached divergence point */
DEBUG("*** Divergence point ***\n");
if (prev == NULL)
return;
if (prev == NULL)
return;
- node = prev->get_node();
+ node = prev->get_node()->get_parent();
while (!node->is_enabled(t))
t = t->get_parent();
while (!node->is_enabled(t))
t = t->get_parent();
nextThread = get_next_replay_thread();
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)
if (!currnode->backtrack_empty())
if (!next_backtrack || *curr > *next_backtrack)
#include "common.h"
#include "model.h"
#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),
Node::Node(ModelAction *act, Node *par, int nthreads)
: action(act),
parent(par),
numBacktracks(0),
may_read_from()
{
numBacktracks(0),
may_read_from()
{
+ if (act)
+ act->set_node(this);
}
/** @brief Node desctructor */
}
/** @brief Node desctructor */
- * 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)
{
*/
void Node::explore_child(ModelAction *act)
{
explore(act->get_tid());
}
explore(act->get_tid());
}