nodestack: push 'create_cv' functionality responsibility back to ModelChecker

It doesn't really make sense to have NodeStack call the 'create_cv' function
for a ModelAction. This commit separates the functionality of 'explore_action'
from 'create_cv', calling each separately from the higher-level
'check_current_action' model-checking function.

diff --git a/action.cc b/action.cc
index d76796d406c4d22d3642850fd2fcfcdae881b5d0..28d95270a7eb19bec65d136034f13e7615edbdec 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -84,7 +84,9 @@ bool ModelAction::is_dependent(ModelAction *act)
 
 void ModelAction::create_cv(ModelAction *parent)
 {
-       ASSERT(cv == NULL);
+       if (cv)
+               return;
+
        if (parent)
                cv = new ClockVector(parent->cv, this);
        else

diff --git a/model.cc b/model.cc
index 274a2d928102f9d2348114e5085f4781f69fe0b6..2ffa22a1028a8008c1c60e52e8e9fee627fac766 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -211,7 +211,8 @@ void ModelChecker::check_current_action(void)
                return;
        }
 
-       curr = node_stack->explore_action(curr, get_parent_action(curr->get_tid()));
+       curr = node_stack->explore_action(curr);
+       curr->create_cv(get_parent_action(curr->get_tid()));
 
        /* Assign 'creation' parent */
        if (curr->get_type() == THREAD_CREATE) {

diff --git a/nodestack.cc b/nodestack.cc
index 2eba02cf20c9739e85227c77ac7510fb4cdd4427..df5fc633ac37aba0b6df464f51be996ab8403eb6 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -117,7 +117,7 @@ void NodeStack::print()
        printf("............................................\n");
 }
 
-ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
+ModelAction * NodeStack::explore_action(ModelAction *act)
 {
        DBG();
 
@@ -135,7 +135,6 @@ ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
 
                /* Record action */
                get_head()->explore_child(act);
-               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 af7808227b420ff431a3549490dc37e55a36fd08..cf3c6db146675c0cb7f41d994f988925209fc976 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -45,7 +45,7 @@ class NodeStack {
 public:
        NodeStack();
        ~NodeStack();
-       ModelAction * explore_action(ModelAction *act, ModelAction *parent);
+       ModelAction * explore_action(ModelAction *act);
        Node * get_head();
        Node * get_next();
        void reset_execution();