diff --git a/base-hw/src/core/kernel/kernel.cc b/base-hw/src/core/kernel/kernel.cc
index b7916a918..5dc32cbb1 100644
--- a/base-hw/src/core/kernel/kernel.cc
+++ b/base-hw/src/core/kernel/kernel.cc
@@ -277,12 +277,28 @@ extern "C" void init_kernel_multiprocessor()
  */
 extern "C" void kernel()
 {
+	/* ensure that no other processor accesses kernel data while we do */
 	data_lock().lock();
+
+	/* determine local processor scheduler */
 	unsigned const processor_id = Processor::executing_id();
 	Processor * const processor = processor_pool()->select(processor_id);
 	Processor_scheduler * const scheduler = processor->scheduler();
-	scheduler->head()->exception(processor_id);
-	scheduler->head()->proceed(processor_id);
+
+	/*
+	 * Request the current processor occupant without any update. While this
+	 * processor was outside the kernel, another processor may have changed the
+	 * scheduling of the local activities in a way that an update would return
+	 * an occupant other than that whose exception caused the kernel entry.
+	 */
+	scheduler->occupant()->exception(processor_id);
+
+	/*
+	 * The processor local as well as remote exception-handling may have
+	 * changed the scheduling of the local activities. Hence we must update the
+	 * processor occupant.
+	 */
+	scheduler->update_occupant()->proceed(processor_id);
 }
 
 
diff --git a/base-hw/src/core/kernel/scheduler.cc b/base-hw/src/core/kernel/scheduler.cc
index 508616e63..46cd4dfaa 100644
--- a/base-hw/src/core/kernel/scheduler.cc
+++ b/base-hw/src/core/kernel/scheduler.cc
@@ -37,7 +37,7 @@ void Kernel::Execution_context::_interrupt(unsigned const processor_id)
 		if (timer()->interrupt_id(processor_id) == irq_id)
 		{
 			/* handle scheduling timeout */
-			__processor->scheduler()->yield();
+			__processor->scheduler()->yield_occupation();
 			timer()->clear_interrupt(processor_id);
 			reset_lap_time(processor_id);
 		} else {
@@ -65,5 +65,5 @@ void Kernel::Execution_context::_unschedule()
 
 void Kernel::Execution_context::_yield()
 {
-	__processor->scheduler()->yield();
+	__processor->scheduler()->yield_occupation();
 }
diff --git a/base-hw/src/core/kernel/scheduler.h b/base-hw/src/core/kernel/scheduler.h
index 9853fa19a..2b1a97065 100644
--- a/base-hw/src/core/kernel/scheduler.h
+++ b/base-hw/src/core/kernel/scheduler.h
@@ -240,7 +240,7 @@ class Kernel::Scheduler
 	protected:
 
 		T * const      _idle;
-		T *            _current;
+		T *            _occupant;
 		Double_list<T> _items[Priority::MAX + 1];
 
 	public:
@@ -250,27 +250,29 @@ class Kernel::Scheduler
 		/**
 		 * Constructor
 		 */
-		Scheduler(T * const idle) : _idle(idle), _current(0) { }
+		Scheduler(T * const idle) : _idle(idle), _occupant(0) { }
 
 		/**
-		 * Get currently scheduled item
+		 * Adjust occupant reference to the current scheduling plan
+		 *
+		 * \return  updated occupant reference
 		 */
-		T * head()
+		T * update_occupant()
 		{
 			for (int i = Priority::MAX; i >= 0 ; i--) {
-				_current = _items[i].head();
-				if (_current) return _current;
+				_occupant = _items[i].head();
+				if (_occupant) { return _occupant; }
 			}
 			return _idle;
 		}
 
 		/**
-		 * End turn of currently scheduled item
+		 * Adjust scheduling plan to the fact that the current occupant yileds
 		 */
-		void yield()
+		void yield_occupation()
 		{
-			if (!_current) return;
-			_items[_current->priority()].head_to_tail();
+			if (!_occupant) { return; }
+			_items[_occupant->priority()].head_to_tail();
 		}
 
 		/**
@@ -292,6 +294,8 @@ class Kernel::Scheduler
 		 ** Accessors **
 		 ***************/
 
+		T * occupant() { return _occupant ? _occupant : _idle; }
+
 		T * idle() const { return _idle; }
 };