Index: generic/src/synch/waitq.c
===================================================================
--- generic/src/synch/waitq.c	(revision 14df080724e02282967a019d3c0e3f89cd15fe7e)
+++ generic/src/synch/waitq.c	(revision 0b917dd28d314c00d3923a555097a34f1ab80fbd)
@@ -100,7 +100,6 @@
 		t->saved_context = t->sleep_timeout_context;
 		do_wakeup = true;
-		
+		t->sleep_queue = NULL;
 		spinlock_unlock(&wq->lock);
-		t->sleep_queue = NULL;
 	}
 	
@@ -155,7 +154,6 @@
 		t->saved_context = t->sleep_interruption_context;
 		do_wakeup = true;
-		
+		t->sleep_queue = NULL;
 		spinlock_unlock(&wq->lock);
-		t->sleep_queue = NULL;
 	}
 	spinlock_unlock(&t->lock);
@@ -419,6 +417,23 @@
 	t = list_get_instance(wq->head.next, thread_t, wq_link);
 	
+	/*
+	 * Lock the thread prior to removing it from the wq.
+	 * This is not necessary because of mutual exclusion
+	 * (the link belongs to the wait queue), but because
+	 * of synchronization with waitq_timeouted_sleep()
+	 * and waitq_interrupt_sleep().
+	 *
+	 * In order for these two functions to work, the following
+	 * invariant must hold:
+	 *
+	 * t->sleep_queue != NULL <=> t sleeps in a wait queue
+	 *
+	 * For an observer who locks the thread, the invariant
+	 * holds only when the lock is held prior to removing
+	 * it from the wait queue.
+	 */
+	spinlock_lock(&t->lock);
 	list_remove(&t->wq_link);
-	spinlock_lock(&t->lock);
+	
 	if (t->timeout_pending && timeout_unregister(&t->sleep_timeout))
 		t->timeout_pending = false;