Index: libcfa/src/concurrency/kernel.cfa
===================================================================
--- libcfa/src/concurrency/kernel.cfa	(revision 6fafda8b82ee096d785c1ff4fba1f1abe4f14324)
+++ libcfa/src/concurrency/kernel.cfa	(revision 7d0ebd0d86c0a2ccd570dafa35c3f322a749ff2d)
@@ -142,16 +142,4 @@
 extern void __disable_interrupts_hard();
 extern void __enable_interrupts_hard();
-
-static inline void __disable_interrupts_checked() {
-	/* paranoid */ verify( __preemption_enabled() );
-	disable_interrupts();
-	/* paranoid */ verify( ! __preemption_enabled() );
-}
-
-static inline void __enable_interrupts_checked( bool poll = true ) {
-	/* paranoid */ verify( ! __preemption_enabled() );
-	enable_interrupts( poll );
-	/* paranoid */ verify( __preemption_enabled() );
-}
 
 
@@ -776,12 +764,13 @@
 // Unconditionnaly wake a thread
 void __wake_proc(processor * this) {
+	/* paranoid */ verify( ! __preemption_enabled() );
+
 	__cfadbg_print_safe(runtime_core, "Kernel : waking Processor %p\n", this);
 
-	__disable_interrupts_checked();
-		/* paranoid */ verify( ! __preemption_enabled() );
-		eventfd_t val;
-		val = 1;
-		eventfd_write( this->idle_fd, val );
-	__enable_interrupts_checked();
+	eventfd_t val;
+	val = 1;
+	eventfd_write( this->idle_fd, val );
+
+	/* paranoid */ verify( ! __preemption_enabled() );
 }
 
Index: libcfa/src/concurrency/kernel/startup.cfa
===================================================================
--- libcfa/src/concurrency/kernel/startup.cfa	(revision 6fafda8b82ee096d785c1ff4fba1f1abe4f14324)
+++ libcfa/src/concurrency/kernel/startup.cfa	(revision 7d0ebd0d86c0a2ccd570dafa35c3f322a749ff2d)
@@ -279,5 +279,7 @@
 	// When its coroutine terminates, it return control to the mainThread
 	// which is currently here
+	/* paranoid */ verify( !__atomic_load_n(&mainProcessor->do_terminate, __ATOMIC_ACQUIRE) );
 	__atomic_store_n(&mainProcessor->do_terminate, true, __ATOMIC_RELEASE);
+	__wake_proc( mainProcessor );
 	__kernel_last_resume( __cfaabi_tls.this_processor );
 	mainThread->self_cor.state = Halted;
@@ -564,13 +566,14 @@
 extern size_t __page_size;
 void ^?{}(processor & this) with( this ){
-	if( ! __atomic_load_n(&do_terminate, __ATOMIC_ACQUIRE) ) {
-		__cfadbg_print_safe(runtime_core, "Kernel : core %p signaling termination\n", &this);
-
-		__atomic_store_n(&do_terminate, true, __ATOMIC_RELAXED);
+	/* paranoid */ verify( !__atomic_load_n(&do_terminate, __ATOMIC_ACQUIRE) );
+	__cfadbg_print_safe(runtime_core, "Kernel : core %p signaling termination\n", &this);
+
+	__atomic_store_n(&do_terminate, true, __ATOMIC_RELAXED);
+	__disable_interrupts_checked();
 		__wake_proc( &this );
-
-		wait( terminated );
-		/* paranoid */ verify( active_processor() != &this);
-	}
+	__enable_interrupts_checked();
+
+	wait( terminated );
+	/* paranoid */ verify( active_processor() != &this);
 
 	__destroy_pthread( kernel_thread, this.stack, 0p );
Index: libcfa/src/concurrency/kernel_private.hfa
===================================================================
--- libcfa/src/concurrency/kernel_private.hfa	(revision 6fafda8b82ee096d785c1ff4fba1f1abe4f14324)
+++ libcfa/src/concurrency/kernel_private.hfa	(revision 7d0ebd0d86c0a2ccd570dafa35c3f322a749ff2d)
@@ -60,4 +60,16 @@
 extern bool __preemption_enabled();
 
+static inline void __disable_interrupts_checked() {
+	/* paranoid */ verify( __preemption_enabled() );
+	disable_interrupts();
+	/* paranoid */ verify( ! __preemption_enabled() );
+}
+
+static inline void __enable_interrupts_checked( bool poll = true ) {
+	/* paranoid */ verify( ! __preemption_enabled() );
+	enable_interrupts( poll );
+	/* paranoid */ verify( __preemption_enabled() );
+}
+
 //release/wake-up the following resources
 void __thread_finish( thread$ * thrd );