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 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(); -- 2.34.1