From e725e347266a91be41447dba497f57f3b6d5413c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 28 May 2012 12:20:01 -0700 Subject: [PATCH] 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. --- model.cc | 2 +- nodestack.cc | 4 ++-- nodestack.h | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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(); -- 2.34.1