diff --git a/.cmake-format.yaml b/.cmake-format.yaml
index 77f34a9ebb75829b23da73103a730fa01d2ca496..eb93d399893596bb37909dbb9465c868ffdaee04 100644
--- a/.cmake-format.yaml
+++ b/.cmake-format.yaml
@@ -53,3 +53,7 @@ additional_commands:
         NUM_PPI: '*'
         INTERRUPT_CONTROLLER: '*'
         TIMER: '*'
+        KERNEL_WCET: '*'
+        CLK_MAGIC: '*'
+        CLK_SHIFT: '*'
+        TIMER_PRECISION: '*'
diff --git a/config.cmake b/config.cmake
index 4f825a6f94b7de37a446950ed5dd4d3ec9fbf10b..7fefcf0a139145cbb5b263554375528561aae0be 100644
--- a/config.cmake
+++ b/config.cmake
@@ -84,6 +84,9 @@ if(DEFINED CONFIGURE_MAX_IRQ)
         math(EXPR BITS "${BITS} + 1")
     endif()
     set(CONFIGURE_IRQ_SLOT_BITS "${BITS}" CACHE INTERNAL "")
+    if(NOT DEFINED ${CONFIGURE_TIMER_PRECISION})
+        set(CONFIGURE_TIMER_PRECISION "0")
+    endif()
     configure_file(
         src/arch/${KernelArch}/platform_gen.h.in
         ${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/platform_gen.h @ONLY
diff --git a/configs/seL4Config.cmake b/configs/seL4Config.cmake
index 72ea4ed3d30375e6aa70a071887055d9265044ae..8f5339fe5909695c71a1c1b136ba8dce478bea4f 100644
--- a/configs/seL4Config.cmake
+++ b/configs/seL4Config.cmake
@@ -102,13 +102,22 @@ unset(CONFIGURE_NUM_PPI CACHE)
 unset(CONFIGURE_INTERRUPT_CONTROLLER CACHE)
 unset(CONFIGURE_TIMER CACHE)
 unset(CONFIGURE_SMMU CACHE)
+unset(CONFIGURE_CLK_SHIFT CACHE)
+unset(CONFIGURE_CLK_MAGIC CACHE)
+unset(CONFIGURE_KERNEL_WCET CACHE)
+unset(CONFIGURE_TIMER_PRECISION CACHE)
+# CLK_SHIFT and CLK_MAGIC are generated from tools/reciprocal.py
+# based on the TIMER_CLK_HZ to simulate division.
+# This could be moved to a cmake function
+# in future to build the values on the first build. Note the calculation
+# can take a long time though.
 function(declare_default_headers)
     cmake_parse_arguments(
         PARSE_ARGV
         0
         CONFIGURE
         ""
-        "TIMER_FREQUENCY;MAX_IRQ;NUM_PPI;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU"
+        "TIMER_FREQUENCY;MAX_IRQ;NUM_PPI;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU;CLK_SHIFT;CLK_MAGIC;KERNEL_WCET;TIMER_PRECISION"
         ""
     )
     set(CONFIGURE_TIMER_FREQUENCY "${CONFIGURE_TIMER_FREQUENCY}" CACHE INTERNAL "")
@@ -118,6 +127,10 @@ function(declare_default_headers)
     set(CONFIGURE_INTERRUPT_CONTROLLER "${CONFIGURE_INTERRUPT_CONTROLLER}" CACHE INTERNAL "")
     set(CONFIGURE_TIMER "${CONFIGURE_TIMER}" CACHE INTERNAL "")
     set(CONFIGURE_SMMU "${CONFIGURE_SMMU}" CACHE INTERNAL "")
+    set(CONFIGURE_CLK_SHIFT "${CONFIGURE_CLK_SHIFT}" CACHE INTERNAL "")
+    set(CONFIGURE_CLK_MAGIC "${CONFIGURE_CLK_MAGIC}" CACHE INTERNAL "")
+    set(CONFIGURE_KERNEL_WCET "${CONFIGURE_KERNEL_WCET}" CACHE INTERNAL "")
+    set(CONFIGURE_TIMER_PRECISION "${CONFIGURE_TIMER_PRECISION}" CACHE INTERNAL "")
 endfunction()
 
 # For all of the common variables we set a default value here if they haven't
diff --git a/include/arch/arm/arch/32/mode/machine/timer.h b/include/arch/arm/arch/32/mode/machine/timer.h
index f5d506311c505886cf15ff0bef11f146ca48c484..c75b6a32013b3f77f0afe4930e6bd49146b370b2 100644
--- a/include/arch/arm/arch/32/mode/machine/timer.h
+++ b/include/arch/arm/arch/32/mode/machine/timer.h
@@ -30,4 +30,32 @@
 #define CNT_CVAL CNTV_CVAL
 #endif
 
+#ifdef CONFIG_KERNEL_MCS
+#include <util.h>
+
+/* timer function definitions that work for all 32bit arm platforms that provide
+ * CLK_MAGIC and TIMER_CLOCK_MHZ -- these definitions might need to move
+ * if we come across an arm platform that does not suit this model */
+
+/* get the max value ticksToUs can be passed without overflowing */
+static inline CONST ticks_t getMaxTicksToUs(void)
+{
+#if USE_KHZ
+    return UINT64_MAX / KHZ_IN_MHZ / CLK_MAGIC;
+#else
+    return UINT64_MAX / CLK_MAGIC;
+#endif
+}
+
+static inline CONST time_t ticksToUs(ticks_t ticks)
+{
+    /* simulate 64bit division using multiplication by reciprocal */
+#if USE_KHZ
+    return (ticks * KHZ_IN_MHZ) * CLK_MAGIC >> CLK_SHIFT;
+#else
+    return (ticks * CLK_MAGIC) >> CLK_SHIFT;
+#endif
+}
+#endif /* CONFIG_KERNEL_MCS */
+
 #endif /* __ARCH_MODE_MACHINE_TIMER_H_ */
diff --git a/include/arch/arm/arch/64/mode/machine/timer.h b/include/arch/arm/arch/64/mode/machine/timer.h
index 2444f8b3b80878f6fb05409b1e8e7423fa24c48d..519414965ae3fb21ff67943a5c277a130545be1b 100644
--- a/include/arch/arm/arch/64/mode/machine/timer.h
+++ b/include/arch/arm/arch/64/mode/machine/timer.h
@@ -26,4 +26,27 @@
 #endif
 #define CNTFRQ   "cntfrq_el0"
 
+#ifdef CONFIG_KERNEL_MCS
+#include <stdint.h>
+#include <util.h>
+
+/* timer function definitions that work for all 64 bit arm platforms */
+static inline CONST ticks_t getMaxTicksToUs(void)
+{
+#if USE_KHZ
+    return UINT64_MAX / TIMER_CLOCK_KHZ;
+#else
+    return UINT64_MAX;
+#endif
+}
+
+static inline CONST time_t ticksToUs(ticks_t ticks)
+{
+#if USE_KHZ
+    return (ticks * TIMER_CLOCK_KHZ) / TIMER_CLOCK_MHZ;
+#else
+    return ticks / TIMER_CLOCK_MHZ;
+#endif
+}
+#endif /* CONFIG_KERNEL_MCS */
 #endif /*  __ARCH_MODE_MACHINE_TIMER_H_ */
diff --git a/include/arch/arm/arch/machine/timer.h b/include/arch/arm/arch/machine/timer.h
index 8bb04c8e8e259a6cb3eb23c4c0327b84a424594c..ab546f9af33be1412bb8f837178793943be64f97 100644
--- a/include/arch/arm/arch/machine/timer.h
+++ b/include/arch/arm/arch/machine/timer.h
@@ -15,6 +15,48 @@
 
 #include <config.h>
 #include <stdint.h>
+
+#ifdef CONFIG_KERNEL_MCS
+#include <types.h>
+#include <util.h>
+#include <mode/util.h>
+
+#define USE_KHZ (TIMER_CLOCK_HZ % HZ_IN_MHZ > 0)
+#define TIMER_CLOCK_KHZ (TIMER_CLOCK_HZ / HZ_IN_KHZ)
+#define TIMER_CLOCK_MHZ (TIMER_CLOCK_HZ / HZ_IN_MHZ)
+
+#include <plat/platform_gen.h>
+#include <mode/machine/timer.h>
+
+void initTimer(void);
+
+/* get the max value usToTicks can be passed without overflowing */
+static inline CONST time_t getMaxUsToTicks(void)
+{
+#if USE_KHZ
+    return UINT64_MAX / TIMER_CLOCK_KHZ;
+#else
+    return UINT64_MAX / TIMER_CLOCK_MHZ;
+#endif
+}
+
+static inline CONST ticks_t usToTicks(time_t us)
+{
+#if USE_KHZ
+    /* reciprocal division overflows too quickly for dividing by KHZ_IN_MHZ.
+     * This operation isn't  used frequently or on many platforms, so use manual
+     * division here */
+    return div64(us * TIMER_CLOCK_KHZ, KHZ_IN_MHZ);
+#else
+    return us * TIMER_CLOCK_MHZ;
+#endif
+}
+
+static inline CONST ticks_t getTimerPrecision(void)
+{
+    return usToTicks(TIMER_PRECISION);
+}
+#else /* CONFIG_KERNEL_MCS */
 #include <mode/machine/timer.h>
 #include <plat/machine/hardware.h>
 
@@ -29,5 +71,6 @@
 #endif
 
 void initTimer(void);
+#endif
 
 #endif /* __ARCH_MACHINE_TIMER_H_ */
diff --git a/src/arch/arm/kernel/boot.c b/src/arch/arm/kernel/boot.c
index 02850890a757e0a6376bb96d348b345cf79acafb..058f45c5dba91163f4e7e1e6692c3b09d8b8c256 100644
--- a/src/arch/arm/kernel/boot.c
+++ b/src/arch/arm/kernel/boot.c
@@ -487,6 +487,10 @@ static BOOT_CODE bool_t try_init_kernel(
     }
     write_it_asid_pool(it_ap_cap, it_pd_cap);
 
+#ifdef CONFIG_KERNEL_MCS
+    NODE_STATE(ksCurTime) = getCurrentTime();
+#endif
+
     /* create the idle thread */
     if (!create_idle_thread()) {
         return false;
diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in
index 6cc74f29ccb974a6a96f77c79abfb2ff13c18015..4a1442e12ebabdcc2a0405bc3714510ad5513ce7 100644
--- a/src/arch/arm/platform_gen.h.in
+++ b/src/arch/arm/platform_gen.h.in
@@ -13,7 +13,13 @@
 #ifndef __ARM_PLAT_H
 #define __ARM_PLAT_H
 
+#include <autoconf.h>
+
 #define TIMER_CLOCK_HZ @CONFIGURE_TIMER_FREQUENCY@
+#define CLK_MAGIC @CONFIGURE_CLK_MAGIC@
+#define CLK_SHIFT @CONFIGURE_CLK_SHIFT@
+#define TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@
+
 enum IRQConstants {
     maxIRQ                      = @CONFIGURE_MAX_IRQ@
 } platform_interrupt_t;
@@ -27,4 +33,12 @@ enum IRQConstants {
 #if (defined(CONFIGURE_SMMU) && defined(CONFIG_ARM_SMMU))
 #include CONFIGURE_SMMU
 #endif
+
+#ifdef CONFIG_KERNEL_MCS
+static inline CONST time_t getKernelWcetUs(void)
+{
+    return @CONFIGURE_KERNEL_WCET@;
+}
+#endif
+
 #endif /* !__ARM_PLAT_H */