diff --git a/headers/private/kernel/boot/arch/arm/arch_cpu.h b/headers/private/kernel/boot/arch/arm/arch_cpu.h
index c81a2f317f..c1f5fe28a3 100644
--- a/headers/private/kernel/boot/arch/arm/arch_cpu.h
+++ b/headers/private/kernel/boot/arch/arm/arch_cpu.h
@@ -20,6 +20,61 @@ void arch_ucode_load(BootVolume& volume);
 bigtime_t system_time();
 void spin(bigtime_t microseconds);
 
+
+static inline uint32
+cpu_read_CPSR(void)
+{
+	uint32 res;
+	asm volatile("MRS %0, CPSR": "=r" (res));
+	return res;
+}
+
+
+static inline uint32
+mmu_read_SCTLR(void)
+{
+	uint32 res;
+	asm volatile("MRC p15, 0, %0, c1, c0, 0": "=r" (res));
+	return res;
+}
+
+
+static inline uint32
+mmu_read_TTBR0(void)
+{
+	uint32 res;
+	asm volatile("MRC p15, 0, %0, c2, c0, 0": "=r" (res));
+	return res;
+}
+
+
+static inline uint32
+mmu_read_TTBR1(void)
+{
+	uint32 res;
+	asm volatile("MRC p15, 0, %0, c2, c0, 1": "=r" (res));
+	return res;
+}
+
+
+static inline uint32
+mmu_read_TTBCR(void)
+{
+	uint32 res;
+	asm volatile("MRC p15, 0, %0, c2, c0, 2": "=r" (res));
+	return res;
+}
+
+
+static inline uint32
+mmu_read_DACR(void)
+{
+	uint32 res;
+	asm volatile("MRC p15, 0, %0, c3, c0, 0": "=r" (res));
+	return res;
+}
+
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/system/boot/platform/efi/arch/arm/arch_start.cpp b/src/system/boot/platform/efi/arch/arm/arch_start.cpp
index 90540bb146..37e0ed50d4 100644
--- a/src/system/boot/platform/efi/arch/arm/arch_start.cpp
+++ b/src/system/boot/platform/efi/arch/arm/arch_start.cpp
@@ -5,6 +5,7 @@
 
 
 #include <kernel.h>
+#include <boot/arch/arm/arch_cpu.h>
 #include <boot/platform.h>
 #include <boot/stage2.h>
 #include <boot/stdio.h>
@@ -14,6 +15,13 @@
 #include "serial.h"
 #include "smp.h"
 
+//#define TRACE_ARCH_START
+#ifdef TRACE_ARCH_START
+#	define TRACE(x...) dprintf(x)
+#else
+#	define TRACE(x...) ;
+#endif
+
 
 #define ALIGN_MEMORY_MAP	4
 
@@ -224,6 +232,13 @@ arch_start_kernel(addr_t kernelEntry)
 
 	//smp_boot_other_cpus(final_ttbr0, kernelEntry, (addr_t)&gKernelArgs);
 
+	TRACE("CPSR = 0x%08" B_PRIx32 "\n", cpu_read_CPSR());
+	TRACE("SCTLR = 0x%08" B_PRIx32 "\n", mmu_read_SCTLR());
+	TRACE("TTBR0 = 0x%08" B_PRIx32 ", TTBR1 = 0x%08" B_PRIx32 ", TTBCR = 0x%08" B_PRIx32 "\n",
+		mmu_read_TTBR0(), mmu_read_TTBR1(), mmu_read_TTBCR());
+	TRACE("DACR = 0x%08" B_PRIx32 "\n",
+		mmu_read_DACR());
+
 	// Enter the kernel!
 	dprintf("enter_kernel(ttbr0: 0x%08x, kernelArgs: 0x%08x, "
 		"kernelEntry: 0x%08x, sp: 0x%08x)\n",