From 94c12b28e9afeed050f40c3d2d625fa0e22f0387 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 20 Apr 2012 10:50:29 -0700
Subject: [PATCH] model: implement, use schedule_next_thread()
Relies on the rest of the model checker to set the next thread; simply returns
the chosen thread.
---
model.cc | 11 +++++++++++
schedule.cc | 6 ++++++
2 files changed, 17 insertions(+)
diff --git a/model.cc b/model.cc
index 4307b39..26fd6ca 100644
--- a/model.cc
+++ b/model.cc
@@ -39,6 +39,17 @@ void ModelChecker::add_system_thread(Thread *t)
this->system_thread = t;
}
+Thread *ModelChecker::schedule_next_thread()
+{
+ Thread *t;
+ if (nextThread == THREAD_ID_T_NONE)
+ return NULL;
+ t = thread_map[nextThread];
+ if (t == NULL)
+ DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+ return t;
+}
+
ModelAction *ModelChecker::get_last_conflict(ModelAction *act)
{
void *loc = act->get_location();
diff --git a/schedule.cc b/schedule.cc
index 0432825..13b640c 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -11,6 +11,12 @@ void Scheduler::add_thread(Thread *t)
Thread *Scheduler::next_thread(void)
{
+ Thread *t = model->schedule_next_thread();
+
+ if (t != NULL) {
+ readyList.remove(t);
+ return t;
+ }
if (readyList.empty())
return NULL;
--
2.34.1