Index: kernel/generic/src/proc/scheduler.c
===================================================================
--- kernel/generic/src/proc/scheduler.c	(revision b2fa1204c76e1eaec329888181d281aac04ed61e)
+++ kernel/generic/src/proc/scheduler.c	(revision ee1c2d9cd5399d6bcfa9ffa802a3e8598188074b)
@@ -52,4 +52,6 @@
 #include <atomic.h>
 #include <synch/spinlock.h>
+#include <synch/workqueue.h>
+#include <synch/rcu.h>
 #include <config.h>
 #include <context.h>
@@ -64,4 +66,5 @@
 #include <debug.h>
 #include <stacktrace.h>
+#include <cpu.h>
 
 static void scheduler_separated_stack(void);
@@ -87,4 +90,5 @@
 {
 	before_thread_runs_arch();
+	rcu_before_thread_runs();
 	
 #ifdef CONFIG_FPU_LAZY
@@ -127,4 +131,6 @@
 static void after_thread_ran(void)
 {
+	workq_after_thread_ran();
+	rcu_after_thread_ran();
 	after_thread_ran_arch();
 }
@@ -219,4 +225,6 @@
 		goto loop;
 	}
+
+	ASSERT(!CPU->idle);
 	
 	unsigned int i;
@@ -398,4 +406,5 @@
 	ASSERT((!THREAD) || (irq_spinlock_locked(&THREAD->lock)));
 	ASSERT(CPU != NULL);
+	ASSERT(interrupts_disabled());
 	
 	/*
@@ -421,4 +430,5 @@
 		
 		case Exiting:
+			rcu_thread_exiting();
 repeat:
 			if (THREAD->detached) {