From a42f201a4e0553616e34433972b7b719e6c8f24a Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 26 Apr 2012 11:38:36 -0700 Subject: [PATCH] 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. --- model.cc | 1 + threads.cc | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 9d23788e..82e65202 100644 --- 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 47a211c2..917090fb 100644 --- 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 -- 2.34.1