Index: kernel/generic/src/synch/waitq.c
===================================================================
--- kernel/generic/src/synch/waitq.c	(revision 3954961e3244230c1f7f8570256342938778edb5)
+++ kernel/generic/src/synch/waitq.c	(revision 200373928c6b0d2d85f0afee8d1fa4db29c2c656)
@@ -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);
 }