From 30999f20b8426081e676adfc76d1c4af7b941e8e Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Sun, 24 Feb 2013 20:59:46 -0800 Subject: [PATCH] fix scheduling stuff to get nice round robin scheduler behavior... --- model.cc | 2 ++ schedule.cc | 6 +++++- schedule.h | 2 ++ 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index ae37889..7fdc824 100644 --- a/model.cc +++ b/model.cc @@ -282,6 +282,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) earliest_diverge = prevnode->get_action(); } } + /* Start the round robin scheduler from this thread id */ + scheduler->set_scheduler_thread(tid); /* The correct sleep set is in the parent node. */ execute_sleep_set(); diff --git a/schedule.cc b/schedule.cc index e874903..8d44eec 100644 --- a/schedule.cc +++ b/schedule.cc @@ -207,6 +207,10 @@ Thread * Scheduler::select_next_thread() return NULL; } +void Scheduler::set_scheduler_thread(thread_id_t tid) { + curr_thread_index=id_to_int(tid); +} + /** * @brief Set the current "running" Thread * @param t Thread to run @@ -215,7 +219,7 @@ void Scheduler::set_current_thread(Thread *t) { ASSERT(t && !t->is_model_thread()); - curr_thread_index = id_to_int(t->get_id()); + // curr_thread_index = id_to_int(t->get_id()); current = t; if (DBG_ENABLED()) diff --git a/schedule.h b/schedule.h index 121da08..6ae2d2b 100644 --- a/schedule.h +++ b/schedule.h @@ -39,6 +39,8 @@ public: bool is_enabled(const Thread *t) const; bool is_enabled(thread_id_t tid) const; bool is_sleep_set(const Thread *t) const; + void set_scheduler_thread(thread_id_t tid); + SNAPSHOTALLOC private: -- 2.34.1