From: Brian Norris <banorris@uci.edu>
Date: Tue, 24 Apr 2012 03:09:45 +0000 (-0700)
Subject: schedule: reset scheduler when thread is removed
X-Git-Tag: pldi2013~514
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d48c1867f8e5b2a3f9695a6bc8f1b5394dcda8e7;p=model-checker.git

schedule: reset scheduler when thread is removed

Ensure that the 'current' thread reference is removed properly.
---

diff --git a/model.cc b/model.cc
index f50b0f9..4f87da3 100644
--- a/model.cc
+++ b/model.cc
@@ -205,6 +205,11 @@ int ModelChecker::add_thread(Thread *t)
 	return 0;
 }
 
+void ModelChecker::remove_thread(Thread *t)
+{
+	scheduler->remove_thread(t);
+}
+
 int ModelChecker::switch_to_master(ModelAction *act)
 {
 	Thread *old, *next;
diff --git a/model.h b/model.h
index 64d052f..ca1de85 100644
--- a/model.h
+++ b/model.h
@@ -79,6 +79,7 @@ public:
 	Thread * schedule_next_thread();
 
 	int add_thread(Thread *t);
+	void remove_thread(Thread *t);
 	Thread * get_thread(thread_id_t tid) { return thread_map[tid]; }
 
 	int get_next_id();
diff --git a/schedule.cc b/schedule.cc
index 67b40ec..c9a1ce1 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -9,6 +9,14 @@ void Scheduler::add_thread(Thread *t)
 	readyList.push_back(t);
 }
 
+void Scheduler::remove_thread(Thread *t)
+{
+	if (current == t)
+		current = NULL;
+	else
+		readyList.remove(t);
+}
+
 Thread * Scheduler::next_thread(void)
 {
 	Thread *t = model->schedule_next_thread();
diff --git a/schedule.h b/schedule.h
index 86e4e40..c633b28 100644
--- a/schedule.h
+++ b/schedule.h
@@ -9,6 +9,7 @@
 class Scheduler {
 public:
 	void add_thread(Thread *t);
+	void remove_thread(Thread *t);
 	Thread * next_thread(void);
 	Thread * get_current_thread(void);
 	void print();