schedule: do not allow model-checker thread to enter scheduler

diff --git a/schedule.cc b/schedule.cc
index cca60ebfba45795252c4e3de97d1223b934aa0f4..dd35237b22232df0744e22baadaaceb54ae6affd 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -48,6 +48,7 @@ bool Scheduler::is_enabled(Thread *t) const
 void Scheduler::add_thread(Thread *t)
 {
        DEBUG("thread %d\n", id_to_int(t->get_id()));
+       ASSERT(!t->is_model_thread());
        set_enabled(t, THREAD_ENABLED);
 }
 
@@ -79,6 +80,7 @@ void Scheduler::sleep(Thread *t)
  */
 void Scheduler::wake(Thread *t)
 {
+       ASSERT(!t->is_model_thread());
        set_enabled(t, THREAD_DISABLED);
        t->set_state(THREAD_READY);
 }
@@ -106,6 +108,9 @@ Thread * Scheduler::next_thread(Thread *t)
                                return NULL;
                        }
                }
+       } else if (t->is_model_thread()) {
+               /* model-checker threads never run */
+               t = NULL;
        } else {
                curr_thread_index = id_to_int(t->get_id());
        }
@@ -120,6 +125,7 @@ Thread * Scheduler::next_thread(Thread *t)
  */
 Thread * Scheduler::get_current_thread() const
 {
+       ASSERT(!current || !current->is_model_thread());
        return current;
 }