bug fix

diff --git a/model.cc b/model.cc
index 33d8e15..c2de313 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -423,7 +423,6 @@ void ModelChecker::finishRunExecution(Thread *old)
 void ModelChecker::consumeAction()
 {
        ModelAction *curr = chosen_thread->get_pending();
 void ModelChecker::consumeAction()
 {
        ModelAction *curr = chosen_thread->get_pending();

-       Thread * th = thread_current();

        chosen_thread->set_pending(NULL);
        chosen_thread = execution->take_step(curr);
 }
        chosen_thread->set_pending(NULL);
        chosen_thread = execution->take_step(curr);
 }


@@ -463,6 +462,8 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        }
        DBG();
        Thread *old = thread_current();
        }
        DBG();
        Thread *old = thread_current();

+       old->set_state(THREAD_READY);
+

        ASSERT(!old->get_pending());
 
        if (inspect_plugin != NULL) {
        ASSERT(!old->get_pending());
 
        if (inspect_plugin != NULL) {

diff --git a/threads.cc b/threads.cc
index 9316031..942d183 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -333,7 +333,6 @@ int Thread::swap(ucontext_t *ctxt, Thread *t)
 
 int Thread::swap(Thread *t, Thread *t2)
 {
 
 int Thread::swap(Thread *t, Thread *t2)
 {

-       t->set_state(THREAD_READY);

        t2->set_state(THREAD_RUNNING);
        if (t == t2)
                return 0;
        t2->set_state(THREAD_RUNNING);
        if (t == t2)
                return 0;