How to port a platform to mcs?

seL4 kernel
1

I’m interested in the rockpro64 platform and I see that it doesn’t currently support mcs. What is required to turn mcs on for a platform?

2

Adding MCS platform support requires adding a timer driver that implements the following functions:

ticks_t getCurrentTime(void);
void setDeadline(ticks_t deadline);
void ackDeadlineIRQ(void);
time_t getKernelWcetUs(void);

For an Arm platform such as the rockpro64, the Arm generic timer driver already implements these functions. The platform configuration needs to provide a constant for KERNEL_WCET (currently this is set to 10us on all platforms), and if it is a 32 bit platform constants for CLK_MAGIC and CLK_SHIFT. These can be obtained by running the reciprocal.py script located in the kernel repository at tools/reciprocal.py. Invoking this script with the platform’s generic timer frequency will provide the magic number and shift amount. The script will then try and validate that the values work for all 32bit divisions and may take a while to finish (on the order of 30mins). Setting these parameters is done in the platform’s config.cmake file. An example change is shown here:

--- a/src/plat/imx8m-evk/config.cmake
+++ b/src/plat/imx8m-evk/config.cmake
@@ -23,9 +23,7 @@ if(KernelPlatformImx8mq-evk OR KernelPlatformImx8mm-evk)
     else()
         fallback_declare_seL4_arch_default(aarch64)
     endif()
-    # MCS is not supported on imx8m.
-    # It requires a timer driver that implements the tickless programming requirements.
-    set(KernelPlatformSupportsMCS OFF)
+
     set(KernelArmCortexA53 ON)
     set(KernelArchArmV8a ON)
     config_set(KernelARMPlatform ARM_PLAT ${KernelPlatform})
@@ -41,6 +39,9 @@ if(KernelPlatformImx8mq-evk OR KernelPlatformImx8mm-evk)
         TIMER drivers/timer/arm_generic.h
         INTERRUPT_CONTROLLER arch/machine/gic_v3.h
         NUM_PPI 32
+        CLK_MAGIC 1llu
+        CLK_SHIFT 3u
+        KERNEL_WCET 10u
     )

Then you would need to run seL4test with MCS enabled (-DMCS=ON) and see that the tests pass.