diff --git a/base-hw/src/core/kernel.cc b/base-hw/src/core/kernel.cc
index 3391405e8..550545e69 100644
--- a/base-hw/src/core/kernel.cc
+++ b/base-hw/src/core/kernel.cc
@@ -57,6 +57,15 @@ namespace Kernel
 	 */
 	static void idle_main() { while (1) ; }
 
+	Pd_ids * pd_ids() { return unsynchronized_singleton<Pd_ids>(); }
+	Thread_ids * thread_ids() { return unsynchronized_singleton<Thread_ids>(); }
+	Signal_context_ids * signal_context_ids() { return unsynchronized_singleton<Signal_context_ids>(); }
+	Signal_receiver_ids * signal_receiver_ids() { return unsynchronized_singleton<Signal_receiver_ids>(); }
+
+	Pd_pool * pd_pool() { return unsynchronized_singleton<Pd_pool>(); }
+	Thread_pool * thread_pool() { return unsynchronized_singleton<Thread_pool>(); }
+	Signal_context_pool * signal_context_pool() { return unsynchronized_singleton<Signal_context_pool>(); }
+	Signal_receiver_pool * signal_receiver_pool() { return unsynchronized_singleton<Signal_receiver_pool>(); }
 
 	/**
 	 * Access to static kernel timer
@@ -91,7 +100,14 @@ namespace Kernel
 
 namespace Kernel
 {
-	class Vm : public Object<Vm, MAX_VMS>,
+	class Vm;
+	typedef Id_allocator<MAX_VMS> Vm_ids;
+	typedef Object_pool<Vm>       Vm_pool;
+
+	Vm_ids  * vm_ids();
+	Vm_pool * vm_pool();
+
+	class Vm : public Object<Vm, MAX_VMS, vm_ids, vm_pool>,
 	           public Execution_context
 	{
 		private:
@@ -139,6 +155,8 @@ namespace Kernel
 			void proceed() { mtc()->continue_vm(_state); }
 	};
 
+	Vm_ids * vm_ids() { return unsynchronized_singleton<Vm_ids>(); }
+	Vm_pool * vm_pool() { return unsynchronized_singleton<Vm_pool>(); }
 
 	/**
 	 * Access to static CPU scheduler
diff --git a/base-hw/src/core/kernel/object.h b/base-hw/src/core/kernel/object.h
index 3c8f82eb8..2b2b018c6 100644
--- a/base-hw/src/core/kernel/object.h
+++ b/base-hw/src/core/kernel/object.h
@@ -47,8 +47,16 @@ namespace Kernel
 
 	/**
 	 * Make all objects of a deriving class findable through unique IDs
+	 *
+	 * \param T              object type
+	 * \param MAX_INSTANCES  max amount of coincidently living objects
+	 * \param ID_ALLOC       accessor function of object-name allocator
+	 * \param POOL           accessor function of object pool
 	 */
-	template <typename T, unsigned MAX_INSTANCES>
+	template <typename T, unsigned MAX_INSTANCES,
+	          Id_allocator<MAX_INSTANCES> * (*ID_ALLOC)(),
+	          Kernel::Object_pool<T> * (* POOL)()>
+
 	class Object;
 }
 
@@ -190,21 +198,12 @@ class Kernel::Id_allocator
 		}
 };
 
-template <typename T, unsigned MAX_INSTANCES>
+template <typename T, unsigned MAX_INSTANCES,
+          Kernel::Id_allocator<MAX_INSTANCES> * (* ID_ALLOC)(),
+          Kernel::Object_pool<T> * (* POOL)()>
+
 class Kernel::Object : public Object_pool<T>::Item
 {
-	private :
-
-		class Id_allocator : public Kernel::Id_allocator<MAX_INSTANCES> { };
-
-		/**
-		 * Unique-ID allocator for objects of T
-		 */
-		static Id_allocator * _id_allocator()
-		{
-			return unsynchronized_singleton<Id_allocator>();
-		}
-
 	public:
 
 		typedef Object_pool<T> Pool;
@@ -212,16 +211,16 @@ class Kernel::Object : public Object_pool<T>::Item
 		/**
 		 * Map of unique IDs to objects of T
 		 */
-		static Pool * pool() { return unsynchronized_singleton<Pool>(); }
+		static Pool * pool() { return POOL(); }
 
 	protected:
 
 		/**
 		 * Constructor
 		 */
-		Object() : Pool::Item(_id_allocator()->alloc())
+		Object() : Pool::Item(ID_ALLOC()->alloc())
 		{
-			pool()->insert(static_cast<T *>(this));
+			POOL()->insert(static_cast<T *>(this));
 		}
 
 		/**
@@ -229,8 +228,8 @@ class Kernel::Object : public Object_pool<T>::Item
 		 */
 		~Object()
 		{
-			pool()->remove(static_cast<T *>(this));
-			_id_allocator()->free(Pool::Item::id());
+			POOL()->remove(static_cast<T *>(this));
+			ID_ALLOC()->free(Pool::Item::id());
 		}
 };
 
diff --git a/base-hw/src/core/kernel/pd.h b/base-hw/src/core/kernel/pd.h
index 662d8d35f..9f0e2bd3c 100644
--- a/base-hw/src/core/kernel/pd.h
+++ b/base-hw/src/core/kernel/pd.h
@@ -53,6 +53,12 @@ namespace Kernel
 	 * Kernel backend of protection domains
 	 */
 	class Pd;
+
+	typedef Id_allocator<MAX_PDS> Pd_ids;
+	typedef Object_pool<Pd>       Pd_pool;
+
+	Pd_ids  * pd_ids();
+	Pd_pool * pd_pool();
 }
 
 class Kernel::Mode_transition_control
@@ -138,7 +144,7 @@ class Kernel::Mode_transition_control
 		}
 };
 
-class Kernel::Pd : public Object<Pd, MAX_PDS>
+class Kernel::Pd : public Object<Pd, MAX_PDS, pd_ids, pd_pool>
 {
 	private:
 
diff --git a/base-hw/src/core/kernel/signal_receiver.h b/base-hw/src/core/kernel/signal_receiver.h
index d42c00b85..72d9e51dd 100644
--- a/base-hw/src/core/kernel/signal_receiver.h
+++ b/base-hw/src/core/kernel/signal_receiver.h
@@ -48,6 +48,16 @@ namespace Kernel
 	 * Combines signal contexts to an entity that handlers can listen to
 	 */
 	class Signal_receiver;
+
+	typedef Id_allocator<MAX_SIGNAL_CONTEXTS>  Signal_context_ids;
+	typedef Object_pool<Signal_context>        Signal_context_pool;
+	typedef Id_allocator<MAX_SIGNAL_RECEIVERS> Signal_receiver_ids;
+	typedef Object_pool<Signal_receiver>       Signal_receiver_pool;
+
+	Signal_context_ids   * signal_context_ids();
+	Signal_context_pool  * signal_context_pool();
+	Signal_receiver_ids  * signal_receiver_ids();
+	Signal_receiver_pool * signal_receiver_pool();
 }
 
 class Kernel::Signal_handler
@@ -183,7 +193,8 @@ class Kernel::Signal_receiver_killer
 
 class Kernel::Signal_context
 :
-	public Object<Signal_context, MAX_SIGNAL_CONTEXTS>
+	public Object<Signal_context, MAX_SIGNAL_CONTEXTS,
+	              signal_context_ids, signal_context_pool>
 {
 	friend class Signal_receiver;
 	friend class Signal_context_killer;
@@ -301,7 +312,8 @@ class Kernel::Signal_context
 
 class Kernel::Signal_receiver
 :
-	public Object<Signal_receiver, MAX_SIGNAL_RECEIVERS>,
+	public Object<Signal_receiver, MAX_SIGNAL_RECEIVERS,
+	              signal_receiver_ids, signal_receiver_pool>,
 	public Signal_context_killer
 {
 	friend class Signal_context;
diff --git a/base-hw/src/core/kernel/thread.h b/base-hw/src/core/kernel/thread.h
index 45800c320..a296f6048 100644
--- a/base-hw/src/core/kernel/thread.h
+++ b/base-hw/src/core/kernel/thread.h
@@ -1,5 +1,5 @@
 /*
- * \brief   Kernel backend for userland execution-contexts
+ * \brief   Kernel backend for execution contexts in userland
  * \author  Martin Stein
  * \date    2012-11-30
  */
@@ -57,6 +57,12 @@ namespace Kernel
 	 * Kernel backend for userland execution-contexts
 	 */
 	class Thread;
+
+	typedef Id_allocator<MAX_THREADS> Thread_ids;
+	typedef Object_pool<Thread>       Thread_pool;
+
+	Thread_ids  * thread_ids();
+	Thread_pool * thread_pool();
 }
 
 class Kernel::Execution_context : public Cpu_scheduler::Item
@@ -85,7 +91,7 @@ class Kernel::Execution_context : public Cpu_scheduler::Item
 class Kernel::Thread
 :
 	public Cpu::User_context,
-	public Object<Thread, MAX_THREADS>,
+	public Object<Thread, MAX_THREADS, thread_ids, thread_pool>,
 	public Execution_context,
 	public Ipc_node,
 	public Irq_receiver,
@@ -335,7 +341,7 @@ class Kernel::Thread
 
 			/* join a protection domain */
 			Pd * const pd = Pd::pool()->object(_pd_id);
-			assert(pd)
+			assert(pd);
 			addr_t const tlb = pd->tlb()->base();
 
 			/* initialize CPU context */