diff --git a/repos/base-hw/lib/mk/arm/core.inc b/repos/base-hw/lib/mk/arm/core.inc
index d5c2e369a..59c5af3f7 100644
--- a/repos/base-hw/lib/mk/arm/core.inc
+++ b/repos/base-hw/lib/mk/arm/core.inc
@@ -11,6 +11,7 @@ INC_DIR += $(REP_DIR)/src/core/include/spec/arm
 SRC_CC += spec/arm/kernel/thread_base.cc
 SRC_CC += spec/arm/kernel/thread.cc
 SRC_CC += spec/arm/kernel/cpu.cc
+SRC_CC += spec/arm/kernel/pd.cc
 SRC_CC += spec/arm/platform_support.cc
 
 # add assembly sources
diff --git a/repos/base-hw/lib/mk/cortex_a15/core.inc b/repos/base-hw/lib/mk/cortex_a15/core.inc
index 749ebeeac..2acb22b08 100644
--- a/repos/base-hw/lib/mk/cortex_a15/core.inc
+++ b/repos/base-hw/lib/mk/cortex_a15/core.inc
@@ -8,5 +8,8 @@
 INC_DIR += $(REP_DIR)/src/core/include/spec/cortex_a15
 INC_DIR += $(REP_DIR)/src/core/include/spec/arm_gic
 
+# add C++ sources
+SRC_CC += spec/cortex_a15/cpu.cc
+
 # include less specific configuration
 include $(REP_DIR)/lib/mk/arm_v7/core.inc
diff --git a/repos/base-hw/lib/mk/x86/core.inc b/repos/base-hw/lib/mk/x86/core.inc
index 3c30ad66e..3d82c5d67 100644
--- a/repos/base-hw/lib/mk/x86/core.inc
+++ b/repos/base-hw/lib/mk/x86/core.inc
@@ -12,6 +12,8 @@ INC_DIR += $(REP_DIR)/src/core/include/spec/x86
 SRC_CC += spec/x86/platform_support.cc
 SRC_CC += spec/x86/kernel/thread.cc
 SRC_CC += spec/x86/kernel/cpu.cc
+SRC_CC += spec/x86/kernel/pd.cc
+SRC_CC += spec/x86/cpu.cc
 SRC_CC += kernel/vm_thread.cc
 SRC_CC += x86/io_port_session_component.cc
 SRC_CC += x86/platform_services.cc
diff --git a/repos/base-hw/src/core/include/kernel/configuration.h b/repos/base-hw/src/core/include/kernel/configuration.h
index 6df1870f9..3d882c6d8 100644
--- a/repos/base-hw/src/core/include/kernel/configuration.h
+++ b/repos/base-hw/src/core/include/kernel/configuration.h
@@ -18,11 +18,7 @@ namespace Kernel
 {
 	enum {
 		DEFAULT_STACK_SIZE   = 16 * 1024,
-		MAX_PDS              = 256,
-		MAX_THREADS          = 256,
-		MAX_SIGNAL_RECEIVERS = 2048,
-		MAX_SIGNAL_CONTEXTS  = 4096,
-		MAX_VMS              = 4,
+		MAX_KERNEL_OBJECTS   = 8192,
 	};
 
 	/* amount of priority bands amongst quota owners in CPU scheduling */
diff --git a/repos/base-hw/src/core/include/kernel/object.h b/repos/base-hw/src/core/include/kernel/object.h
index 2f391087e..9a18a7048 100644
--- a/repos/base-hw/src/core/include/kernel/object.h
+++ b/repos/base-hw/src/core/include/kernel/object.h
@@ -1,11 +1,12 @@
 /*
  * \brief   Objects that are findable through unique IDs
  * \author  Martin Stein
+ * \author  Stefan Kalkowski
  * \date    2012-11-30
  */
 
 /*
- * Copyright (C) 2012-2013 Genode Labs GmbH
+ * Copyright (C) 2012-2015 Genode Labs GmbH
  *
  * This file is part of the Genode OS framework, which is distributed
  * under the terms of the GNU General Public License version 2.
@@ -16,16 +17,14 @@
 
 /* Genode includes */
 #include <util/avl_tree.h>
-#include <base/printf.h>
+#include <util/bit_allocator.h>
 
 /* core includes */
 #include <assert.h>
+#include <kernel/configuration.h>
 
 namespace Kernel
 {
-	template <typename T> class Avl_tree : public Genode::Avl_tree<T> { };
-	template <typename T> class Avl_node : public Genode::Avl_node<T> { };
-
 	/**
 	 * Map unique sortable IDs to objects
 	 *
@@ -36,29 +35,17 @@ namespace Kernel
 
 	/**
 	 * Manage allocation of a static set of IDs
-	 *
-	 * \param SIZE  amount of allocatable IDs
 	 */
-	template <unsigned SIZE>
-	class Id_allocator;
+	using Id_allocator = Genode::Bit_allocator<MAX_KERNEL_OBJECTS>;
+	Id_allocator & id_alloc();
 
 	/**
 	 * 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
-	 *
-	 * FIXME: Most of the bother with template parameters regarding ID
-	 *        allocator and object pool is caused by the use of
-	 *        unsynchronized singletons. By avoiding the use of
-	 *        unsynchronized singletons one can at least remove
-	 *        ID_ALLOC_T.
+	 * \param T object type
+	 * \param POOL accessor function of object pool
 	 */
-	template <typename T, unsigned MAX_INSTANCES, typename ID_ALLOC_T,
-	          ID_ALLOC_T * (*ID_ALLOC)(), Kernel::Object_pool<T> * (* POOL)()>
-
+	template <typename T, Kernel::Object_pool<T> * (* POOL)()>
 	class Object;
 }
 
@@ -94,11 +81,11 @@ class Kernel::Object_pool
 
 	private:
 
-		Avl_tree<Item> _tree;
+		Genode::Avl_tree<Item> _tree;
 };
 
 template <typename T>
-class Kernel::Object_pool<T>::Item : public Avl_node<Item>
+class Kernel::Object_pool<T>::Item : public Genode::Avl_node<Item>
 {
 	protected:
 
@@ -117,7 +104,8 @@ class Kernel::Object_pool<T>::Item : public Avl_node<Item>
 		Item * find(unsigned const object_id)
 		{
 			if (object_id == id()) { return this; }
-			Item * const subtree = Avl_node<Item>::child(object_id > id());
+			Item * const subtree =
+				Genode::Avl_node<Item>::child(object_id > id());
 			if (!subtree) { return 0; }
 			return subtree->find(object_id);
 		}
@@ -135,79 +123,13 @@ class Kernel::Object_pool<T>::Item : public Avl_node<Item>
 		bool higher(Item * i) const { return i->id() > id(); }
 };
 
-template <unsigned SIZE>
-class Kernel::Id_allocator
-{
-	private:
-
-		enum {
-			MIN = 1,
-			MAX = MIN + SIZE - 1
-		};
-
-		bool     _free[MAX + 1];
-		unsigned _free_id;
-
-		/**
-		 * Return wether 'id' is a valid ID
-		 */
-		bool _valid_id(unsigned const id) const
-		{
-			return id >= MIN && id <= MAX;
-		}
-
-	public:
-
-		/**
-		 * Constructor
-		 */
-		Id_allocator() : _free_id(MIN)
-		{
-			/* free all IDs */
-			for (unsigned i = MIN; i <= MAX; i++) { _free[i] = 1; }
-		}
-
-		/**
-		 * Allocate a free ID
-		 *
-		 * \return  ID that has been allocated by the call
-		 */
-		unsigned alloc()
-		{
-			/* FIXME: let userland donate RAM to avoid out of mem */
-			if (!_valid_id(_free_id)) {
-				PERR("failed to allocate ID");
-				while (1) { }
-			}
-			/* allocate _free_id */
-			_free[_free_id] = 0;
-			unsigned const id = _free_id;
-
-			/* update _free_id */
-			_free_id++;
-			for (; _free_id <= MAX && !_free[_free_id]; _free_id++) { }
-			return id;
-		}
-
-		/**
-		 * Free ID 'id'
-		 */
-		void free(unsigned const id)
-		{
-			assert(_valid_id(id));
-			_free[id] = 1;
-			if (id < _free_id) { _free_id = id; }
-		}
-};
-
-template <typename T, unsigned MAX_INSTANCES, typename ID_ALLOC_T,
-          ID_ALLOC_T * (* ID_ALLOC)(), Kernel::Object_pool<T> * (* POOL)()>
 
+template <typename T, Kernel::Object_pool<T> * (* POOL)()>
 class Kernel::Object : public Object_pool<T>::Item
 {
 	public:
 
-		typedef Object_pool<T> Pool;
+		using Pool = Object_pool<T>;
 
 		/**
 		 * Map of unique IDs to objects of T
@@ -216,21 +138,13 @@ class Kernel::Object : public Object_pool<T>::Item
 
 	protected:
 
-		/**
-		 * Constructor
-		 */
-		Object() : Pool::Item(ID_ALLOC()->alloc())
-		{
-			POOL()->insert(static_cast<T *>(this));
-		}
+		Object() : Pool::Item(id_alloc().alloc()) {
+			POOL()->insert(static_cast<T *>(this)); }
 
-		/**
-		 * Destructor
-		 */
 		~Object()
 		{
 			POOL()->remove(static_cast<T *>(this));
-			ID_ALLOC()->free(Pool::Item::id());
+			id_alloc().free(Pool::Item::id());
 		}
 };
 
diff --git a/repos/base-hw/src/core/include/kernel/pd.h b/repos/base-hw/src/core/include/kernel/pd.h
index 52650e99d..b9c4b8dee 100644
--- a/repos/base-hw/src/core/include/kernel/pd.h
+++ b/repos/base-hw/src/core/include/kernel/pd.h
@@ -21,7 +21,6 @@
 
 /* core includes */
 #include <kernel/early_translations.h>
-#include <kernel/configuration.h>
 #include <kernel/object.h>
 #include <kernel/cpu.h>
 #include <assert.h>
@@ -97,10 +96,8 @@ namespace Kernel
 	 */
 	class Pd;
 
-	class Pd_ids : public Id_allocator<MAX_PDS> { };
 	typedef Object_pool<Pd> Pd_pool;
 
-	Pd_ids  * pd_ids();
 	Pd_pool * pd_pool();
 
 	Lock & data_lock();
@@ -221,7 +218,8 @@ class Kernel::Mode_transition_control
 		 }
 } __attribute__((aligned(Mode_transition_control::ALIGN)));
 
-class Kernel::Pd : public Object<Pd, MAX_PDS, Pd_ids, pd_ids, pd_pool>
+
+class Kernel::Pd : public Object<Pd, pd_pool>, public Cpu::Pd
 {
 	public:
 
@@ -240,17 +238,14 @@ class Kernel::Pd : public Object<Pd, MAX_PDS, Pd_ids, pd_ids, pd_pool>
 		 * \param table        translation table of the PD
 		 * \param platform_pd  core object of the PD
 		 */
-		Pd(Table * const table, Platform_pd * const platform_pd)
-		: _table(table), _platform_pd(platform_pd) { }
+		Pd(Table * const table, Platform_pd * const platform_pd);
+
+		~Pd();
 
 		/**
 		 * Let the CPU context 'c' join the PD
 		 */
-		void admit(Cpu::Context * const c)
-		{
-			c->protection_domain(id());
-			c->translation_table((addr_t)translation_table());
-		}
+		void admit(Cpu::Context * const c);
 
 
 		/***************
diff --git a/repos/base-hw/src/core/include/kernel/signal_receiver.h b/repos/base-hw/src/core/include/kernel/signal_receiver.h
index 54a05596b..d1091685d 100644
--- a/repos/base-hw/src/core/include/kernel/signal_receiver.h
+++ b/repos/base-hw/src/core/include/kernel/signal_receiver.h
@@ -19,7 +19,6 @@
 #include <base/signal.h>
 
 /* core include */
-#include <kernel/configuration.h>
 #include <kernel/object.h>
 
 namespace Kernel
@@ -49,14 +48,10 @@ namespace Kernel
 	 */
 	class Signal_receiver;
 
-	class Signal_context_ids  : public Id_allocator<MAX_SIGNAL_CONTEXTS> { };
-	class Signal_receiver_ids : public Id_allocator<MAX_SIGNAL_RECEIVERS> { };
 	typedef Object_pool<Signal_context>  Signal_context_pool;
 	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();
 }
 
@@ -202,9 +197,7 @@ class Kernel::Signal_context_killer
 };
 
 class Kernel::Signal_context
-:
-	public Object<Signal_context, MAX_SIGNAL_CONTEXTS,
-	              Signal_context_ids, signal_context_ids, signal_context_pool>
+: public Object<Signal_context, signal_context_pool>
 {
 	friend class Signal_receiver;
 	friend class Signal_context_killer;
@@ -350,10 +343,7 @@ class Kernel::Signal_context
 };
 
 class Kernel::Signal_receiver
-:
-	public Object<Signal_receiver, MAX_SIGNAL_RECEIVERS,
-	              Signal_receiver_ids, signal_receiver_ids,
-	              signal_receiver_pool>
+: public Object<Signal_receiver, signal_receiver_pool>
 {
 	friend class Signal_context;
 	friend class Signal_handler;
diff --git a/repos/base-hw/src/core/include/kernel/thread.h b/repos/base-hw/src/core/include/kernel/thread.h
index af1206e1a..685703454 100644
--- a/repos/base-hw/src/core/include/kernel/thread.h
+++ b/repos/base-hw/src/core/include/kernel/thread.h
@@ -15,7 +15,6 @@
 #define _KERNEL__THREAD_H_
 
 /* core includes */
-#include <kernel/configuration.h>
 #include <kernel/signal_receiver.h>
 #include <kernel/ipc_node.h>
 #include <kernel/cpu.h>
@@ -33,17 +32,15 @@ namespace Kernel
 	 */
 	class Thread;
 
-	class Thread_ids : public Id_allocator<MAX_THREADS> { };
 	typedef Object_pool<Thread> Thread_pool;
 
-	Thread_ids  * thread_ids();
 	Thread_pool * thread_pool();
 }
 
 class Kernel::Thread
 :
 	public Cpu::User_context,
-	public Object<Thread, MAX_THREADS, Thread_ids, thread_ids, thread_pool>,
+	public Object<Thread, thread_pool>,
 	public Cpu_domain_update, public Ipc_node, public Signal_context_killer,
 	public Signal_handler, public Thread_base, public Cpu_job
 {
diff --git a/repos/base-hw/src/core/include/kernel/vm.h b/repos/base-hw/src/core/include/kernel/vm.h
index 1530c62f3..4b8d97a47 100644
--- a/repos/base-hw/src/core/include/kernel/vm.h
+++ b/repos/base-hw/src/core/include/kernel/vm.h
@@ -28,16 +28,13 @@ namespace Kernel
 	 */
 	class Vm;
 
-	class Vm_ids : public Id_allocator<MAX_VMS> { };
 	typedef Object_pool<Vm> Vm_pool;
 
-	Vm_ids  * vm_ids();
 	Vm_pool * vm_pool();
 }
 
 
-class Kernel::Vm : public Object<Vm, MAX_VMS, Vm_ids, vm_ids, vm_pool>,
-                   public Cpu_job
+class Kernel::Vm : public Object<Vm, vm_pool>, public Cpu_job
 {
 	private:
 
diff --git a/repos/base-hw/src/core/include/spec/arm/cpu_support.h b/repos/base-hw/src/core/include/spec/arm/cpu_support.h
index 7b1690174..e414c6593 100644
--- a/repos/base-hw/src/core/include/spec/arm/cpu_support.h
+++ b/repos/base-hw/src/core/include/spec/arm/cpu_support.h
@@ -365,7 +365,17 @@ class Genode::Arm
 			/**
 			 * Assign protection domain
 			 */
-			void protection_domain(unsigned const id) { cidr = id; }
+			void protection_domain(Genode::uint8_t const id) { cidr = id; }
+		};
+
+		/**
+		 * This class comprises ARM specific protection domain attributes
+		 */
+		struct Pd
+		{
+			Genode::uint8_t asid; /* address space id */
+
+			Pd(Genode::uint8_t id) : asid(id) {}
 		};
 
 		/**
diff --git a/repos/base-hw/src/core/include/spec/arm_v6/cpu.h b/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
index 87ccba4df..93811c927 100644
--- a/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
+++ b/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
@@ -33,7 +33,11 @@ namespace Genode
 	class Cpu;
 }
 
-namespace Kernel { using Genode::Cpu_lazy_state; }
+namespace Kernel {
+	using Genode::Cpu_lazy_state;
+
+	class Pd;
+}
 
 class Genode::Cpu : public Arm
 {
@@ -119,18 +123,9 @@ class Genode::Cpu : public Arm
 		/**
 		 * Switch to the virtual mode in kernel
 		 *
-		 * \param table       base of targeted translation table
-		 * \param process_id  process ID of the initial address space
+		 * \param pd  kernel's pd object
 		 */
-		static void
-		init_virt_kernel(addr_t const table, unsigned const process_id)
-		{
-			Cidr::write(process_id);
-			Dacr::write(Dacr::init_virt_kernel());
-			Ttbr0::write(Ttbr0::init(table));
-			Ttbcr::write(0);
-			Sctlr::write(Sctlr::init_virt_kernel());
-		}
+		static void init_virt_kernel(Kernel::Pd* pd);
 
 		/**
 		 * Ensure that TLB insertions get applied
diff --git a/repos/base-hw/src/core/include/spec/arm_v7/cpu_support.h b/repos/base-hw/src/core/include/spec/arm_v7/cpu_support.h
index a7629f112..f6aa43a05 100644
--- a/repos/base-hw/src/core/include/spec/arm_v7/cpu_support.h
+++ b/repos/base-hw/src/core/include/spec/arm_v7/cpu_support.h
@@ -26,6 +26,9 @@ namespace Genode
 	class Arm_v7;
 }
 
+namespace Kernel { class Pd; }
+
+
 class Genode::Arm_v7 : public Arm
 {
 	public:
@@ -150,19 +153,9 @@ class Genode::Arm_v7 : public Arm
 		/**
 		 * Switch to the virtual mode in kernel
 		 *
-		 * \param table       base of targeted translation table
-		 * \param process_id  process ID of the kernel address-space
+		 * \param pd  kernel's pd object
 		 */
-		static void
-		init_virt_kernel(addr_t const table, unsigned const process_id)
-		{
-			Cidr::write(process_id);
-			Dacr::write(Dacr::init_virt_kernel());
-			Ttbr0::write(Ttbr0::init(table));
-			Ttbcr::write(0);
-			Sctlr::write(Sctlr::init_virt_kernel());
-			inval_branch_predicts();
-		}
+		static void init_virt_kernel(Kernel::Pd* pd);
 
 		inline static void finish_init_phys_kernel();
 
diff --git a/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h b/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
index e1157d7d4..ad9e3f448 100644
--- a/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
+++ b/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
@@ -316,7 +316,7 @@ class Genode::Cpu : public Arm_v7
 			/**
 			 * Assign protection domain
 			 */
-			void protection_domain(unsigned const id) {
+			void protection_domain(Genode::uint8_t const id) {
 				Ttbr0::Asid::set(ttbr0, id); }
 		};
 
@@ -425,20 +425,10 @@ class Genode::Cpu : public Arm_v7
 		/**
 		 * Switch to the virtual mode in kernel
 		 *
-		 * \param table       base of targeted translation table
-		 * \param process_id  process ID of the kernel address-space
+		 * \param pd  kernel pd object pointer
 		 */
-		static void
-		init_virt_kernel(addr_t const table, unsigned const process_id)
-		{
-			Mair0::write(Mair0::init_virt_kernel());
-			Cidr::write(process_id);
-			Dacr::write(Dacr::init_virt_kernel());
-			Ttbr0::write(Ttbr0::init(table, 1));
-			Ttbcr::write(Ttbcr::init_virt_kernel());
-			Sctlr::write(Sctlr::init_virt_kernel());
-			inval_branch_predicts();
-		}
+		static void init_virt_kernel(Kernel::Pd * pd);
+
 
 		/*************
 		 ** Dummies **
diff --git a/repos/base-hw/src/core/include/spec/x86/cpu.h b/repos/base-hw/src/core/include/spec/x86/cpu.h
index b1ce01816..921502f2b 100644
--- a/repos/base-hw/src/core/include/spec/x86/cpu.h
+++ b/repos/base-hw/src/core/include/spec/x86/cpu.h
@@ -46,7 +46,12 @@ namespace Genode
 	class Cpu;
 }
 
-namespace Kernel { using Genode::Cpu_lazy_state; }
+namespace Kernel
+{
+	using Genode::Cpu_lazy_state;
+
+	class Pd;
+}
 
 class Genode::Cpu_lazy_state
 {
@@ -236,27 +241,38 @@ class Genode::Cpu
 			addr_t translation_table() const { return cr3; }
 
 			/**
-			 * Assign translation-table base 'table'
+			 * Initialize context
+			 *
+			 * \param table  physical base of appropriate translation table
+			 * \param core   whether it is a core thread or not
 			 */
-			void translation_table(addr_t const table) {
-				cr3 = Cr3::init(table); }
+			void init(addr_t const table, bool core)
+			{
+				/* Constants to handle IF, IOPL values */
+				enum {
+					EFLAGS_IF_SET = 1 << 9,
+					EFLAGS_IOPL_3 = 3 << 12,
+				};
 
-			/**
-			 * Assign protection domain
-			 */
-			void protection_domain(unsigned const id) { }
+				cr3 = Cr3::init(table);
+
+				/*
+				 * Enable interrupts for all threads, set I/O privilege level
+				 * (IOPL) to 3 for core threads to allow UART access.
+				 */
+				eflags = EFLAGS_IF_SET;
+				if (core) eflags |= EFLAGS_IOPL_3;
+				else Gdt::load(Cpu::exception_entry);
+			}
 		};
 
+		struct Pd {};
+
 		/**
 		 * An usermode execution state
 		 */
 		struct User_context : Context
 		{
-			/**
-			 * Constructor
-			 */
-			User_context();
-
 			/**
 			 * Support for kernel calls
 			 */
@@ -276,37 +292,6 @@ class Genode::Cpu
 			Kernel::Call_arg user_arg_5() const { return r9; }
 			Kernel::Call_arg user_arg_6() const { return r10; }
 			Kernel::Call_arg user_arg_7() const { return r11; }
-
-			/* Constants to handle thread-specific IF, IOPL values */
-			enum {
-				CORE_PD_ID    = 1,
-				EFLAGS_IF_SET = 1 << 9,
-				EFLAGS_IOPL_3 = 3 << 12,
-			};
-
-			/**
-			 * Initialize thread context
-			 *
-			 * \param table  physical base of appropriate translation table
-			 * \param pd_id  kernel name of appropriate protection domain
-			 */
-			void init_thread(addr_t const table, unsigned const pd_id)
-			{
-				protection_domain(pd_id);
-				translation_table(table);
-
-				Gdt::load(Cpu::exception_entry);
-
-				/*
-				 * Enable interrupts for all threads, set I/O privilege level
-				 * (IOPL) to 3 for core threads to allow UART access.
-				 */
-				eflags = EFLAGS_IF_SET;
-				if (pd_id == CORE_PD_ID)
-				{
-					eflags |= EFLAGS_IOPL_3;
-				}
-			}
 		};
 
 		/**
@@ -376,12 +361,9 @@ class Genode::Cpu
 		/**
 		 * Switch to the virtual mode in kernel
 		 *
-		 * \param table       base of targeted translation table
-		 * \param process_id  process ID of the kernel address-space
+		 * \param pd  kernel's pd object
 		 */
-		static void
-		init_virt_kernel(addr_t const table, unsigned const process_id) {
-			Cr3::write(Cr3::init(table)); }
+		static void init_virt_kernel(Kernel::Pd * pd);
 
 		inline static void finish_init_phys_kernel() { _init_fpu(); }
 
diff --git a/repos/base-hw/src/core/kernel/kernel.cc b/repos/base-hw/src/core/kernel/kernel.cc
index 87d4e1544..a5591a35a 100644
--- a/repos/base-hw/src/core/kernel/kernel.cc
+++ b/repos/base-hw/src/core/kernel/kernel.cc
@@ -52,11 +52,6 @@ namespace Kernel
 	/* import Genode types */
 	typedef Genode::Core_thread_id Core_thread_id;
 
-	Pd_ids * pd_ids() { return unmanaged_singleton<Pd_ids>(); }
-	Thread_ids * thread_ids() { return unmanaged_singleton<Thread_ids>(); }
-	Signal_context_ids * signal_context_ids() { return unmanaged_singleton<Signal_context_ids>(); }
-	Signal_receiver_ids * signal_receiver_ids() { return unmanaged_singleton<Signal_receiver_ids>(); }
-
 	Pd_pool * pd_pool() { return unmanaged_singleton<Pd_pool>(); }
 	Thread_pool * thread_pool() { return unmanaged_singleton<Thread_pool>(); }
 	Signal_context_pool * signal_context_pool() { return unmanaged_singleton<Signal_context_pool>(); }
@@ -123,6 +118,7 @@ namespace Kernel
 			{
 				using namespace Genode;
 
+
 				Platform_pd::_id = Pd::id();
 
 				/* map exception vector for core */
@@ -188,6 +184,9 @@ namespace Kernel
 }
 
 
+Kernel::Id_allocator & Kernel::id_alloc() {
+	return *unmanaged_singleton<Id_allocator>(); }
+
 Pic * Kernel::pic() { return unmanaged_singleton<Pic>(); }
 
 
@@ -215,8 +214,7 @@ extern "C" void init_kernel_up()
 	 */
 
 	/* calculate in advance as needed later when data writes aren't allowed */
-	core_tt_base = (addr_t) core_pd()->translation_table();
-	core_pd_id   = core_pd()->id();
+	core_pd();
 
 	/* initialize all CPU objects */
 	cpu_pool();
@@ -297,7 +295,7 @@ extern "C" void init_kernel_mp()
 	Cpu::init_phys_kernel();
 
 	/* switch to core address space */
-	Cpu::init_virt_kernel(core_tt_base, core_pd_id);
+	Cpu::init_virt_kernel(core_pd());
 
 	/*
 	 * Now it's safe to use 'cmpxchg'
diff --git a/repos/base-hw/src/core/kernel/thread.cc b/repos/base-hw/src/core/kernel/thread.cc
index a2e7b293f..eeb97560c 100644
--- a/repos/base-hw/src/core/kernel/thread.cc
+++ b/repos/base-hw/src/core/kernel/thread.cc
@@ -170,7 +170,7 @@ void Thread::init(Cpu * const cpu, Pd * const pd,
 
 	/* join protection domain */
 	_pd = pd;
-	User_context::init_thread((addr_t)_pd->translation_table(), pd_id());
+	_pd->admit(this);
 
 	/* print log message */
 	if (START_VERBOSE) {
@@ -507,10 +507,6 @@ void Thread::_call_access_thread_regs()
 }
 
 
-void Thread::_call_update_pd() {
-	if (Cpu_domain_update::_do_global(user_arg_1())) { _pause(); } }
-
-
 void Thread::_call_update_data_region()
 {
 	/*
@@ -558,7 +554,7 @@ void Thread::_call_update_instr_region()
 
 void Thread::_print_activity_table()
 {
-	for (unsigned id = 0; id < MAX_THREADS; id++) {
+	for (unsigned id = 0; id < MAX_KERNEL_OBJECTS; id++) {
 		Thread * const t = Thread::pool()->object(id);
 		if (!t) { continue; }
 		t->_print_activity(t == this);
diff --git a/repos/base-hw/src/core/spec/arm/kernel/pd.cc b/repos/base-hw/src/core/spec/arm/kernel/pd.cc
new file mode 100644
index 000000000..750cf3612
--- /dev/null
+++ b/repos/base-hw/src/core/spec/arm/kernel/pd.cc
@@ -0,0 +1,43 @@
+/*
+ * \brief   Kernel backend for protection domains
+ * \author  Stefan Kalkowski
+ * \date    2015-03-20
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* Genode includes */
+#include <util/bit_allocator.h>
+
+/* core includes */
+#include <kernel/pd.h>
+
+using Asid_allocator = Genode::Bit_allocator<256>;
+
+static Asid_allocator &alloc() {
+	return *unmanaged_singleton<Asid_allocator>(); }
+
+
+Kernel::Pd::Pd(Kernel::Pd::Table * const table,
+               Genode::Platform_pd * const platform_pd)
+: Kernel::Cpu::Pd((Genode::uint8_t)alloc().alloc()),
+  _table(table), _platform_pd(platform_pd) { }
+
+
+Kernel::Pd::~Pd() {
+	/* clean up buffers of memory management */
+	Cpu::flush_tlb_by_pid(asid);
+	alloc().free(asid);
+}
+
+
+void Kernel::Pd::admit(Kernel::Cpu::Context * const c)
+{
+	c->protection_domain(asid);
+	c->translation_table((addr_t)translation_table());
+}
diff --git a/repos/base-hw/src/core/spec/arm/kernel/thread.cc b/repos/base-hw/src/core/spec/arm/kernel/thread.cc
index ffa3ba258..daae32c13 100644
--- a/repos/base-hw/src/core/spec/arm/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/arm/kernel/thread.cc
@@ -122,3 +122,9 @@ void Thread::_mmu_exception()
 	}
 	PERR("unknown MMU exception");
 }
+
+
+void Thread::_call_update_pd()
+{
+	if (Cpu_domain_update::_do_global(user_arg_1())) { _pause(); }
+}
diff --git a/repos/base-hw/src/core/spec/arm_v6/cpu.cc b/repos/base-hw/src/core/spec/arm_v6/cpu.cc
index 58fac14d2..5161c1960 100644
--- a/repos/base-hw/src/core/spec/arm_v6/cpu.cc
+++ b/repos/base-hw/src/core/spec/arm_v6/cpu.cc
@@ -14,9 +14,20 @@
  */
 
 #include <cpu.h>
+#include <kernel/pd.h>
 
 void Genode::Arm::flush_data_caches() {
 	asm volatile ("mcr p15, 0, %[rd], c7, c14, 0" :: [rd]"r"(0) : ); }
 
 void Genode::Arm::invalidate_data_caches() {
 	asm volatile ("mcr p15, 0, %[rd], c7, c6, 0" :: [rd]"r"(0) : ); }
+
+
+void Genode::Cpu::init_virt_kernel(Kernel::Pd* pd)
+{
+	Cidr::write(pd->asid);
+	Dacr::write(Dacr::init_virt_kernel());
+	Ttbr0::write(Ttbr0::init((Genode::addr_t)pd->translation_table()));
+	Ttbcr::write(0);
+	Sctlr::write(Sctlr::init_virt_kernel());
+}
diff --git a/repos/base-hw/src/core/spec/arm_v7/cpu.cc b/repos/base-hw/src/core/spec/arm_v7/cpu.cc
index c53cabc26..3f01d5c9e 100644
--- a/repos/base-hw/src/core/spec/arm_v7/cpu.cc
+++ b/repos/base-hw/src/core/spec/arm_v7/cpu.cc
@@ -13,6 +13,7 @@
  */
 
 #include <cpu.h>
+#include <kernel/pd.h>
 
 /**
  * Helpers that increase readability of MCR and MRC commands
@@ -156,3 +157,14 @@ Genode::Arm::Psr::access_t Genode::Arm::Psr::init_user_with_trustzone()
 	A::set(v, 1);
 	return v;
 }
+
+
+void Genode::Arm_v7::init_virt_kernel(Kernel::Pd * pd)
+{
+	Cidr::write(pd->asid);
+	Dacr::write(Dacr::init_virt_kernel());
+	Ttbr0::write(Ttbr0::init((Genode::addr_t)pd->translation_table()));
+	Ttbcr::write(0);
+	Sctlr::write(Sctlr::init_virt_kernel());
+	inval_branch_predicts();
+}
diff --git a/repos/base-hw/src/core/spec/arm_v7/trustzone/kernel/vm.cc b/repos/base-hw/src/core/spec/arm_v7/trustzone/kernel/vm.cc
index 3585cd014..2917d05bc 100644
--- a/repos/base-hw/src/core/spec/arm_v7/trustzone/kernel/vm.cc
+++ b/repos/base-hw/src/core/spec/arm_v7/trustzone/kernel/vm.cc
@@ -22,7 +22,6 @@ extern Genode::addr_t _tz_master_context;
 
 namespace Kernel
 {
-	Vm_ids * vm_ids() { return unmanaged_singleton<Vm_ids>(); }
 	Vm_pool * vm_pool() { return unmanaged_singleton<Vm_pool>(); }
 }
 
diff --git a/repos/base-hw/src/core/spec/arm_v7/virtualization/kernel/vm.cc b/repos/base-hw/src/core/spec/arm_v7/virtualization/kernel/vm.cc
index 73b5d12de..90e03f0fd 100644
--- a/repos/base-hw/src/core/spec/arm_v7/virtualization/kernel/vm.cc
+++ b/repos/base-hw/src/core/spec/arm_v7/virtualization/kernel/vm.cc
@@ -16,7 +16,6 @@
 
 namespace Kernel
 {
-	Vm_ids * vm_ids() { return unmanaged_singleton<Vm_ids>(); }
 	Vm_pool * vm_pool() { return unmanaged_singleton<Vm_pool>(); }
 
 	/**
diff --git a/repos/base-hw/src/core/spec/cortex_a15/cpu.cc b/repos/base-hw/src/core/spec/cortex_a15/cpu.cc
new file mode 100644
index 000000000..226916873
--- /dev/null
+++ b/repos/base-hw/src/core/spec/cortex_a15/cpu.cc
@@ -0,0 +1,27 @@
+/*
+ * \brief   Kernel backend for protection domains
+ * \author  Stefan Kalkowski
+ * \date    2015-03-20
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* core includes */
+#include <kernel/pd.h>
+#include <cpu.h>
+
+void Genode::Cpu::init_virt_kernel(Kernel::Pd * pd)
+{
+	Mair0::write(Mair0::init_virt_kernel());
+	Dacr::write(Dacr::init_virt_kernel());
+	Ttbr0::write(Ttbr0::init((Genode::addr_t)pd->translation_table(),
+	                         pd->asid));
+	Ttbcr::write(Ttbcr::init_virt_kernel());
+	Sctlr::write(Sctlr::init_virt_kernel());
+	inval_branch_predicts();
+}
diff --git a/repos/base-hw/src/core/spec/x86/cpu.cc b/repos/base-hw/src/core/spec/x86/cpu.cc
new file mode 100644
index 000000000..31141831c
--- /dev/null
+++ b/repos/base-hw/src/core/spec/x86/cpu.cc
@@ -0,0 +1,19 @@
+/*
+ * \brief   Kernel backend for protection domains
+ * \author  Stefan Kalkowski
+ * \date    2015-03-20
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* core includes */
+#include <cpu.h>
+#include <kernel/pd.h>
+
+void Genode::Cpu::init_virt_kernel(Kernel::Pd * pd) {
+	Cr3::write(Cr3::init((addr_t)pd->translation_table())); }
diff --git a/repos/base-hw/src/core/spec/x86/kernel/cpu.cc b/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
index ed6095a8d..9b0c906e9 100644
--- a/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
+++ b/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
@@ -23,7 +23,7 @@ Cpu_idle::Cpu_idle(Cpu * const cpu) : Cpu_job(Cpu_priority::min, 0)
 	Cpu_job::cpu(cpu);
 	ip = (addr_t)&_main;
 	sp = (addr_t)&_stack[stack_size];
-	init_thread((addr_t)core_pd()->translation_table(), core_pd()->id());
+	init((addr_t)core_pd()->translation_table(), true);
 }
 
 
diff --git a/repos/base-hw/src/core/spec/x86/kernel/pd.cc b/repos/base-hw/src/core/spec/x86/kernel/pd.cc
new file mode 100644
index 000000000..cdaed7a1e
--- /dev/null
+++ b/repos/base-hw/src/core/spec/x86/kernel/pd.cc
@@ -0,0 +1,27 @@
+/*
+ * \brief   Kernel backend for protection domains
+ * \author  Stefan Kalkowski
+ * \date    2015-03-20
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* core includes */
+#include <platform_pd.h>
+#include <kernel/pd.h>
+
+Kernel::Pd::Pd(Kernel::Pd::Table   * const table,
+               Genode::Platform_pd * const platform_pd)
+: _table(table), _platform_pd(platform_pd) { }
+
+
+Kernel::Pd::~Pd() { }
+
+
+void Kernel::Pd::admit(Kernel::Cpu::Context * const c) {
+	c->init((addr_t)translation_table(), this == Kernel::core_pd()); }
diff --git a/repos/base-hw/src/core/spec/x86/kernel/thread.cc b/repos/base-hw/src/core/spec/x86/kernel/thread.cc
index a19844654..528eca097 100644
--- a/repos/base-hw/src/core/spec/x86/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/x86/kernel/thread.cc
@@ -47,3 +47,6 @@ void Thread::exception(unsigned const cpu)
 	     pd_label(), label(), trapno, errcode);
 	_stop();
 }
+
+
+void Thread::_call_update_pd() { }
diff --git a/repos/base-hw/src/core/spec/x86/platform_support.cc b/repos/base-hw/src/core/spec/x86/platform_support.cc
index 5309fd07c..97811be40 100644
--- a/repos/base-hw/src/core/spec/x86/platform_support.cc
+++ b/repos/base-hw/src/core/spec/x86/platform_support.cc
@@ -67,6 +67,3 @@ long Platform::irq(long const user_irq)
 	if (user_irq) return user_irq + Board::VECTOR_REMAP_BASE;
 	return Board::TIMER_VECTOR_USER;
 }
-
-
-Cpu::User_context::User_context() { }