diff --git a/Kconfig b/Kconfig
index d70483451..3251ceb28 100644
--- a/Kconfig
+++ b/Kconfig
@@ -147,6 +147,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A9
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for EXYNOS4 platform (ODROID-X).
 
@@ -156,6 +157,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for EXYNOS5410 platform (ODROID-XU).
 
@@ -165,6 +167,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for EXYNOS5422 platform (ODROID-XU3).
 
@@ -173,6 +176,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for EXYNOS5250 platform (ARNDALE).
 
@@ -181,6 +185,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for Qualcomm Snapdragon S4 APQ8064 platforms (Inforce IFC6410).
 
@@ -190,6 +195,7 @@ menu "seL4 System"
             select ARM_CORTEX_A9
             select ARCH_ARM_V7A
             select PLAT_IMX6
+            select ARCH_ARM_MPCORE
             help
                 Support for iMX6 platform (Sabre Lite).
 
@@ -199,6 +205,7 @@ menu "seL4 System"
             select ARM_CORTEX_A9
             select ARCH_ARM_V7A
             select PLAT_IMX6
+            select ARCH_ARM_MPCORE
             help
                 Support for iMX6 platform (Wandboard Quad).
 
@@ -208,6 +215,7 @@ menu "seL4 System"
             select ARM_CORTEX_A7
             select ARCH_ARM_V7A
             select PLAT_IMX7
+            select ARCH_ARM_MPCORE
             help
                 Support for iMX7 Sabre Dual.
 
@@ -216,6 +224,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A9
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for Xilinx Zynq-7000 platforms.
 
@@ -230,6 +239,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for ALLWINNERA20 platform (CUBIETRUCK).
 
@@ -238,6 +248,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A15
             select ARCH_ARM_V7A
+            select ARCH_ARM_MPCORE
             help
                 Support for Tegra K1 platform
 
@@ -246,6 +257,7 @@ menu "seL4 System"
             depends on ARCH_ARM
             select ARM_CORTEX_A57
             select ARCH_ARM_V8A
+            select ARCH_ARM_MPCORE
             help
                 Support for HiKey platform.
 
diff --git a/include/arch/arm/arch/32/mode/machine.h b/include/arch/arm/arch/32/mode/machine.h
index f04431cec..fab93fd9c 100644
--- a/include/arch/arm/arch/32/mode/machine.h
+++ b/include/arch/arm/arch/32/mode/machine.h
@@ -152,6 +152,21 @@ static inline void writeTTBR0(paddr_t addr)
     asm volatile("mcr p15, 0, %0, c2, c0, 0" : :
                  "r"((addr & 0xffffe000) | 0x18));
 }
+
+/** DONT_TRANSLATE */
+static inline void writeTPIDRURW(word_t reg)
+{
+    asm volatile("mcr p15, 0, %0, c13, c0, 2" :: "r"(reg));
+}
+
+/** DONT_TRANSLATE */
+static inline word_t readTPIDRURW(void)
+{
+    word_t reg;
+    asm volatile("mrc p15, 0, %0, c13, c0, 2" : "=r"(reg));
+    return reg;
+}
+
 static inline void setCurrentPD(paddr_t addr)
 {
     /* Mask supplied address (retain top 19 bits).  Set the lookup cache bits:
diff --git a/include/arch/arm/arch/32/mode/machine/registerset.h b/include/arch/arm/arch/32/mode/machine/registerset.h
index 4e497108e..a30796c22 100644
--- a/include/arch/arm/arch/32/mode/machine/registerset.h
+++ b/include/arch/arm/arch/32/mode/machine/registerset.h
@@ -93,7 +93,14 @@ enum _register {
     CPSR = 16,
 
     FaultInstruction = 17,
+#ifdef CONFIG_ARCH_ARM_MPCORE
+    /* user readable/writable thread ID register.
+     * name comes from the ARM manual */
+    TPIDRURW = 18,
+    n_contextRegisters = 19,
+#else
     n_contextRegisters = 18,
+#endif
 };
 
 compile_assert(sp_offset_correct, SP * sizeof(word_t) == PT_SP)
diff --git a/include/arch/arm/arch/kernel/traps.h b/include/arch/arm/arch/kernel/traps.h
index 24dc29938..393b3e482 100644
--- a/include/arch/arm/arch/kernel/traps.h
+++ b/include/arch/arm/arch/kernel/traps.h
@@ -16,10 +16,16 @@
 
 static inline void arch_c_entry_hook(void)
 {
+#ifdef CONFIG_ARCH_ARM_MPCORE
+    setRegister(ksCurThread, TPIDRURW, readTPIDRURW());
+#endif
 }
 
 static inline void arch_c_exit_hook(void)
 {
+#ifdef CONFIG_ARCH_ARM_MPCORE
+    writeTPIDRURW(getRegister(ksCurThread, TPIDRURW));
+#endif
 }
 
 void c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
diff --git a/src/arch/arm/Kconfig b/src/arch/arm/Kconfig
index 4337c9d1a..b87f8b30e 100644
--- a/src/arch/arm/Kconfig
+++ b/src/arch/arm/Kconfig
@@ -56,3 +56,13 @@ config EXPORT_VCNT_USER
         WARNING: selecting this option opens a timing
         channel
 
+config ARCH_ARM_MPCORE
+    bool "ARM platform supports MPCore"
+    default n
+    depends on ARCH_ARM
+    select IPC_BUF_TPIDRURW
+    help
+        On MPCore supported platforms there are additional
+        registers and features available. Some of these
+        the kernel just needs to be aware of, and others
+        enable additional kernel features.