Index: kernel/generic/include/synch/waitq.h
===================================================================
--- kernel/generic/include/synch/waitq.h	(revision 497bd656d30dfa5181c542cab4d9d1807cbe1bbd)
+++ kernel/generic/include/synch/waitq.h	(revision 9fe9d296d25d20339552aebcfe9b776a1bf262f8)
@@ -77,5 +77,4 @@
 extern void waitq_sleep_finish(waitq_t *, int, ipl_t);
 extern void waitq_wakeup(waitq_t *, wakeup_mode_t);
-extern void waitq_complete_wakeup(waitq_t *);
 extern void _waitq_wakeup_unsafe(waitq_t *, wakeup_mode_t);
 extern void waitq_interrupt_sleep(struct thread *);
Index: kernel/generic/src/synch/rcu.c
===================================================================
--- kernel/generic/src/synch/rcu.c	(revision 497bd656d30dfa5181c542cab4d9d1807cbe1bbd)
+++ kernel/generic/src/synch/rcu.c	(revision 9fe9d296d25d20339552aebcfe9b776a1bf262f8)
@@ -492,5 +492,4 @@
 	_rcu_call(expedite, &completion.rcu_item, synch_complete);
 	waitq_sleep(&completion.wq);
-	waitq_complete_wakeup(&completion.wq);
 }
 
Index: kernel/generic/src/synch/spinlock.c
===================================================================
--- kernel/generic/src/synch/spinlock.c	(revision 497bd656d30dfa5181c542cab4d9d1807cbe1bbd)
+++ kernel/generic/src/synch/spinlock.c	(revision 9fe9d296d25d20339552aebcfe9b776a1bf262f8)
@@ -199,7 +199,6 @@
  *
  * @param lock    IRQ spinlock to be locked.
- * @param irq_dis If true, interrupts are actually disabled
- *                prior locking the spinlock. If false, interrupts
- *                are expected to be already disabled.
+ * @param irq_dis If true, disables interrupts before locking the spinlock.
+ *                If false, interrupts are expected to be already disabled.
  *
  */
Index: kernel/generic/src/synch/waitq.c
===================================================================
--- kernel/generic/src/synch/waitq.c	(revision 497bd656d30dfa5181c542cab4d9d1807cbe1bbd)
+++ kernel/generic/src/synch/waitq.c	(revision 9fe9d296d25d20339552aebcfe9b776a1bf262f8)
@@ -57,4 +57,6 @@
 
 static void waitq_sleep_timed_out(void *);
+static void waitq_complete_wakeup(waitq_t *);
+
 
 /** Initialize wait queue
@@ -330,4 +332,18 @@
 		break;
 	default:
+		/* 
+		 * Wait for a waitq_wakeup() or waitq_unsleep() to complete
+		 * before returning from waitq_sleep() to the caller. Otherwise
+		 * the caller might expect that the wait queue is no longer used 
+		 * and deallocate it (although the wakeup on a another cpu has 
+		 * not yet completed and is using the wait queue). 
+		 * 
+		 * Note that we have to do this for ESYNCH_OK_BLOCKED and
+		 * ESYNCH_INTERRUPTED, but not necessarily for ESYNCH_TIMEOUT
+		 * where the timeout handler stops using the waitq before waking 
+		 * us up. To be on the safe side, ensure the waitq is not in use 
+		 * anymore in this case as well.
+		 */
+		waitq_complete_wakeup(wq);
 		break;
 	}
@@ -357,5 +373,5 @@
 	} else {
 		if (PARAM_NON_BLOCKING(flags, usec)) {
-			/* Return immediatelly instead of going to sleep */
+			/* Return immediately instead of going to sleep */
 			return ESYNCH_WOULD_BLOCK;
 		}
@@ -448,4 +464,6 @@
  * exits. It returns immediately if there are no concurrent wakeups 
  * at the time.
+ * 
+ * Interrupts must be disabled.
  * 
  * Example usage:
@@ -466,7 +484,9 @@
  *     // callback() completed its work, but it may still be accessing 
  *     // wq in waitq_wakeup(). Therefore it is not yet safe to return 
- *     // or it would clobber up our stack (where wq is stored).
- *     waitq_complete_wakeup(&wq);
- *     // waitq_wakeup() is complete, it is safe to free wq.
+ *     // from waitq_sleep() or it would clobber up our stack (where wq 
+ *     // is stored). waitq_sleep() ensures the wait queue is no longer
+ *     // in use by invoking waitq_complete_wakeup() internally.
+ *     
+ *     // waitq_sleep() returned, it is safe to free wq.
  * }
  * @endcode
@@ -474,8 +494,10 @@
  * @param wq  Pointer to a wait queue.
  */
-void waitq_complete_wakeup(waitq_t *wq)
-{
-	irq_spinlock_lock(&wq->lock, true);
-	irq_spinlock_unlock(&wq->lock, true);
+static void waitq_complete_wakeup(waitq_t *wq)
+{
+	ASSERT(interrupts_disabled());
+	
+	irq_spinlock_lock(&wq->lock, false);
+	irq_spinlock_unlock(&wq->lock, false);
 }