diff --git a/.cmake-format.yaml b/.cmake-format.yaml
index cb4813890..eb4985d57 100644
--- a/.cmake-format.yaml
+++ b/.cmake-format.yaml
@@ -52,5 +52,6 @@ additional_commands:
         CLK_MAGIC: '*'
         CLK_SHIFT: '*'
         TIMER_PRECISION: '*'
+        TIMER_OVERHEAD_TICKS: '*'
         MAX_SID: '*'
         MAX_CB: '*'
diff --git a/config.cmake b/config.cmake
index 589a93f63..4b8d0cec0 100644
--- a/config.cmake
+++ b/config.cmake
@@ -74,6 +74,9 @@ if(DEFINED CALLED_declare_default_headers)
     if(NOT DEFINED CONFIGURE_TIMER_PRECISION)
         set(CONFIGURE_TIMER_PRECISION "0")
     endif()
+    if(NOT DEFINED CONFIGURE_TIMER_OVERHEAD_TICKS)
+        set(CONFIGURE_TIMER_OVERHEAD_TICKS "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 1a4d879fd..cdbc14dcc 100644
--- a/configs/seL4Config.cmake
+++ b/configs/seL4Config.cmake
@@ -118,7 +118,7 @@ macro(declare_default_headers)
     cmake_parse_arguments(
         CONFIGURE
         ""
-        "TIMER_FREQUENCY;MAX_IRQ;NUM_PPI;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU;CLK_SHIFT;CLK_MAGIC;KERNEL_WCET;TIMER_PRECISION;MAX_SID;MAX_CB"
+        "TIMER_FREQUENCY;MAX_IRQ;NUM_PPI;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU;CLK_SHIFT;CLK_MAGIC;KERNEL_WCET;TIMER_PRECISION;TIMER_OVERHEAD_TICKS;MAX_SID;MAX_CB"
         ""
         ${ARGN}
     )
diff --git a/include/arch/arm/arch/machine/timer.h b/include/arch/arm/arch/machine/timer.h
index b184576c5..0df9b80df 100644
--- a/include/arch/arm/arch/machine/timer.h
+++ b/include/arch/arm/arch/machine/timer.h
@@ -50,7 +50,7 @@ static inline CONST ticks_t usToTicks(time_t us)
 
 static inline CONST ticks_t getTimerPrecision(void)
 {
-    return usToTicks(TIMER_PRECISION);
+    return usToTicks(TIMER_PRECISION) + TIMER_OVERHEAD_TICKS;
 }
 #else /* CONFIG_KERNEL_MCS */
 #include <mode/machine/timer.h>
diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in
index 9c44d5475..bfb0c0bf6 100644
--- a/src/arch/arm/platform_gen.h.in
+++ b/src/arch/arm/platform_gen.h.in
@@ -12,6 +12,7 @@
 #define CLK_MAGIC @CONFIGURE_CLK_MAGIC@
 #define CLK_SHIFT @CONFIGURE_CLK_SHIFT@
 #define TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@
+#define TIMER_OVERHEAD_TICKS @CONFIGURE_TIMER_OVERHEAD_TICKS@
 
 enum IRQConstants {
     maxIRQ                      = @CONFIGURE_MAX_IRQ@
diff --git a/src/plat/tqma8xqp1gb/config.cmake b/src/plat/tqma8xqp1gb/config.cmake
index c50230859..6b4b54e93 100644
--- a/src/plat/tqma8xqp1gb/config.cmake
+++ b/src/plat/tqma8xqp1gb/config.cmake
@@ -22,6 +22,7 @@ if(KernelPlatformTqma8xqp1gb)
         TIMER_FREQUENCY 8000000
         MAX_IRQ 512
         TIMER drivers/timer/arm_generic.h
+        TIMER_OVERHEAD_TICKS 1
         INTERRUPT_CONTROLLER arch/machine/gic_v3.h
         NUM_PPI 32
         CLK_MAGIC 1llu