#define INITIAL_THREAD_ID 0
+class Backtrack {
+public:
+ Backtrack(ModelAction *d, action_list_t *t) {
+ diverge = d;
+ actionTrace = t;
+ iter = actionTrace->begin();
+ }
+ ModelAction * get_diverge() { return diverge; }
+ action_list_t * get_trace() { return actionTrace; }
+ void advance_state() { iter++; }
+ ModelAction * get_state() {
+ return iter == actionTrace->end() ? NULL : *iter;
+ }
+private:
+ ModelAction *diverge;
+ action_list_t *actionTrace;
+ /* points to position in actionTrace as we replay */
+ action_list_t::iterator iter;
+};
+
ModelChecker *model;
ModelChecker::ModelChecker()
this->exploring = NULL;
this->nextThread = THREAD_ID_T_NONE;
- rootNode = new TreeNode(NULL);
+ rootNode = new TreeNode();
currentNode = rootNode;
action_trace = new action_list_t();
}
print_summary();
if ((exploring = model->get_next_backtrack()) == NULL)
return false;
- model->reset_to_initial_state();
- nextThread = get_next_replay_thread();
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
exploring->get_diverge()->print();
print_list(exploring->get_trace());
}
+
+ model->reset_to_initial_state();
+ nextThread = get_next_replay_thread();
return true;
}
{
ModelAction *prev;
TreeNode *node;
+ Thread *t = get_thread(act->get_tid());
prev = get_last_conflict(act);
if (prev == NULL)
node = prev->get_node();
+ while (t && !node->is_enabled(t))
+ t = t->get_parent();
+
/* Check if this has been explored already */
- if (node->hasBeenExplored(act->get_tid()))
+ if (node->hasBeenExplored(t->get_id()))
return;
/* If this is a new backtracking point, mark the tree */
- if (node->setBacktrack(act->get_tid()) != 0)
+ if (node->setBacktrack(t->get_id()) != 0)
return;
DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
- prev->get_tid(), act->get_tid());
+ prev->get_tid(), t->get_id());
if (DBG_ENABLED()) {
prev->print();
act->print();
nextThread = advance_backtracking_state();
next->set_node(currentNode);
set_backtracking(next);
- currentNode = currentNode->exploreChild(next->get_tid());
+ currentNode = currentNode->explore_child(next);
this->action_trace->push_back(next);
}