model: bugfix - reset the "current_action" after it has been processed

There are executions under which we may call ModelChecker::check_current_action()
twice in a row without an acutal ModelAction (curren_action) being set in
between. This causes the previous action to be queued twice in our trace
listing.

This can be solved 2 ways:
(1) set current_action to NULL after processing it
(2) move all calls to check_current_action() under the THREAD_READY codepath,
    so that we guarantee that some Thread pushed an Action back to the
    model-checking system

I do both.

diff --git a/model.cc b/model.cc
index 9d23788e8939746cd8bf720e2c8ece25e46f8ae7..82e65202510076338130dea1d51488e52fa1b720 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -197,6 +197,7 @@ void ModelChecker::check_current_action(void)
                DEBUG("trying to push NULL action...\n");
                return;
        }
+       current_action = NULL;
        nextThread = advance_backtracking_state();
        next->set_node(currentNode);
        set_backtracking(next);

diff --git a/threads.cc b/threads.cc
index 47a211c20fe37ea25bf2536dc26cbbc520437291..917090fb71500665009e1c5d4d0e50d3de729e06 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -121,11 +121,11 @@ static int thread_system_next(void)
        Thread *curr, *next;
 
        curr = thread_current();
-       model->check_current_action();
        if (curr) {
-               if (curr->get_state() == THREAD_READY)
+               if (curr->get_state() == THREAD_READY) {
+                       model->check_current_action();
                        model->scheduler->add_thread(curr);
-               else if (curr->get_state() == THREAD_RUNNING)
+               } else if (curr->get_state() == THREAD_RUNNING)
                        /* Stopped while running; i.e., completed */
                        curr->complete();
                else