Index: kernel/generic/src/synch/rcu.c
===================================================================
--- kernel/generic/src/synch/rcu.c	(revision 09737cc97ffcee4a01bd7eaee34d72d7821ae8c6)
+++ kernel/generic/src/synch/rcu.c	(revision 5e5cef3b7bf7f9684a41a5a30a8d2022b309efd7)
@@ -1028,4 +1028,7 @@
 			interrupts_restore(ipl);
 		}
+
+		printf("Bug: thread (id %" PRIu64 " \"%s\") exited while in RCU read"
+			" section.\n", THREAD->tid, THREAD->name);
 	}
 }
@@ -1452,4 +1455,5 @@
 	ASSERT(THREAD->state == Exiting);
 	ASSERT(PREEMPTION_DISABLED || interrupts_disabled());
+	
 	/* 
 	 * The thread forgot to exit its reader critical section. 
@@ -1461,4 +1465,7 @@
 		THREAD->rcu.nesting_cnt = 1;
 		read_unlock_impl(&THREAD->rcu.nesting_cnt);
+
+		printf("Bug: thread (id %" PRIu64 " \"%s\") exited while in RCU read"
+			" section.\n", THREAD->tid, THREAD->name);
 	}
 }
