Index: libcfa/src/concurrency/kernel.cfa
===================================================================
--- libcfa/src/concurrency/kernel.cfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/kernel.cfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -300,5 +300,5 @@
 	// register the processor unless it's the main thread which is handled in the boot sequence
 	if(this != mainProcessor) {
-		this->id = doregister(this);
+		this->id = doregister((__processor_id_t*)this);
 		ready_queue_grow( this->cltr );
 	}
@@ -346,5 +346,5 @@
 	if(this != mainProcessor) {
 		ready_queue_shrink( this->cltr );
-		unregister(this);
+		unregister((__processor_id_t*)this);
 	}
 	else {
@@ -416,5 +416,5 @@
 		if(unlikely(thrd_dst->preempted != __NO_PREEMPTION)) {
 			// The thread was preempted, reschedule it and reset the flag
-			__schedule_thread( thrd_dst );
+			__schedule_thread( (__processor_id_t*)this, thrd_dst );
 			break RUNNING;
 		}
@@ -609,5 +609,5 @@
 // Scheduler routines
 // KERNEL ONLY
-void __schedule_thread( $thread * thrd ) {
+void __schedule_thread( struct __processor_id_t * id, $thread * thrd ) {
 	/* paranoid */ verify( thrd );
 	/* paranoid */ verify( thrd->state != Halted );
@@ -623,9 +623,9 @@
 	if (thrd->preempted == __NO_PREEMPTION) thrd->state = Ready;
 
-	ready_schedule_lock( kernelTLS.this_processor );
+	ready_schedule_lock  ( id );
 		push( thrd->curr_cluster, thrd );
 
 		__wake_one(thrd->curr_cluster);
-	ready_schedule_unlock( kernelTLS.this_processor );
+	ready_schedule_unlock( id );
 
 	/* paranoid */ verify( ! kernelTLS.preemption_state.enabled );
@@ -636,7 +636,7 @@
 	/* paranoid */ verify( ! kernelTLS.preemption_state.enabled );
 
-	ready_schedule_lock( kernelTLS.this_processor );
+	ready_schedule_lock  ( (__processor_id_t*)kernelTLS.this_processor );
 		$thread * head = pop( this );
-	ready_schedule_unlock( kernelTLS.this_processor );
+	ready_schedule_unlock( (__processor_id_t*)kernelTLS.this_processor );
 
 	/* paranoid */ verify( ! kernelTLS.preemption_state.enabled );
@@ -645,5 +645,5 @@
 
 // KERNEL ONLY unpark with out disabling interrupts
-void __unpark( $thread * thrd __cfaabi_dbg_ctx_param2 ) {
+void __unpark(  struct __processor_id_t * id, $thread * thrd __cfaabi_dbg_ctx_param2 ) {
 	static_assert(sizeof(thrd->state) == sizeof(int));
 
@@ -663,5 +663,5 @@
 			// Wake lost the race,
 			thrd->state = Blocked;
-			__schedule_thread( thrd );
+			__schedule_thread( id, thrd );
 			break;
 		case Rerun:
@@ -681,5 +681,5 @@
 
 	disable_interrupts();
-	__unpark( thrd __cfaabi_dbg_ctx_fwd2 );
+	__unpark( (__processor_id_t*)kernelTLS.this_processor, thrd __cfaabi_dbg_ctx_fwd2 );
 	enable_interrupts( __cfaabi_dbg_ctx );
 }
@@ -798,5 +798,5 @@
 	(*mainProcessor){};
 
-	mainProcessor->id = doregister(mainProcessor);
+	mainProcessor->id = doregister( (__processor_id_t*)mainProcessor);
 
 	//initialize the global state variables
@@ -809,5 +809,5 @@
 	// Add the main thread to the ready queue
 	// once resume is called on mainProcessor->runner the mainThread needs to be scheduled like any normal thread
-	__schedule_thread(mainThread);
+	__schedule_thread((__processor_id_t *)mainProcessor, mainThread);
 
 	// SKULLDUGGERY: Force a context switch to the main processor to set the main thread's context to the current UNIX
@@ -853,5 +853,5 @@
 	kernel_stop_preemption();
 
-	unregister(mainProcessor);
+	unregister((__processor_id_t*)mainProcessor);
 
 	// Destroy the main processor and its context in reverse order of construction
Index: libcfa/src/concurrency/kernel.hfa
===================================================================
--- libcfa/src/concurrency/kernel.hfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/kernel.hfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -47,5 +47,9 @@
 extern struct cluster * mainCluster;
 
-// Processor
+// Processor id, required for scheduling threads
+struct __processor_id_t {
+	unsigned id;
+};
+
 coroutine processorCtx_t {
 	struct processor * proc;
@@ -54,4 +58,6 @@
 // Wrapper around kernel threads
 struct processor {
+	inline __processor_id_t;
+
 	// Main state
 	// Coroutine ctx who does keeps the state of the processor
@@ -60,5 +66,4 @@
 	// Cluster from which to get threads
 	struct cluster * cltr;
-	unsigned int id;
 
 	// Name of the processor
Index: libcfa/src/concurrency/kernel_private.hfa
===================================================================
--- libcfa/src/concurrency/kernel_private.hfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/kernel_private.hfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -25,4 +25,6 @@
 // Scheduler
 
+struct __attribute__((aligned(64))) __scheduler_lock_id_t;
+
 extern "C" {
 	void disable_interrupts() OPTIONAL_THREAD;
@@ -31,5 +33,5 @@
 }
 
-void __schedule_thread( $thread * ) __attribute__((nonnull (1)));
+void __schedule_thread( struct __processor_id_t *, $thread * ) __attribute__((nonnull (2)));
 
 //Block current thread and release/wake-up the following resources
@@ -73,5 +75,5 @@
 
 // KERNEL ONLY unpark with out disabling interrupts
-void __unpark( $thread * thrd __cfaabi_dbg_ctx_param2 );
+void __unpark( struct __processor_id_t *, $thread * thrd __cfaabi_dbg_ctx_param2 );
 
 //-----------------------------------------------------------------------------
@@ -108,6 +110,6 @@
 // Cells use by the reader writer lock
 // while not generic it only relies on a opaque pointer
-struct __attribute__((aligned(64))) __processor_id {
-	processor * volatile handle;
+struct __attribute__((aligned(64))) __scheduler_lock_id_t {
+	__processor_id_t * volatile handle;
 	volatile bool lock;
 };
@@ -115,8 +117,8 @@
 // Lock-Free registering/unregistering of threads
 // Register a processor to a given cluster and get its unique id in return
-unsigned doregister( struct processor * proc );
+unsigned doregister( struct __processor_id_t * proc );
 
 // Unregister a processor from a given cluster using its id, getting back the original pointer
-void     unregister( struct processor * proc );
+void     unregister( struct __processor_id_t * proc );
 
 //=======================================================================
@@ -167,5 +169,5 @@
 
 	// data pointer
-	__processor_id * data;
+	__scheduler_lock_id_t * data;
 };
 
@@ -178,5 +180,5 @@
 // Reader side : acquire when using the ready queue to schedule but not
 //  creating/destroying queues
-static inline void ready_schedule_lock( struct processor * proc) with(*__scheduler_lock) {
+static inline void ready_schedule_lock( struct __processor_id_t * proc) with(*__scheduler_lock) {
 	unsigned iproc = proc->id;
 	/*paranoid*/ verify(data[iproc].handle == proc);
@@ -197,5 +199,5 @@
 }
 
-static inline void ready_schedule_unlock( struct processor * proc) with(*__scheduler_lock) {
+static inline void ready_schedule_unlock( struct __processor_id_t * proc) with(*__scheduler_lock) {
 	unsigned iproc = proc->id;
 	/*paranoid*/ verify(data[iproc].handle == proc);
Index: libcfa/src/concurrency/preemption.cfa
===================================================================
--- libcfa/src/concurrency/preemption.cfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/preemption.cfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -39,5 +39,5 @@
 // FwdDeclarations : timeout handlers
 static void preempt( processor   * this );
-static void timeout( $thread * this );
+static void timeout( struct __processor_id_t * id, $thread * this );
 
 // FwdDeclarations : Signal handlers
@@ -90,5 +90,5 @@
 
 // Tick one frame of the Discrete Event Simulation for alarms
-static void tick_preemption() {
+static void tick_preemption( struct __processor_id_t * id ) {
 	alarm_node_t * node = 0p;							// Used in the while loop but cannot be declared in the while condition
 	alarm_list_t * alarms = &event_kernel->alarms;		// Local copy for ease of reading
@@ -108,5 +108,5 @@
 		}
 		else {
-			timeout( node->thrd );
+			timeout( id, node->thrd );
 		}
 
@@ -268,6 +268,6 @@
 
 // reserved for future use
-static void timeout( $thread * this ) {
-	__unpark( this __cfaabi_dbg_ctx2 );
+static void timeout( struct __processor_id_t * id, $thread * this ) {
+	__unpark( id, this __cfaabi_dbg_ctx2 );
 }
 
@@ -405,4 +405,7 @@
 // Waits on SIGALRM and send SIGUSR1 to whom ever needs it
 static void * alarm_loop( __attribute__((unused)) void * args ) {
+	__processor_id_t id;
+	id.id = doregister(&id);
+
 	// Block sigalrms to control when they arrive
 	sigset_t mask;
@@ -449,5 +452,5 @@
 			// __cfaabi_dbg_print_safe( "Kernel : Preemption thread tick\n" );
 			lock( event_kernel->lock __cfaabi_dbg_ctx2 );
-			tick_preemption();
+			tick_preemption( &id );
 			unlock( event_kernel->lock );
 			break;
@@ -462,4 +465,5 @@
 EXIT:
 	__cfaabi_dbg_print_safe( "Kernel : Preemption thread stopping\n" );
+	unregister(&id);
 	return 0p;
 }
Index: libcfa/src/concurrency/ready_queue.cfa
===================================================================
--- libcfa/src/concurrency/ready_queue.cfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/ready_queue.cfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -74,5 +74,5 @@
 }
 
-void ?{}( __processor_id & this, struct processor * proc ) {
+void ?{}( __scheduler_lock_id_t & this, __processor_id_t * proc ) {
 	this.handle = proc;
 	this.lock   = false;
@@ -81,5 +81,5 @@
 //=======================================================================
 // Lock-Free registering/unregistering of threads
-unsigned doregister( struct processor * proc ) with(*__scheduler_lock) {
+unsigned doregister( struct __processor_id_t * proc ) with(*__scheduler_lock) {
 	__cfadbg_print_safe(ready_queue, "Kernel : Registering proc %p for RW-Lock\n", proc);
 
@@ -89,5 +89,5 @@
 	// Check among all the ready
 	for(uint_fast32_t i = 0; i < s; i++) {
-		processor * null = 0p; // Re-write every loop since compare thrashes it
+		__processor_id_t * null = 0p; // Re-write every loop since compare thrashes it
 		if( __atomic_load_n(&data[i].handle, (int)__ATOMIC_RELAXED) == null
 			&& __atomic_compare_exchange_n( &data[i].handle, &null, proc, false, __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)) {
@@ -106,5 +106,5 @@
 
 	// Step - 3 : Mark space as used and then publish it.
-	__processor_id * storage = (__processor_id *)&data[n];
+	__scheduler_lock_id_t * storage = (__scheduler_lock_id_t *)&data[n];
 	(*storage){ proc };
 	while(true) {
@@ -125,5 +125,5 @@
 }
 
-void unregister( struct processor * proc ) with(*__scheduler_lock) {
+void unregister( struct __processor_id_t * proc ) with(*__scheduler_lock) {
 	unsigned id = proc->id;
 	/*paranoid*/ verify(id < ready);
@@ -188,14 +188,4 @@
 	} before, after;
 
-#if defined(__CFA_WITH_VERIFY__)
-	// id of last processor to acquire the lock
-	// needed only to check for mutual exclusion violations
-	unsigned int last_id;
-
-	// number of items on this list
-	// needed only to check for deadlocks
-	unsigned int count;
-#endif
-
 	// Optional statistic counters
 	#if !defined(__CFA_NO_SCHED_STATS__)
@@ -235,8 +225,4 @@
 void ?{}( __intrusive_lane_t & this ) {
 	this.lock = false;
-	#if defined(__CFA_WITH_VERIFY__)
-		this.last_id = -1u;
-		this.count = 0u;
-	#endif
 
 	this.before.link.prev = 0p;
@@ -279,5 +265,4 @@
 	/* paranoid */ verify(tail(this)->link.next == 0p );
 	/* paranoid */ verify(tail(this)->link.prev == head(this) );
-	/* paranoid */ verify(this.count == 0u );
 }
 
@@ -293,6 +278,4 @@
 		/* paranoid */ verify(head(this)->link.prev == 0p);
 
-		this.count++;
-
 		if(this.before.link.ts == 0l) {
 			/* paranoid */ verify(tail(this)->link.prev == head(this));
@@ -346,9 +329,6 @@
 	$thread * next = node->link.next;
 
-	#if defined(__CFA_WITH_VERIFY__)
-		this.count--;
-		/* paranoid */ verify(node != tail);
-		/* paranoid */ verify(node);
-	#endif
+	/* paranoid */ verify(node != tail);
+	/* paranoid */ verify(node);
 
 	// Do the pop
@@ -637,9 +617,4 @@
 	} while( !__atomic_try_acquire( &lanes.data[i].lock ) );
 
-	#if defined(__CFA_WITH_VERIFY__)
-		/* paranoid */ verify(lanes.data[i].last_id == -1u);
-		/* paranoid */ lanes.data[i].last_id = kernelTLS.this_processor->id;
-	#endif
-
 	bool first = false;
 
@@ -655,10 +630,4 @@
 		arrive( snzi, i );
 	}
-
-	#if defined(__CFA_WITH_VERIFY__)
-		/* paranoid */ verifyf( lanes.data[i].last_id == kernelTLS.this_processor->id, "Expected last processor to lock queue %u to be %u, was %u\n", i, lanes.data[i].last_id, kernelTLS.this_processor->id );
-		/* paranoid */ verifyf( lanes.data[i].lock, "List %u is not locked\n", i );
-		/* paranoid */ lanes.data[i].last_id = -1u;
-	#endif
 
 	// Unlock and return
@@ -698,17 +667,7 @@
 	if( !__atomic_try_acquire(&lane.lock) ) return 0p;
 
-	#if defined(__CFA_WITH_VERIFY__)
-		/* paranoid */ verify(lane.last_id == -1u);
-		/* paranoid */ lane.last_id = kernelTLS.this_processor->id;
-	#endif
-
 
 	// If list is empty, unlock and retry
 	if( is_empty(lane) ) {
-		#if defined(__CFA_WITH_VERIFY__)
-			/* paranoid */ verify(lane.last_id == kernelTLS.this_processor->id);
-			/* paranoid */ lane.last_id = -1u;
-		#endif
-
 		__atomic_unlock(&lane.lock);
 		return 0p;
@@ -721,5 +680,4 @@
 
 	/* paranoid */ verify(thrd);
-	/* paranoid */ verify(lane.last_id == kernelTLS.this_processor->id);
 	/* paranoid */ verify(lane.lock);
 
@@ -728,9 +686,4 @@
 		depart( snzi, w );
 	}
-
-	#if defined(__CFA_WITH_VERIFY__)
-		/* paranoid */ verify(lane.last_id == kernelTLS.this_processor->id);
-		/* paranoid */ lane.last_id = -1u;
-	#endif
 
 	// Unlock and return
@@ -874,12 +827,4 @@
 		^(snzi){};
 
-		// Make sure that the total thread count stays the same
-		#if defined(__CFA_WITH_VERIFY__)
-			size_t nthreads = 0;
-			for( idx; (size_t)lanes.count ) {
-				nthreads += lanes.data[idx].count;
-			}
-		#endif
-
 		size_t ocount = lanes.count;
 		// Check that we have some space left
@@ -940,12 +885,4 @@
 			}
 		}
-
-		// Make sure that the total thread count stayed the same
-		#if defined(__CFA_WITH_VERIFY__)
-			for( idx; (size_t)lanes.count ) {
-				nthreads -= lanes.data[idx].count;
-			}
-			verifyf(nthreads == 0, "Shrinking changed number of threads");
-		#endif
 	}
 
Index: libcfa/src/concurrency/thread.cfa
===================================================================
--- libcfa/src/concurrency/thread.cfa	(revision b388ee817181b3a403189e26e13ce3bdd381cf21)
+++ libcfa/src/concurrency/thread.cfa	(revision 9b1dcc2f454a40116801b690de79c7b7c402765c)
@@ -62,5 +62,5 @@
 	verify( this_thrd->context.SP );
 
-	__schedule_thread(this_thrd);
+	__schedule_thread( (__processor_id_t *)kernelTLS.this_processor, this_thrd);
 	enable_interrupts( __cfaabi_dbg_ctx );
 }