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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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();