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.
Node *currnode;
ModelAction *curr = this->current_action;
Node *currnode;
ModelAction *curr = this->current_action;
current_action = NULL;
if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
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) {
/* Assign 'creation' parent */
if (curr->get_type() == THREAD_CREATE) {
ASSERT(!node_list.empty());
if (get_head()->has_been_explored(act->get_tid())) {
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++;
+ 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()
}
Node * NodeStack::get_head()