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.

diff --git a/model.cc b/model.cc
index 86d28ec0bfc4119b16f0c5c0eba62c34d05ea3d5..42f412f421e389267d58d1ce6fba9c6d9fb44cf2 100644 (file)
--- 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 1d2bc9648fc1365d059cceab96490866c3fd2cf5..2eba02cf20c9739e85227c77ac7510fb4cdd4427 100644 (file)
--- 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 cf3c6db146675c0cb7f41d994f988925209fc976..af7808227b420ff431a3549490dc37e55a36fd08 100644 (file)
--- 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();