nodestack/model: refactor explore_action(), change return semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.

diff --git a/model.cc b/model.cc
index 090528500e4d11c20ed63f852738b290c43559dd..077cc53ea9cd252365214cb2a424a0da8476002b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -230,14 +230,21 @@ void ModelChecker::check_current_action(void)
        Node *currnode;
 
        ModelAction *curr = this->current_action;
+       ModelAction *tmp;
        current_action = NULL;
        if (!curr) {
                DEBUG("trying to push NULL action...\n");
                return;
        }
 
-       curr = node_stack->explore_action(curr);
-       curr->create_cv(get_parent_action(curr->get_tid()));
+       tmp = node_stack->explore_action(curr);
+       if (tmp) {
+               /* Discard duplicate ModelAction */
+               delete curr;
+               curr = tmp;
+       } else {
+               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 e342456c7bc74d856d3844f1aad5bc1d11acb5c1..c9878a339ec384febedaa95385e31cac478cc169 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -150,22 +150,21 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        ASSERT(!node_list.empty());
 
        if (get_head()->has_been_explored(act->get_tid())) {
-               /* Discard duplicate ModelAction */
-               delete act;
-               iter++;
-       } else { /* Diverging from previous execution */
-               /* Clear out remainder of list */
-               node_list_t::iterator it = iter;
-               it++;
-               clear_node_list(&node_list, it, node_list.end());
-
-               /* Record action */
-               get_head()->explore_child(act);
-               node_list.push_back(new Node(act, model->get_num_threads()));
-               total_nodes++;
                iter++;
+               return (*iter)->get_action();
        }
-       return (*iter)->get_action();
+
+       /* Diverging from previous execution; clear out remainder of list */
+       node_list_t::iterator it = iter;
+       it++;
+       clear_node_list(&node_list, it, node_list.end());
+
+       /* Record action */
+       get_head()->explore_child(act);
+       node_list.push_back(new Node(act, model->get_num_threads()));
+       total_nodes++;
+       iter++;
+       return NULL;
 }
 
 Node * NodeStack::get_head()