From: Brian Norris <banorris@uci.edu>
Date: Tue, 13 Mar 2012 03:51:25 +0000 (-0700)
Subject: libthreads: perform all scheduling/model-checking from master thread
X-Git-Tag: pldi2013~590
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=9cd547903789a3f025a1063368df509fc935d5f1;p=model-checker.git

libthreads: perform all scheduling/model-checking from master thread

To keep all user-space actions under control, we should perform all scheduling
and model-checking from the main system thread. This pushes some of the
thread_yield() logic to a system function (as desired).
---

diff --git a/libthreads.c b/libthreads.c
index 892d784..4233c0e 100644
--- a/libthreads.c
+++ b/libthreads.c
@@ -61,9 +61,8 @@ int thread_yield(void)
 
 	DBG();
 	old = thread_current();
-	model->scheduler->add_thread(old);
-	next = model->scheduler->next_thread();
-	DEBUG("(%d, %d)\n", old->index, next->index);
+	old->state = THREAD_READY;
+	next = model->system_thread;
 	return thread_swap(old, next);
 }
 
@@ -74,17 +73,38 @@ static void thread_dispose(struct thread *t)
 	stack_free(t->stack);
 }
 
-static void thread_wait_finish(void)
+/*
+ * Return 1 if found next thread, 0 otherwise
+ */
+static int thread_system_next(void)
 {
 	struct thread *curr, *next;
 
+	curr = thread_current();
+	if (curr) {
+		if (curr->state == THREAD_READY)
+			model->scheduler->add_thread(curr);
+		else if (curr->state == THREAD_RUNNING)
+			/* Stopped while running; i.e., completed */
+			thread_dispose(curr);
+		else
+			DEBUG("ERROR: current thread in unexpected state??\n");
+	}
+	next = model->scheduler->next_thread();
+	if (next)
+		next->state = THREAD_RUNNING;
+	DEBUG("(%d, %d)\n", curr ? curr->index : -1, next ? next->index : -1);
+	if (!next)
+		return 1;
+	return thread_swap(model->system_thread, next);
+}
+
+static void thread_wait_finish(void)
+{
+
 	DBG();
 
-	do {
-		if ((curr = thread_current()))
-			thread_dispose(curr);
-		next = model->scheduler->next_thread();
-	} while (next && !thread_swap(model->system_thread, next));
+	while (!thread_system_next());
 }
 
 int thread_create(struct thread *t, void (*start_routine), void *arg)