[atch-axel-93] make CONFIGURE_KERNEL_WCET generic

config.cmake

@@ -49,34 +49,28 @@ set_property(
 # These options are now set in seL4Config.cmake
 if(DEFINED CALLED_declare_default_headers)
     # calculate the irq cnode size based on MAX_NUM_IRQ
-    if("${KernelArch}" STREQUAL "riscv")
+    if(KernelArchRiscV)
         math(EXPR MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ} + 2")
-    else()
-        if(
-            DEFINED KernelMaxNumNodes
-            AND CONFIGURE_NUM_PPI GREATER "0"
-            AND "${KernelArch}" STREQUAL "arm"
-        )
+    elseif(KernelArchARM)
+        set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
+        if(DEFINED CONFIGURE_NUM_PPI)
+            # The PPIs are a part of CONFIGURE_MAX_IRQ, but they are separate
+            # for each core.
             math(
                 EXPR MAX_NUM_IRQ
-                "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
+                "${MAX_NUM_IRQ} + ((${KernelMaxNumNodes} - 1) * ${CONFIGURE_NUM_PPI})"
             )
-        else()
-            set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
         endif()
+    else()
+        # Don't make any assumption about other architectures.
+        message(FATAL_ERROR "unsupported architecture: '${KernelArch}'")
     endif()
     set(BITS "0")
     while(MAX_NUM_IRQ GREATER "0")
         math(EXPR BITS "${BITS} + 1")
         math(EXPR MAX_NUM_IRQ "${MAX_NUM_IRQ} >> 1")
     endwhile()
     set(CONFIGURE_IRQ_SLOT_BITS "${BITS}" CACHE INTERNAL "")
-    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

@@ -129,6 +129,17 @@ macro(declare_default_headers)
         ""
         ${ARGN}
     )
+
+    if(KernelArchARM)
+        if(NOT DEFINED CONFIGURE_NUM_PPI)
+            set(CONFIGURE_NUM_PPI "32")
+        endif()
+    else()
+        if(DEFINED CONFIGURE_NUM_PPI)
+            message(FATAL_ERROR "NUM_PPI is currently for ARM only")
+        endif()
+    endif()
+
     set(CALLED_declare_default_headers 1)
 endmacro()
 

include/arch/arm/arch/machine/timer.h

@@ -50,10 +50,6 @@ static inline CONST ticks_t usToTicks(time_t us)
 #endif
 }
 
-static inline CONST ticks_t getTimerPrecision(void)
-{
-    return usToTicks(TIMER_PRECISION) + TIMER_OVERHEAD_TICKS;
-}
 #else /* CONFIG_KERNEL_MCS */
 #include <mode/machine/timer.h>
 #include <plat/machine/hardware.h>

include/arch/riscv/arch/machine/timer.h

@@ -16,12 +16,6 @@
 /* The scheduler clock is greater than 1MHz */
 #define TICKS_IN_US (TIMER_CLOCK_HZ / (US_IN_MS * MS_IN_S))
 
-static inline CONST time_t getKernelWcetUs(void)
-{
-    /* Copied from x86_64. Hopefully it's an overestimate here. */
-    return  10u;
-}
-
 static inline PURE ticks_t usToTicks(time_t us)
 {
     return us * TICKS_IN_US;
@@ -32,10 +26,6 @@ static inline PURE time_t ticksToUs(ticks_t ticks)
     return div64(ticks, TICKS_IN_US);
 }
 
-static inline PURE ticks_t getTimerPrecision(void)
-{
-    return usToTicks(1);
-}
 
 /* Get the max. ticks_t value that can be expressed in time_t (time in us). This
  * is the max. value ticksToUs() can be passed without overflowing.

include/arch/x86/arch/machine/timer.h

@@ -14,10 +14,9 @@
 #include <mode/util.h>
 #include <arch/kernel/apic.h>
 
-static inline CONST time_t getKernelWcetUs(void)
-{
-    return  10u;
-}
+#ifndef CONFIGURE_TIMER_PRECISION
+#define CONFIGURE_TIMER_PRECISION   1
+#endif
 
 static inline PURE ticks_t usToTicks(time_t us)
 {
@@ -33,11 +32,6 @@ static inline PURE time_t getMaxUsToTicks(void)
     return div64(UINT64_MAX, x86KStscMhz);
 }
 
-static inline PURE ticks_t getTimerPrecision(void)
-{
-    return usToTicks(1u);
-}
-
 static inline void ackDeadlineIRQ(void)
 {
 }

include/kernel/sporadic.h

@@ -29,24 +29,50 @@
 #include <machine/timer.h>
 #include <model/statedata.h>
 
-/* To do an operation in the kernel, the thread must have
- * at least this much budget - see comment on refill_sufficient */
-#define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE)
-#define MIN_BUDGET    (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE)
-#if (CONFIG_KERNEL_STATIC_MAX_PERIOD_US) != 0
-#define MAX_PERIOD_US (CONFIG_KERNEL_STATIC_MAX_PERIOD_US)
-#else
+static inline CONST time_t getMinBudgetUs(void)
+{
+    time_t wcet_us = getKernelWcetUs();
+    /*
+     * The minimum budget is calculated based on the fact that the thread must
+     * have enough budget to do a kernel operation and thus must have at least
+     * enough budget to enter and exit the kernel after usage is charged to it.
+     */
+    return 2 * wcet_us * CONFIG_KERNEL_WCET_SCALE;
+}
+
+static inline PURE ticks_t getMinBudgetTicks(void)
+{
+    return usToTicks(getMinBudgetUs());
+}
+
 /* The maximum period determines the point at which the scheduling logic
  * will no longer function correctly (UINT64_MAX - 5 * MAX_PERIOD), so
  * we keep the maximum period relatively small to ensure that the system
  * can function for a reasonably long time.
  *
  * Anything below getMaxUsToTicks() / 8 would ensure that time up to
  * 2^63 would still be be valid as 5 * (getMaxUsToTicks()) must be less
- * than 2^62. */
-#define MAX_PERIOD_US (getMaxUsToTicks() / 8)
-#endif /* CONFIG_KERNEL_STATIC_MAX_PERIOD_US != 0 */
-#define MAX_RELEASE_TIME (UINT64_MAX - 5 * usToTicks(MAX_PERIOD_US))
+ * than 2^62.
+ */
+static inline CONST time_t getMaxPeriodUs(void)
+{
+#if (CONFIG_KERNEL_STATIC_MAX_PERIOD_US != 0)
+    return CONFIG_KERNEL_STATIC_MAX_PERIOD_US;
+#else
+    return getMaxUsToTicks() / 8;
+#endif
+}
+
+static inline PURE ticks_t getMaxReleaseTimeTicks(void)
+{
+    return UINT64_MAX - 5 * usToTicks(getMaxPeriodUs());
+}
+
+/* ToDo: remove old defines from the code */
+#define MIN_BUDGET_US       getMinBudgetUs()
+#define MIN_BUDGET          getMinBudgetTicks()
+#define MAX_PERIOD_US       getMaxPeriodUs()
+#define MAX_RELEASE_TIME    getMaxReleaseTimeTicks()
 
 /* Short hand for accessing refill queue items */
 static inline refill_t *refill_index(sched_context_t *sc, word_t index)
@@ -115,7 +141,7 @@ static inline ticks_t refill_capacity(sched_context_t *sc, ticks_t usage)
  */
 static inline bool_t refill_sufficient(sched_context_t *sc, ticks_t usage)
 {
-    return refill_capacity(sc, usage) >= MIN_BUDGET;
+    return refill_capacity(sc, usage) >= getMinBudgetTicks();
 }
 
 /*
@@ -144,14 +170,13 @@ static inline bool_t sc_active(sched_context_t *sc)
  */
 static inline bool_t sc_released(sched_context_t *sc)
 {
-    if (sc_active(sc)) {
-        /* All refills must all be greater than MIN_BUDGET so this
-         * should be true for all active SCs */
-        assert(refill_sufficient(sc, 0));
-        return refill_ready(sc);
-    } else {
+    if (unlikely(!sc_active(sc))) {
         return false;
     }
+    /* All refills must all be greater than getMinBudgetTicks() so this
+     * should be true for all active SCs */
+    assert(refill_sufficient(sc, 0));
+    return refill_ready(sc);
 }
 
 /*

include/machine/timer.h

@@ -25,12 +25,44 @@ static inline void setDeadline(ticks_t deadline);
 /** MODIFIES: [*] */
 static inline void ackDeadlineIRQ(void);
 
-/* get the expected wcet of the kernel for this platform */
-static PURE inline ticks_t getKernelWcetTicks(void)
+static inline CONST time_t getKernelWcetUs(void)
 {
-    return usToTicks(getKernelWcetUs());
+    /* On ARM and RISC-V the CMake macro declare_default_headers() allows
+     * platforms to set custom values for CONFIGURE_KERNEL_WCET. On x86 there
+     * is no such mechanism because there is the 'pc99' platform only, so a
+     * custom value could be defined in 'include/plat/pc99/plat/machine.h' or
+     * 'include/arch/x86/arch/machine/timer.h'
+     */
+#ifdef CONFIGURE_KERNEL_WCET
+    return CONFIGURE_KERNEL_WCET;
+#else
+    /*
+     * Using 10 us turned out to be a good default value, but it seems this has
+     * been copy/pasted ever since. At 1 GHz this corresponds to 10.000 cylces,
+     * which seems very far on safe side for modern platforms. But actuallay,
+     * it would be good to have a better explanation how to practically check
+     * how good this value is in a specific platform and a reasonable system
+     * configuration.
+     */
+    return 10;
+#endif
 }
-#else /* CONFIG_KERNEL_MCS */
+
+static inline CONST ticks_t getTimerPrecision(void)
+{
+    ticks_t precision = 0;
+#ifdef CONFIGURE_TIMER_PRECISION
+    precision += usToTicks(CONFIGURE_TIMER_PRECISION);
+#endif
+#ifdef CONFIGURE_TIMER_OVERHEAD_TICKS
+    precision += CONFIGURE_TIMER_OVERHEAD_TICKS;
+#endif
+    return precision;
+}
+
+#else /* not CONFIG_KERNEL_MCS */
+
 static inline void resetTimer(void);
-#endif /* !CONFIG_KERNEL_MCS */
+
+#endif /* [not] CONFIG_KERNEL_MCS */
 

include/plat/pc99/plat/machine.h

@@ -14,7 +14,7 @@
 /* interrupt vectors (corresponds to IDT entries) */
 
 #define IRQ_INT_OFFSET 0x20
-#define IRQ_CNODE_SLOT_BITS 8
+#define IRQ_CNODE_SLOTS BIT(8)
 
 typedef enum _interrupt_t {
     int_invalid                 = -1,

src/arch/arm/platform_gen.h.in

@@ -11,35 +11,26 @@
 #define TIMER_CLOCK_HZ ULL_CONST(@CONFIGURE_TIMER_FREQUENCY@)
 #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@
+
+#cmakedefine CONFIGURE_TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@
+#cmakedefine CONFIGURE_TIMER_OVERHEAD_TICKS @CONFIGURE_TIMER_OVERHEAD_TICKS@
+
+#ifdef CONFIG_KERNEL_MCS
+#cmakedefine CONFIGURE_KERNEL_WCET @CONFIGURE_KERNEL_WCET@
+#endif
 
 enum IRQConstants {
     maxIRQ                      = @CONFIGURE_MAX_IRQ@
 } platform_interrupt_t;
 
-#define IRQ_CNODE_SLOT_BITS (@CONFIGURE_IRQ_SLOT_BITS@)
-
 #include <@CONFIGURE_INTERRUPT_CONTROLLER@>
 #include <@CONFIGURE_TIMER@>
 
 #cmakedefine CONFIGURE_SMMU <@CONFIGURE_SMMU@>
-#if (defined(CONFIGURE_SMMU) && defined(CONFIG_TK1_SMMU))
+#if defined(CONFIGURE_SMMU) && (defined(CONFIG_TK1_SMMU) || defined(CONFIG_ARM_SMMU))
 #include CONFIGURE_SMMU
-#endif
-
-#cmakedefine CONFIGURE_SMMU <@CONFIGURE_SMMU@>
-#if (defined(CONFIGURE_SMMU) && defined(CONFIG_ARM_SMMU))
-#include CONFIGURE_SMMU
-
+#ifdef CONFIG_ARM_SMMU
 #define SMMU_MAX_SID  @CONFIGURE_MAX_SID@
 #define SMMU_MAX_CB  @CONFIGURE_MAX_CB@
-
-#endif
-
-#ifdef CONFIG_KERNEL_MCS
-static inline CONST time_t getKernelWcetUs(void)
-{
-    return @CONFIGURE_KERNEL_WCET@;
-}
-#endif
+#endif /* CONFIG_ARM_SMMU */
+#endif /* CONFIGURE_SMMU  && (CONFIG_TK1_SMMU || CONFIG_ARM_SMMU) */

src/arch/riscv/platform_gen.h.in

@@ -10,6 +10,13 @@
 
 #define TIMER_CLOCK_HZ ULL_CONST(@CONFIGURE_TIMER_FREQUENCY@)
 
+#cmakedefine CONFIGURE_TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@
+#cmakedefine CONFIGURE_TIMER_OVERHEAD_TICKS @CONFIGURE_TIMER_OVERHEAD_TICKS@
+
+#ifdef CONFIG_KERNEL_MCS
+#cmakedefine CONFIGURE_KERNEL_WCET @CONFIGURE_KERNEL_WCET@
+#endif
+
 #include <machine/interrupt.h>
 
 /*
@@ -41,6 +48,4 @@ enum irqNumbers {
     irqInvalid = 0
 };
 
-#define IRQ_CNODE_SLOT_BITS (@CONFIGURE_IRQ_SLOT_BITS@)
-
 #include <@CONFIGURE_INTERRUPT_CONTROLLER@>

src/model/statedata.c

@@ -76,10 +76,15 @@ UP_STATE_DEFINE(timestamp_t, benchmark_kernel_number_schedules);
 word_t ksWorkUnitsCompleted;
 
 irq_state_t intStateIRQTable[INT_STATE_ARRAY_SIZE];
-/* CNode containing interrupt handler endpoints - like all seL4 objects, this CNode needs to be
- * of a size that is a power of 2 and aligned to its size. */
-cte_t intStateIRQNode[BIT(IRQ_CNODE_SLOT_BITS)] ALIGN(BIT(IRQ_CNODE_SLOT_BITS + seL4_SlotBits));
-compile_assert(irqCNodeSize, sizeof(intStateIRQNode) >= ((INT_STATE_ARRAY_SIZE) *sizeof(cte_t)));
+/*
+ * This is semantically a CNode containing interrupt handler endpoints.
+ * However, it is kernel internal only and never exposed to userland, so it
+ * can be allocated statically. The convention for all CNodes is, that their
+ * size is a a power of 2 and they are aligned aligned to its size. But that
+ * seems driven a by the way memory management and allocation works, so this
+ * is not necessary here.
+ */
+cte_t intStateIRQNode[INT_STATE_ARRAY_SIZE];
 
 /* Currently active domain */
 dom_t ksCurDomain;

src/object/interrupt.c

@@ -201,13 +201,15 @@ void handleInterrupt(irq_t irq)
         return;
     }
 
-    switch (intStateIRQTable[IRQT_TO_IDX(irq)]) {
+    word_t idx = IRQT_TO_IDX(irq);
+
+    switch (intStateIRQTable[idx]) {
     case IRQSignal: {
         /* Merging the variable declaration and initialization into one line
          * requires an update in the proofs first. Might be a c89 legacy.
          */
         cap_t cap;
-        cap = intStateIRQNode[IRQT_TO_IDX(irq)].cap;
+        cap = intStateIRQNode[idx].cap;
         if (cap_get_capType(cap) == cap_notification_cap &&
             cap_notification_cap_get_capNtfnCanSend(cap)) {
             sendSignal(NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)),

src/plat/allwinnerA20/config.cmake

@@ -24,7 +24,6 @@ if(KernelPlatformAllwinnerA20)
     declare_default_headers(
         TIMER_FREQUENCY 24000000
         MAX_IRQ 122
-        NUM_PPI 32
         TIMER drivers/timer/arm_generic.h
         INTERRUPT_CONTROLLER arch/machine/gic_v2.h
     )

src/plat/am335x/config.cmake

@@ -52,7 +52,6 @@ if(KernelPlatformAM335X)
         TIMER_FREQUENCY 24000000
         CLK_MAGIC 2863311531llu
         CLK_SHIFT 36u
-        KERNEL_WCET 10u
     )
 endif()