diff --git a/base-hw/src/core/arm_v7/mode_transition.s b/base-hw/src/core/arm_v7/mode_transition.s
index d22f37f64..a3ff14fc8 100644
--- a/base-hw/src/core/arm_v7/mode_transition.s
+++ b/base-hw/src/core/arm_v7/mode_transition.s
@@ -47,6 +47,7 @@
 	/* load kernel section table */
 	adr sp, _mt_master_context_begin
 	ldr sp, [sp, #19*4]
+	orr sp, sp, #0b1000000 /* set TTBR0 flags */
 	mcr p15, 0, sp, c2, c0, 0
 	isb
 	dsb
@@ -128,6 +129,7 @@
 	/* get user contextidr and section table */
 	ldr sp, [lr, #18*4]
 	ldr lr, [lr, #19*4]
+	orr lr, lr, #0b1000000 /* set TTBR0 flags */
 
 	/********************************************************
 	 ** From now on, until we leave kernel mode, we must   **
diff --git a/base-hw/src/core/cpu/arm.h b/base-hw/src/core/cpu/arm.h
index f21be4848..156cb3fcc 100644
--- a/base-hw/src/core/cpu/arm.h
+++ b/base-hw/src/core/cpu/arm.h
@@ -170,11 +170,6 @@ namespace Arm
 		 */
 		struct Ttbr0 : Register<32>
 		{
-			struct Irgn_1 : Bitfield<0,1> /* inner cachable mode */
-			{
-				enum { NON_CACHEABLE = 0 };
-			};
-
 			struct S : Bitfield<1,1> { }; /* shareable */
 
 			struct Rgn : Bitfield<3, 2> /* outer cachable attributes */
@@ -209,7 +204,6 @@ namespace Arm
 			static access_t init_virt_kernel(addr_t const sect_table)
 			{
 				return S::bits(0) |
-				       Irgn_1::bits(Irgn_1::NON_CACHEABLE) |
 				       Rgn::bits(Rgn::NON_CACHEABLE) |
 				       Ba::masked((addr_t)sect_table);
 			}
diff --git a/base-hw/src/core/cpu/arm_v6.h b/base-hw/src/core/cpu/arm_v6.h
index a3759fd61..0473d547f 100644
--- a/base-hw/src/core/cpu/arm_v6.h
+++ b/base-hw/src/core/cpu/arm_v6.h
@@ -111,6 +111,11 @@ namespace Arm_v6
 		 */
 		struct Ttbr0 : Arm::Cpu::Ttbr0
 		{
+			struct C : Bitfield<0,1> /* inner cachable mode */
+			{
+				enum { NON_CACHEABLE = 0 };
+			};
+
 			struct P : Bitfield<2,1> { }; /* memory controller ECC enabled */
 
 			/**
@@ -121,7 +126,8 @@ namespace Arm_v6
 			static access_t init_virt_kernel(addr_t const sect_table)
 			{
 				return Arm::Cpu::Ttbr0::init_virt_kernel(sect_table) |
-				       P::bits(0);
+				       P::bits(0) |
+				       C::bits(C::NON_CACHEABLE);
 			}
 		};
 
@@ -163,6 +169,11 @@ namespace Arm_v6
 			Ttbcr::write(Ttbcr::init_virt_kernel());
 			Sctlr::write(Sctlr::init_virt_kernel());
 		}
+
+		/**
+		 * Ensure that TLB insertions get applied
+		 */
+		static void tlb_insertions() { flush_tlb(); }
 	};
 }
 
diff --git a/base-hw/src/core/cpu/arm_v7.h b/base-hw/src/core/cpu/arm_v7.h
index 178ea7b7d..5b8c7682c 100644
--- a/base-hw/src/core/cpu/arm_v7.h
+++ b/base-hw/src/core/cpu/arm_v7.h
@@ -124,10 +124,8 @@ namespace Arm_v7
 		{
 			struct Nos : Bitfield<6,1> { }; /* not outer shareable */
 
-			struct Irgn_0 : Bitfield<6,1> /* inner cachable mode */
-			{
-				enum { NON_CACHEABLE = 0 };
-			};
+			struct Irgn_1 : Bitfield<0,1> { }; /* inner cachable mode */
+			struct Irgn_0 : Bitfield<6,1> { }; /* inner cachable mode */
 
 			/**
 			 * Value for the switch to virtual mode in kernel
@@ -138,7 +136,8 @@ namespace Arm_v7
 			{
 				return Arm::Cpu::Ttbr0::init_virt_kernel(sect_table) |
 				       Nos::bits(0) |
-				       Irgn_0::bits(Irgn_0::NON_CACHEABLE);
+				       Irgn_1::bits(0) |
+				       Irgn_0::bits(1);
 			}
 		};
 
diff --git a/base-hw/src/core/cpu/cortex_a8.h b/base-hw/src/core/cpu/cortex_a8.h
new file mode 100644
index 000000000..796982029
--- /dev/null
+++ b/base-hw/src/core/cpu/cortex_a8.h
@@ -0,0 +1,37 @@
+/*
+ * \brief  CPU driver for core
+ * \author Martin stein
+ * \date   2011-11-03
+ */
+
+/*
+ * Copyright (C) 2011-2012 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.
+ */
+
+#ifndef _CPU__CORTEX_A8_H_
+#define _CPU__CORTEX_A8_H_
+
+/* core includes */
+#include <cpu/arm_v7.h>
+
+namespace Cortex_a8
+{
+	using namespace Genode;
+
+	/**
+	 * CPU driver for core
+	 */
+	struct Cpu : Arm_v7::Cpu
+	{
+		/**
+		 * Ensure that TLB insertions get applied
+		 */
+		static void tlb_insertions() { flush_tlb(); }
+	};
+}
+
+#endif /* _CPU__CORTEX_A8_H_ */
+
diff --git a/base-hw/src/core/cpu/cortex_a9.h b/base-hw/src/core/cpu/cortex_a9.h
index 46e2848ea..c8eac6ac8 100644
--- a/base-hw/src/core/cpu/cortex_a9.h
+++ b/base-hw/src/core/cpu/cortex_a9.h
@@ -45,6 +45,13 @@ namespace Cortex_a9
 			PRIVATE_TIMER_IRQ = 29,
 			PRIVATE_TIMER_CLK = PERIPH_CLK
 		};
+
+		/**
+		 * Ensure that TLB insertions get applied
+		 *
+		 * Nothing to do because MMU uses caches on pagetable walks
+		 */
+		static void tlb_insertions() { }
 	};
 }
 
diff --git a/base-hw/src/core/imx53/cpu.h b/base-hw/src/core/imx53/cpu.h
index 1b0df6db9..70d2ea9aa 100644
--- a/base-hw/src/core/imx53/cpu.h
+++ b/base-hw/src/core/imx53/cpu.h
@@ -15,14 +15,14 @@
 #define _IMX53__CPU_H_
 
 /* core includes */
-#include <cpu/arm_v7.h>
+#include <cpu/cortex_a8.h>
 
 namespace Genode
 {
 	/**
 	 * CPU driver for core
 	 */
-	class Cpu : public Arm_v7::Cpu { };
+	class Cpu : public Cortex_a8::Cpu { };
 }
 
 #endif /* _IMX53__CPU_H_ */
diff --git a/base-hw/src/core/kernel.cc b/base-hw/src/core/kernel.cc
index 698a757b7..bf2894219 100644
--- a/base-hw/src/core/kernel.cc
+++ b/base-hw/src/core/kernel.cc
@@ -948,7 +948,7 @@ namespace Kernel
 		 * the memory that holds the TLB data, because the latter
 		 * is not feasible in core space.
 		 */
-		Cpu::flush_caches();
+		Cpu::tlb_insertions();
 
 		/* resume targeted thread */
 		t->resume();