bug fix
authorBrian Demsky <bdemsky@uci.edu>
Sat, 29 Aug 2020 08:11:59 +0000 (01:11 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Sat, 29 Aug 2020 08:11:59 +0000 (01:11 -0700)
model.cc
threads.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();
-       Thread * th = thread_current();
        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();
+       old->set_state(THREAD_READY);
+
        ASSERT(!old->get_pending());
 
        if (inspect_plugin != NULL) {
index 9316031..942d183 100644 (file)
@@ -333,7 +333,6 @@ int Thread::swap(ucontext_t *ctxt, Thread *t)
 
 int Thread::swap(Thread *t, Thread *t2)
 {
-       t->set_state(THREAD_READY);
        t2->set_state(THREAD_RUNNING);
        if (t == t2)
                return 0;