From: Brian Norris <banorris@uci.edu>
Date: Wed, 12 Sep 2012 02:48:38 +0000 (-0700)
Subject: threads, model, schedule: refactor thread joining
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=2cd14a2ba5f68a5bd35c1094c9d5a83891b483f8;p=c11tester.git

threads, model, schedule: refactor thread joining

The Thread can hold a list of ModelAction (instead of Threads) that are waiting
for its completion. This will give the exiting Thread a better ability to
handle the event.

This also deletes Scheduler::wait, since it is no superceded by Scheduler::sleep.
---

diff --git a/model.cc b/model.cc
index cb7e43f0..4f29e21b 100644
--- a/model.cc
+++ b/model.cc
@@ -360,17 +360,20 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		break;
 	}
 	case THREAD_JOIN: {
-		Thread *wait, *join;
-		wait = get_thread(curr);
-		join = (Thread *)curr->get_location();
-		if (!join->is_complete())
-			scheduler->wait(wait, join);
+		Thread *waiting, *blocking;
+		waiting = get_thread(curr);
+		blocking = (Thread *)curr->get_location();
+		if (!blocking->is_complete()) {
+			blocking->push_wait_list(curr);
+			scheduler->sleep(waiting);
+		}
 		break;
 	}
 	case THREAD_FINISH: {
 		Thread *th = get_thread(curr);
 		while (!th->wait_list_empty()) {
-			Thread *wake = th->pop_wait_list();
+			ModelAction *act = th->pop_wait_list();
+			Thread *wake = get_thread(act);
 			scheduler->wake(wake);
 		}
 		th->complete();
diff --git a/schedule.cc b/schedule.cc
index 9063fdb4..cbb4957a 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -31,20 +31,6 @@ void Scheduler::remove_thread(Thread *t)
 		readyList.remove(t);
 }
 
-/**
- * Force one Thread to wait on another Thread. The "join" Thread should
- * eventually wake up the waiting Thread via Scheduler::wake.
- * @param wait The Thread that should wait
- * @param join The Thread on which we are waiting.
- */
-void Scheduler::wait(Thread *wait, Thread *join)
-{
-	ASSERT(!join->is_complete());
-	remove_thread(wait);
-	join->push_wait_list(wait);
-	wait->set_state(THREAD_BLOCKED);
-}
-
 /**
  * Prevent a Thread from being scheduled. The sleeping Thread should be
  * re-awoken via Scheduler::wake.
diff --git a/schedule.h b/schedule.h
index 7875e0b6..a7483e02 100644
--- a/schedule.h
+++ b/schedule.h
@@ -18,7 +18,6 @@ public:
 	Scheduler();
 	void add_thread(Thread *t);
 	void remove_thread(Thread *t);
-	void wait(Thread *wait, Thread *join);
 	void sleep(Thread *t);
 	void wake(Thread *t);
 	Thread * next_thread(Thread *t);
diff --git a/threads.h b/threads.h
index 248d948f..87a21ef2 100644
--- a/threads.h
+++ b/threads.h
@@ -79,17 +79,17 @@ public:
 	bool wait_list_empty() { return wait_list.empty(); }
 
 	/**
-	 * Add a thread to the waiting list for this thread.
-	 * @param t The Thread to add
+	 * Add a ModelAction to the waiting list for this thread.
+	 * @param t The ModelAction to add. Must be a JOIN.
 	 */
-	void push_wait_list(Thread *t) { wait_list.push_back(t); }
+	void push_wait_list(ModelAction *act) { wait_list.push_back(act); }
 
 	/**
-	 * Remove one Thread from the waiting list
-	 * @return The Thread that was removed from the waiting list
+	 * Remove one ModelAction from the waiting list
+	 * @return The ModelAction that was removed from the waiting list
 	 */
-	Thread * pop_wait_list() {
-		Thread *ret = wait_list.front();
+	ModelAction * pop_wait_list() {
+		ModelAction *ret = wait_list.front();
 		wait_list.pop_back();
 		return ret;
 	}
@@ -111,11 +111,11 @@ private:
 	thread_state state;
 
 	/**
-	 * A list of Threads waiting on this Thread. Particularly, this list is
-	 * used for thread joins, where another Thread waits for this Thread to
-	 * complete
+	 * A list of ModelActions waiting on this Thread. Particularly, this
+	 * list is used for thread joins, where another Thread waits for this
+	 * Thread to complete
 	 */
-	std::vector<Thread *> wait_list;
+	std::vector<ModelAction *> wait_list;
 
 	/**
 	 * The value returned by the last action in this thread