Index: libcfa/src/concurrency/invoke.h
===================================================================
--- libcfa/src/concurrency/invoke.h	(revision 4fa44e709bfb1dc5336916a9c723d0d31fece21d)
+++ libcfa/src/concurrency/invoke.h	(revision 1b143ded4ae1e7c2af89dc3d277840dae5225d9a)
@@ -166,5 +166,5 @@
 		struct $thread * next;
 		struct $thread * prev;
-		unsigned long long ts;
+		volatile unsigned long long ts;
 	};
 
Index: libcfa/src/concurrency/io.cfa
===================================================================
--- libcfa/src/concurrency/io.cfa	(revision 4fa44e709bfb1dc5336916a9c723d0d31fece21d)
+++ libcfa/src/concurrency/io.cfa	(revision 1b143ded4ae1e7c2af89dc3d277840dae5225d9a)
@@ -357,5 +357,5 @@
 					// The thread was preempted and now it is on the ready queue
 					/* paranoid */ verify( thrd.state == Active );           // The thread better be in this state
-					/* paranoid */ verify( thrd.next == 1p );                // The thread should be the last on the list
+					/* paranoid */ verify( thrd.next != 0p );                // The thread should be the last on the list
 					/* paranoid */ verify( this.ready_queue.head == &thrd ); // The thread should be the only thing on the list
 
Index: libcfa/src/concurrency/monitor.cfa
===================================================================
--- libcfa/src/concurrency/monitor.cfa	(revision 4fa44e709bfb1dc5336916a9c723d0d31fece21d)
+++ libcfa/src/concurrency/monitor.cfa	(revision 1b143ded4ae1e7c2af89dc3d277840dae5225d9a)
@@ -907,5 +907,5 @@
 	// For each thread in the entry-queue
 	for(	$thread ** thrd_it = &entry_queue.head;
-		*thrd_it;
+		(*thrd_it) != 1p;
 		thrd_it = &(*thrd_it)->link.next
 	) {
Index: libcfa/src/concurrency/ready_queue.cfa
===================================================================
--- libcfa/src/concurrency/ready_queue.cfa	(revision 4fa44e709bfb1dc5336916a9c723d0d31fece21d)
+++ libcfa/src/concurrency/ready_queue.cfa	(revision 1b143ded4ae1e7c2af89dc3d277840dae5225d9a)
@@ -15,5 +15,5 @@
 
 #define __cforall_thread__
-#define __CFA_DEBUG_PRINT_READY_QUEUE__
+// #define __CFA_DEBUG_PRINT_READY_QUEUE__
 
 #include "bits/defs.hfa"
@@ -112,8 +112,8 @@
 // Helpers used by extract
 // (_mask_bitsidx() & X) returns a bit index valid for a __cfa_readyQ_mask_t, where X is any integer
-static inline __cfa_readyQ_mask_t _mask_bitsidx () { return (8 * sizeof(__cfa_readyQ_mask_t)) - 1; }
+static inline __cfa_readyQ_mask_t _mask_bitsidx () __attribute__ ((const)) { return (8 * sizeof(__cfa_readyQ_mask_t)) - 1; }
 
 // (X >> _mask_shiftidx()) retuns an index into an array of __cfa_readyQ_mask_t
-static inline __cfa_readyQ_mask_t _mask_shiftidx() { return (8 * sizeof(__cfa_readyQ_mask_t)) - __builtin_clzl(_mask_bitsidx()); }
+static inline __cfa_readyQ_mask_t _mask_shiftidx() __attribute__ ((const)) { return (8 * sizeof(__cfa_readyQ_mask_t)) - __builtin_clzl(_mask_bitsidx()); }
 
 
@@ -121,6 +121,6 @@
 // Given an index into the large mask, returns the bit index and which __cfa_readyQ_mask_t index in the array
 static inline [__cfa_readyQ_mask_t, __cfa_readyQ_mask_t] extract(__cfa_readyQ_mask_t idx) {
-	__cfa_readyQ_mask_t word = idx >> _mask_bitsidx();
-	__cfa_readyQ_mask_t bit  = idx &  _mask_shiftidx();
+	__cfa_readyQ_mask_t word = idx >> _mask_shiftidx();
+	__cfa_readyQ_mask_t bit  = idx &  _mask_bitsidx();
 	return [bit, word];
 }
@@ -188,5 +188,5 @@
 	}
 
-	__cfadbg_print_safe(ready_queue, "Kernel : Registering proc %p done, id %u\n", proc, n);
+	__cfadbg_print_safe(ready_queue, "Kernel : Registering proc %p done, id %lu\n", proc, n);
 
 	// Return new spot.
@@ -304,6 +304,6 @@
 	/* paranoid */ verifyf(((intptr_t)(&this) % 128) == 0, "Expected address to be aligned %p %% 128 == %zd", &this, ((intptr_t)(&this) % 128));
 
-	/* paranoid */ verifyf(_mask_shiftidx() == 6 , "%zu", _mask_shiftidx());
-	/* paranoid */ verifyf(_mask_bitsidx () == 63, "%zu", _mask_bitsidx());
+	/* paranoid */ verifyf(_mask_shiftidx() == 6 , "%llu", _mask_shiftidx());
+	/* paranoid */ verifyf(_mask_bitsidx () == 63, "%llu", _mask_bitsidx());
 }
 
@@ -422,5 +422,5 @@
 // Check whether or not list is empty
 static inline bool is_empty(__intrusive_lane_t & this) {
-	verify( (this.before.link.ts == 0) == (this.count == 0) );
+	// Cannot verify here since it may not be locked
 	return this.before.link.ts == 0;
 }
@@ -428,5 +428,5 @@
 // Return the timestamp
 static inline unsigned long long ts(__intrusive_lane_t & this) {
-	verify( this.before.link.ts == this.before.link.next->link.ts );
+	// Cannot verify here since it may not be locked
 	return this.before.link.ts;
 }
@@ -520,4 +520,6 @@
 	[bit, word] = extract(index);
 
+	__cfadbg_print_safe(ready_queue, "Kernel : Ready queue extracted index %u as [bit %llu, word %llu]\n", index, bit, word);
+
 	// Conditional check
 	verifyf(
@@ -552,5 +554,5 @@
 	// Conditional check
 	verifyf(
-		strict == STRICT && // Conditional check if it was expected to be set
+		strict != STRICT || // Conditional check if it was expected to be set
 		((mask[word] & (1ull << bit)) != 0),
 		"Before clear %llu:%llu (%u), %llx & %llx", word, bit, index, mask[word], (1ull << bit)
@@ -562,5 +564,5 @@
 	// Conditional check
 	verifyf(
-		strict == STRICT && // Conditional check if it was expected to be cleared
+		strict != STRICT || // Conditional check if it was expected to be cleared
 		ret,
 		"Bit was set but btr returned false"
@@ -576,4 +578,6 @@
 //-----------------------------------------------------------------------
 __attribute__((hot)) bool push(struct cluster * cltr, struct $thread * thrd) with (cltr->ready_queue) {
+	__cfadbg_print_safe(ready_queue, "Kernel : Pushing %p on cluster %p (mask %llu)\n", thrd, cltr, used.mask[0]);
+
 	// write timestamp
 	thrd->link.ts = rdtscl();
@@ -605,4 +609,7 @@
 	// If this lane used to be empty we need to do more
 	if(lane_first) {
+		// Update the bit mask
+		mask_set((__cfa_readyQ_mask_t *)used.mask, i, STRICT);
+
 		// Update the global count
 		size_t ret = __atomic_fetch_add( &used.count, 1z, __ATOMIC_SEQ_CST);
@@ -610,7 +617,4 @@
 		// Check if the entire queue used to be empty
 		first = (ret == 0);
-
-		// Update the bit mask
-		mask_set((__cfa_readyQ_mask_t *)used.mask, i, STRICT);
 	}
 
@@ -624,4 +628,6 @@
 	// Unlock and return
 	__atomic_unlock( &lanes.data[i].lock );
+
+	__cfadbg_print_safe(ready_queue, "Kernel : Pushed %p on cluster %p (idx: %u, mask %llu, first %d)\n", thrd, cltr, i, used.mask[0], lane_first);
 
 	// Update statistics
@@ -807,8 +813,9 @@
 
 				if(sl.before.link.ts == 0l) {
-					assert(tail(sl)->link.next == 0p);
 					assert(tail(sl)->link.prev == head(sl));
 					assert(head(sl)->link.next == tail(sl));
-					assert(head(sl)->link.prev == 0p);
+				} else {
+					assert(tail(sl)->link.prev != head(sl));
+					assert(head(sl)->link.next != tail(sl));
 				}
 			}
@@ -917,5 +924,5 @@
 		for( idx; (size_t)lanes.count ~ ocount) {
 			// Lock is not strictly needed but makes checking invariants much easier
-			bool locked = __atomic_try_acquire(&lanes.data[idx].lock);
+			__attribute__((unused)) bool locked = __atomic_try_acquire(&lanes.data[idx].lock);
 			verify(locked);