bugfix - set backtrack events according to an *enabled* thread

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index c829312166033342c8c8d077f0ec2acd63c33230..e3238258a3aa86b0570ff8ed8159eb62e27a899c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -8,6 +8,26 @@
 
 #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()
@@ -23,7 +43,7 @@ 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();
 }
@@ -108,18 +128,27 @@ thread_id_t ModelChecker::advance_backtracking_state()
 
        /* Else, we are trying to replay an execution */
        exploring->advance_state();
-       if (exploring->get_state() == NULL)
-               DEBUG("*** error: reached end of backtrack trace\n");
+
+       ASSERT(exploring->get_state() != NULL);
 
        return get_next_replay_thread();
 }
 
 bool ModelChecker::next_execution()
 {
+       DBG();
+
        num_executions++;
        print_summary();
        if ((exploring = model->get_next_backtrack()) == NULL)
                return false;
+
+       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;
@@ -153,6 +182,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
        ModelAction *prev;
        TreeNode *node;
+       Thread *t = get_thread(act->get_tid());
 
        prev = get_last_conflict(act);
        if (prev == NULL)
@@ -160,15 +190,18 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
        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();
@@ -200,25 +233,31 @@ void ModelChecker::check_current_action(void)
        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);
 }
 
 void ModelChecker::print_summary(void)
 {
-       action_list_t::iterator it;
-
        printf("\n");
-       printf("---------------------------------------------------------------------\n");
        printf("Number of executions: %d\n", num_executions);
-       printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
+       printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
 
        scheduler->print();
 
-       printf("Trace:\n\n");
+       print_list(action_trace);
+       printf("\n");
+
+}
+
+void ModelChecker::print_list(action_list_t *list)
+{
+       action_list_t::iterator it;
+
+       printf("---------------------------------------------------------------------\n");
+       printf("Trace:\n");
 
-       for (it = action_trace->begin(); it != action_trace->end(); it++) {
-               DBG();
+       for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
        }
        printf("---------------------------------------------------------------------\n");