MCS, ARM: Introduce TIMER_OVERHEAD_TICKS

For ARM currently TIMER_PRECISION exists, but that is in microseconds
and not fine-grained enough.

This is needed to make periodic tasks synchronous with the system clock.
If this value is zero every period will be extended with the overhead of
taking an interrupt and reading the system clock. To avoid this drift,
the configured value should be set to at least the average overhead.

See also issue #844.

Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>

.cmake-format.yaml

@@ -52,5 +52,6 @@ additional_commands:
         CLK_MAGIC: '*'
         CLK_SHIFT: '*'
         TIMER_PRECISION: '*'
+        TIMER_OVERHEAD_TICKS: '*'
         MAX_SID: '*'
         MAX_CB: '*'

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

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}
     )

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>

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@

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