From: Brian Norris <banorris@uci.edu>
Date: Fri, 20 Apr 2012 17:50:29 +0000 (-0700)
Subject: model: implement, use schedule_next_thread()
X-Git-Tag: pldi2013~528
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=94c12b28e9afeed050f40c3d2d625fa0e22f0387;p=model-checker.git

model: implement, use schedule_next_thread()

Relies on the rest of the model checker to set the next thread; simply returns
the chosen thread.
---

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;