From 3c042e03161bc4da056a0659e0c3b7ce489fbaed Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 30 Nov 2023 13:51:57 +0100 Subject: [PATCH 01/10] arm: remove duplicate define for CONFIGURE_SMMU Also remove redundancies Signed-off-by: Axel Heider --- src/arch/arm/platform_gen.h.in | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in index bfb0c0bf6b..9f3ae321bd 100644 --- a/src/arch/arm/platform_gen.h.in +++ b/src/arch/arm/platform_gen.h.in @@ -24,18 +24,13 @@ enum IRQConstants { #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 +#endif /* CONFIG_ARM_SMMU */ +#endif /* CONFIGURE_SMMU && (CONFIG_TK1_SMMU || CONFIG_ARM_SMMU) */ #ifdef CONFIG_KERNEL_MCS static inline CONST time_t getKernelWcetUs(void) From 51307929087562b29c7c656f15bb63d2d2568639 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 16 Nov 2023 21:57:54 +0100 Subject: [PATCH 02/10] provide a default for CONFIGURE_KERNEL_WCET As this tends to be copy-pasted for every new platform, remove the explicit need to set something and provide a default instead. Signed-off-by: Axel Heider --- include/arch/riscv/arch/machine/timer.h | 6 ------ include/arch/x86/arch/machine/timer.h | 5 ----- include/machine/timer.h | 23 +++++++++++++++++++++++ src/arch/arm/platform_gen.h.in | 11 ++++------- src/arch/riscv/platform_gen.h.in | 4 ++++ src/plat/am335x/config.cmake | 1 - src/plat/bcm2711/config.cmake | 1 - src/plat/bcm2837/config.cmake | 1 - src/plat/exynos4/config.cmake | 1 - src/plat/exynos5/config.cmake | 1 - src/plat/hikey/config.cmake | 1 - src/plat/imx6/config.cmake | 1 - src/plat/imx7/config.cmake | 1 - src/plat/imx8m-evk/config.cmake | 1 - src/plat/maaxboard/config.cmake | 1 - src/plat/odroidc2/config.cmake | 1 - src/plat/odroidc4/config.cmake | 1 - src/plat/omap3/config.cmake | 1 - src/plat/qemu-arm-virt/config.cmake | 1 - src/plat/quartz64/config.cmake | 1 - src/plat/rockpro64/config.cmake | 1 - src/plat/tk1/config.cmake | 2 +- src/plat/tqma8xqp1gb/config.cmake | 1 - src/plat/tx1/config.cmake | 1 - src/plat/tx2/config.cmake | 1 - src/plat/zynq7000/config.cmake | 1 - src/plat/zynqmp/config.cmake | 1 - 27 files changed, 32 insertions(+), 40 deletions(-) diff --git a/include/arch/riscv/arch/machine/timer.h b/include/arch/riscv/arch/machine/timer.h index eb287c0c8c..d80ddd9a4e 100644 --- a/include/arch/riscv/arch/machine/timer.h +++ b/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; diff --git a/include/arch/x86/arch/machine/timer.h b/include/arch/x86/arch/machine/timer.h index 5771277b58..6274cbaf89 100644 --- a/include/arch/x86/arch/machine/timer.h +++ b/include/arch/x86/arch/machine/timer.h @@ -14,11 +14,6 @@ #include #include -static inline CONST time_t getKernelWcetUs(void) -{ - return 10u; -} - static inline PURE ticks_t usToTicks(time_t us) { assert(x86KStscMhz > 0); diff --git a/include/machine/timer.h b/include/machine/timer.h index 70f412b69f..30c49e9cc4 100644 --- a/include/machine/timer.h +++ b/include/machine/timer.h @@ -25,6 +25,29 @@ static inline void setDeadline(ticks_t deadline); /** MODIFIES: [*] */ static inline void ackDeadlineIRQ(void); +static inline CONST time_t getKernelWcetUs(void) +{ + /* 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 +} + /* get the expected wcet of the kernel for this platform */ static PURE inline ticks_t getKernelWcetTicks(void) { diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in index 9f3ae321bd..2d8ec0e314 100644 --- a/src/arch/arm/platform_gen.h.in +++ b/src/arch/arm/platform_gen.h.in @@ -14,6 +14,10 @@ #define TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@ #define 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; @@ -31,10 +35,3 @@ enum IRQConstants { #define SMMU_MAX_CB @CONFIGURE_MAX_CB@ #endif /* CONFIG_ARM_SMMU */ #endif /* CONFIGURE_SMMU && (CONFIG_TK1_SMMU || CONFIG_ARM_SMMU) */ - -#ifdef CONFIG_KERNEL_MCS -static inline CONST time_t getKernelWcetUs(void) -{ - return @CONFIGURE_KERNEL_WCET@; -} -#endif diff --git a/src/arch/riscv/platform_gen.h.in b/src/arch/riscv/platform_gen.h.in index 491c019946..8ed49a6384 100644 --- a/src/arch/riscv/platform_gen.h.in +++ b/src/arch/riscv/platform_gen.h.in @@ -10,6 +10,10 @@ #define TIMER_CLOCK_HZ ULL_CONST(@CONFIGURE_TIMER_FREQUENCY@) +#ifdef CONFIG_KERNEL_MCS +#cmakedefine CONFIGURE_KERNEL_WCET @CONFIGURE_KERNEL_WCET@ +#endif + #include /* diff --git a/src/plat/am335x/config.cmake b/src/plat/am335x/config.cmake index 89f362f19d..49639de9c3 100644 --- a/src/plat/am335x/config.cmake +++ b/src/plat/am335x/config.cmake @@ -52,7 +52,6 @@ if(KernelPlatformAM335X) TIMER_FREQUENCY 24000000 CLK_MAGIC 2863311531llu CLK_SHIFT 36u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/bcm2711/config.cmake b/src/plat/bcm2711/config.cmake index d66df9de92..6cf7cc4bdb 100644 --- a/src/plat/bcm2711/config.cmake +++ b/src/plat/bcm2711/config.cmake @@ -52,7 +52,6 @@ if(KernelPlatformRpi4) NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h - KERNEL_WCET 10u CLK_MAGIC 5337599559llu CLK_SHIFT 58u ) diff --git a/src/plat/bcm2837/config.cmake b/src/plat/bcm2837/config.cmake index 56d0098ed3..88679e1ad4 100644 --- a/src/plat/bcm2837/config.cmake +++ b/src/plat/bcm2837/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformRpi3) NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER drivers/irq/bcm2836-armctrl-ic.h - KERNEL_WCET 10u CLK_MAGIC 458129845llu CLK_SHIFT 43u ) diff --git a/src/plat/exynos4/config.cmake b/src/plat/exynos4/config.cmake index b260f17791..4df8383fe5 100644 --- a/src/plat/exynos4/config.cmake +++ b/src/plat/exynos4/config.cmake @@ -22,7 +22,6 @@ if(KernelPlatformExynos4) NUM_PPI 32 TIMER drivers/timer/exynos4412-mct.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h - KERNEL_WCET 10u CLK_MAGIC 2863311531llu CLK_SHIFT 36u ) diff --git a/src/plat/exynos5/config.cmake b/src/plat/exynos5/config.cmake index dbb6ec02ee..d092e3bb0f 100644 --- a/src/plat/exynos5/config.cmake +++ b/src/plat/exynos5/config.cmake @@ -59,7 +59,6 @@ if(KernelPlatExynos5) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 2863311531llu CLK_SHIFT 36u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/hikey/config.cmake b/src/plat/hikey/config.cmake index 3eff84c5df..cdc810ac19 100644 --- a/src/plat/hikey/config.cmake +++ b/src/plat/hikey/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformHikey) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 458129845llu CLK_SHIFT 39u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/imx6/config.cmake b/src/plat/imx6/config.cmake index e5b01420cb..98dc70c86c 100644 --- a/src/plat/imx6/config.cmake +++ b/src/plat/imx6/config.cmake @@ -72,7 +72,6 @@ if(KernelPlatImx6) TIMER ${timer_file} CLK_SHIFT 41llu CLK_MAGIC 4415709349llu - KERNEL_WCET 10llu TIMER_PRECISION 2u ) endif() diff --git a/src/plat/imx7/config.cmake b/src/plat/imx7/config.cmake index 4ba6e7c875..5bd606db2f 100644 --- a/src/plat/imx7/config.cmake +++ b/src/plat/imx7/config.cmake @@ -25,7 +25,6 @@ if(KernelPlatImx7) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 1llu CLK_SHIFT 8u - KERNEL_WCET 10u ) else() config_set(KernelPlatImx7 PLAT_IMX7 OFF) diff --git a/src/plat/imx8m-evk/config.cmake b/src/plat/imx8m-evk/config.cmake index 73acd39797..bae963e403 100644 --- a/src/plat/imx8m-evk/config.cmake +++ b/src/plat/imx8m-evk/config.cmake @@ -40,7 +40,6 @@ if(KernelPlatformImx8mq-evk OR KernelPlatformImx8mm-evk OR KernelPlatformImx8mp- NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/maaxboard/config.cmake b/src/plat/maaxboard/config.cmake index 32b1f17e0e..108ad21f60 100644 --- a/src/plat/maaxboard/config.cmake +++ b/src/plat/maaxboard/config.cmake @@ -31,7 +31,6 @@ if(KernelPlatformMaaxboard) NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/odroidc2/config.cmake b/src/plat/odroidc2/config.cmake index 2ffb76643c..eef4995ab1 100644 --- a/src/plat/odroidc2/config.cmake +++ b/src/plat/odroidc2/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformOdroidc2) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 375299969u CLK_SHIFT 53u - KERNEL_WCET 10u TIMER_PRECISION 1u ) endif() diff --git a/src/plat/odroidc4/config.cmake b/src/plat/odroidc4/config.cmake index 06b5efdb17..d5fbf9e2c8 100644 --- a/src/plat/odroidc4/config.cmake +++ b/src/plat/odroidc4/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformOdroidc4) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 375299969u CLK_SHIFT 53u - KERNEL_WCET 10u TIMER_PRECISION 1u ) endif() diff --git a/src/plat/omap3/config.cmake b/src/plat/omap3/config.cmake index 0bf16034c1..4e96343dce 100644 --- a/src/plat/omap3/config.cmake +++ b/src/plat/omap3/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformOMAP3) TIMER drivers/timer/omap3430.h CLK_MAGIC 1321528399llu CLK_SHIFT 34u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/qemu-arm-virt/config.cmake b/src/plat/qemu-arm-virt/config.cmake index 7eec8a57f3..e1b50d49ba 100644 --- a/src/plat/qemu-arm-virt/config.cmake +++ b/src/plat/qemu-arm-virt/config.cmake @@ -259,7 +259,6 @@ if(KernelPlatformQEMUArmVirt) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 4611686019llu CLK_SHIFT 58u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/quartz64/config.cmake b/src/plat/quartz64/config.cmake index 4bf4e2d2d2..03a37e5238 100644 --- a/src/plat/quartz64/config.cmake +++ b/src/plat/quartz64/config.cmake @@ -21,7 +21,6 @@ if(KernelPlatformQuartz64) TIMER_FREQUENCY 24000000 MAX_IRQ 231 NUM_PPI 32 - KERNEL_WCET 10u TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h ) diff --git a/src/plat/rockpro64/config.cmake b/src/plat/rockpro64/config.cmake index 5959c6d69a..69bee63e94 100644 --- a/src/plat/rockpro64/config.cmake +++ b/src/plat/rockpro64/config.cmake @@ -21,7 +21,6 @@ if(KernelPlatformRockpro64) TIMER_FREQUENCY 24000000 MAX_IRQ 181 NUM_PPI 32 - KERNEL_WCET 10u TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h ) diff --git a/src/plat/tk1/config.cmake b/src/plat/tk1/config.cmake index 024b19159c..ad5aef8927 100644 --- a/src/plat/tk1/config.cmake +++ b/src/plat/tk1/config.cmake @@ -26,7 +26,7 @@ if(KernelPlatformTK1) SMMU plat/machine/smmu.h CLK_MAGIC 2863311531llu CLK_SHIFT 35u - KERNEL_WCET 100u + KERNEL_WCET 100 ) endif() diff --git a/src/plat/tqma8xqp1gb/config.cmake b/src/plat/tqma8xqp1gb/config.cmake index 746c608b2f..3a43827a2f 100644 --- a/src/plat/tqma8xqp1gb/config.cmake +++ b/src/plat/tqma8xqp1gb/config.cmake @@ -27,7 +27,6 @@ if(KernelPlatformTqma8xqp1gb) NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/tx1/config.cmake b/src/plat/tx1/config.cmake index e311b23be9..6c580323c1 100644 --- a/src/plat/tx1/config.cmake +++ b/src/plat/tx1/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformTx1) TIMER drivers/timer/arm_generic.h CLK_MAGIC 2863311531llu CLK_SHIFT 35u - KERNEL_WCET 10u ) endif() diff --git a/src/plat/tx2/config.cmake b/src/plat/tx2/config.cmake index 0bd1531211..ae7351efeb 100644 --- a/src/plat/tx2/config.cmake +++ b/src/plat/tx2/config.cmake @@ -27,7 +27,6 @@ if(KernelPlatformTx2) TIMER drivers/timer/arm_generic.h CLK_SHIFT 57u CLK_MAGIC 4611686019u - KERNEL_WCET 10u SMMU drivers/smmu/smmuv2.h MAX_SID 128 MAX_CB 64 diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake index 1491dfb6cd..e5433607bf 100644 --- a/src/plat/zynq7000/config.cmake +++ b/src/plat/zynq7000/config.cmake @@ -32,7 +32,6 @@ if(KernelPlatformZynq7000) TIMER ${timer_file} CLK_SHIFT 40llu CLK_MAGIC 3435973837llu - KERNEL_WCET 10llu ) endif() diff --git a/src/plat/zynqmp/config.cmake b/src/plat/zynqmp/config.cmake index 67d839e556..b2dfb2b381 100644 --- a/src/plat/zynqmp/config.cmake +++ b/src/plat/zynqmp/config.cmake @@ -63,7 +63,6 @@ if(KernelPlatformZynqmp) INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 1374389535llu CLK_SHIFT 37u - KERNEL_WCET 10u ) endif() From 5c15427bd3005a882d7fadadd00f3e7b0ef2ec27 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Mon, 27 Nov 2023 19:25:25 +0100 Subject: [PATCH 03/10] WCET: try to simplify code --- include/kernel/sporadic.h | 61 +++++++++++++++++++++++++++------------ include/machine/timer.h | 11 +++---- 2 files changed, 47 insertions(+), 25 deletions(-) diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h index 35518b7b86..e13e2a524b 100644 --- a/include/kernel/sporadic.h +++ b/include/kernel/sporadic.h @@ -29,13 +29,22 @@ #include #include -/* 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 @@ -43,10 +52,27 @@ * * 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); } /* diff --git a/include/machine/timer.h b/include/machine/timer.h index 30c49e9cc4..e7e230ec20 100644 --- a/include/machine/timer.h +++ b/include/machine/timer.h @@ -48,12 +48,9 @@ static inline CONST time_t getKernelWcetUs(void) #endif } -/* get the expected wcet of the kernel for this platform */ -static PURE inline ticks_t getKernelWcetTicks(void) -{ - return usToTicks(getKernelWcetUs()); -} -#else /* CONFIG_KERNEL_MCS */ +#else /* not CONFIG_KERNEL_MCS */ + static inline void resetTimer(void); -#endif /* !CONFIG_KERNEL_MCS */ + +#endif /* [not] CONFIG_KERNEL_MCS */ From b009696874bb1f232facd2312eaf31d6ac30af80 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 17 Nov 2023 20:55:01 +0100 Subject: [PATCH 04/10] make getTimerPrecision() generic Signed-off-by: Axel Heider --- config.cmake | 6 ------ include/arch/arm/arch/machine/timer.h | 4 ---- include/arch/riscv/arch/machine/timer.h | 8 ++++---- include/arch/x86/arch/machine/timer.h | 9 ++++----- include/machine/timer.h | 12 ++++++++++++ src/arch/arm/platform_gen.h.in | 5 +++-- src/arch/riscv/platform_gen.h.in | 3 +++ 7 files changed, 26 insertions(+), 21 deletions(-) diff --git a/config.cmake b/config.cmake index 30e7f624d6..4a43ef3f25 100644 --- a/config.cmake +++ b/config.cmake @@ -71,12 +71,6 @@ if(DEFINED CALLED_declare_default_headers) 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 diff --git a/include/arch/arm/arch/machine/timer.h b/include/arch/arm/arch/machine/timer.h index 553d85291b..3506714ca9 100644 --- a/include/arch/arm/arch/machine/timer.h +++ b/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 #include diff --git a/include/arch/riscv/arch/machine/timer.h b/include/arch/riscv/arch/machine/timer.h index d80ddd9a4e..d16d9284ee 100644 --- a/include/arch/riscv/arch/machine/timer.h +++ b/include/arch/riscv/arch/machine/timer.h @@ -13,6 +13,10 @@ #include #include +#ifndef CONFIGURE_TIMER_PRECISION +#define CONFIGURE_TIMER_PRECISION 1 +#endif + /* The scheduler clock is greater than 1MHz */ #define TICKS_IN_US (TIMER_CLOCK_HZ / (US_IN_MS * MS_IN_S)) @@ -26,10 +30,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. diff --git a/include/arch/x86/arch/machine/timer.h b/include/arch/x86/arch/machine/timer.h index 6274cbaf89..504ccef910 100644 --- a/include/arch/x86/arch/machine/timer.h +++ b/include/arch/x86/arch/machine/timer.h @@ -14,6 +14,10 @@ #include #include +#ifndef CONFIGURE_TIMER_PRECISION +#define CONFIGURE_TIMER_PRECISION 1 +#endif + static inline PURE ticks_t usToTicks(time_t us) { assert(x86KStscMhz > 0); @@ -28,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) { } diff --git a/include/machine/timer.h b/include/machine/timer.h index e7e230ec20..cf0462e026 100644 --- a/include/machine/timer.h +++ b/include/machine/timer.h @@ -48,6 +48,18 @@ static inline CONST time_t getKernelWcetUs(void) #endif } +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); diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in index 2d8ec0e314..d599bddb31 100644 --- a/src/arch/arm/platform_gen.h.in +++ b/src/arch/arm/platform_gen.h.in @@ -11,8 +11,9 @@ #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@ diff --git a/src/arch/riscv/platform_gen.h.in b/src/arch/riscv/platform_gen.h.in index 8ed49a6384..16e2f57e69 100644 --- a/src/arch/riscv/platform_gen.h.in +++ b/src/arch/riscv/platform_gen.h.in @@ -10,6 +10,9 @@ #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 From 0040a3302014110e821495e66ed71bda16df8015 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 17 Nov 2023 20:56:02 +0100 Subject: [PATCH 05/10] riscv: make timer precision default to 0 Align RISC-V with ARM behavior Signed-off-by: Axel Heider --- include/arch/riscv/arch/machine/timer.h | 4 ---- 1 file changed, 4 deletions(-) diff --git a/include/arch/riscv/arch/machine/timer.h b/include/arch/riscv/arch/machine/timer.h index d16d9284ee..a64e49ab48 100644 --- a/include/arch/riscv/arch/machine/timer.h +++ b/include/arch/riscv/arch/machine/timer.h @@ -13,10 +13,6 @@ #include #include -#ifndef CONFIGURE_TIMER_PRECISION -#define CONFIGURE_TIMER_PRECISION 1 -#endif - /* The scheduler clock is greater than 1MHz */ #define TICKS_IN_US (TIMER_CLOCK_HZ / (US_IN_MS * MS_IN_S)) From b51ff66b949bda705269a3ce5fa5eeab07cea9c6 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 1 Dec 2023 15:40:55 +0100 Subject: [PATCH 06/10] cmake: use flags instead of strings Signed-off-by: Axel Heider --- config.cmake | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/config.cmake b/config.cmake index 4a43ef3f25..151f89a589 100644 --- a/config.cmake +++ b/config.cmake @@ -49,14 +49,10 @@ 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" - ) + if(DEFINED KernelMaxNumNodes AND CONFIGURE_NUM_PPI GREATER "0" AND KernelArchARM) math( EXPR MAX_NUM_IRQ "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}" From fa1eec02626b9c296d11c8577769bba132481550 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 17 Nov 2023 22:02:52 +0100 Subject: [PATCH 07/10] cmake: make MAX_NUM_IRQ calculation arch specific - KernelMaxNumNodes is always defined, it's at lest 1 - check CONFIGURE_NUM_PPI explicitly Signed-off-by: Axel Heider --- config.cmake | 14 +++++++++----- configs/seL4Config.cmake | 11 +++++++++++ 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/config.cmake b/config.cmake index 151f89a589..baf2e86d49 100644 --- a/config.cmake +++ b/config.cmake @@ -51,15 +51,19 @@ if(DEFINED CALLED_declare_default_headers) # calculate the irq cnode size based on MAX_NUM_IRQ if(KernelArchRiscV) math(EXPR MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ} + 2") - else() - if(DEFINED KernelMaxNumNodes AND CONFIGURE_NUM_PPI GREATER "0" AND KernelArchARM) + 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") diff --git a/configs/seL4Config.cmake b/configs/seL4Config.cmake index 6432191896..7c25c4a3dd 100644 --- a/configs/seL4Config.cmake +++ b/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() From 08631c2ff70b955ead736e51596d5dce34f2ffa1 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 17 Nov 2023 22:10:22 +0100 Subject: [PATCH 08/10] drop IRQ_CNODE_SLOT_BITS --- include/plat/pc99/plat/machine.h | 2 +- src/arch/arm/platform_gen.h.in | 2 -- src/arch/riscv/platform_gen.h.in | 2 -- src/model/statedata.c | 13 +++++++++---- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/include/plat/pc99/plat/machine.h b/include/plat/pc99/plat/machine.h index aebcb55106..2681dc63cf 100644 --- a/include/plat/pc99/plat/machine.h +++ b/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, diff --git a/src/arch/arm/platform_gen.h.in b/src/arch/arm/platform_gen.h.in index d599bddb31..a87ce442e0 100644 --- a/src/arch/arm/platform_gen.h.in +++ b/src/arch/arm/platform_gen.h.in @@ -23,8 +23,6 @@ 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@> diff --git a/src/arch/riscv/platform_gen.h.in b/src/arch/riscv/platform_gen.h.in index 16e2f57e69..fc8ff77020 100644 --- a/src/arch/riscv/platform_gen.h.in +++ b/src/arch/riscv/platform_gen.h.in @@ -48,6 +48,4 @@ enum irqNumbers { irqInvalid = 0 }; -#define IRQ_CNODE_SLOT_BITS (@CONFIGURE_IRQ_SLOT_BITS@) - #include <@CONFIGURE_INTERRUPT_CONTROLLER@> diff --git a/src/model/statedata.c b/src/model/statedata.c index 88d7bbdc8f..d6d88a47b2 100644 --- a/src/model/statedata.c +++ b/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; From 27288a91fb38553280157bb7ae36b11b2f338128 Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Fri, 17 Nov 2023 21:42:07 +0100 Subject: [PATCH 09/10] remove NUM_PPI --- src/plat/allwinnerA20/config.cmake | 1 - src/plat/apq8064/config.cmake | 1 - src/plat/bcm2711/config.cmake | 1 - src/plat/bcm2837/config.cmake | 1 - src/plat/exynos4/config.cmake | 1 - src/plat/exynos5/config.cmake | 1 - src/plat/imx6/config.cmake | 1 - src/plat/imx7/config.cmake | 1 - src/plat/imx8m-evk/config.cmake | 1 - src/plat/maaxboard/config.cmake | 1 - src/plat/odroidc2/config.cmake | 1 - src/plat/odroidc4/config.cmake | 1 - src/plat/qemu-arm-virt/config.cmake | 1 - src/plat/quartz64/config.cmake | 1 - src/plat/rockpro64/config.cmake | 1 - src/plat/tk1/config.cmake | 1 - src/plat/tqma8xqp1gb/config.cmake | 1 - src/plat/tx1/config.cmake | 1 - src/plat/tx2/config.cmake | 1 - src/plat/zynq7000/config.cmake | 1 - src/plat/zynqmp/config.cmake | 1 - 21 files changed, 21 deletions(-) diff --git a/src/plat/allwinnerA20/config.cmake b/src/plat/allwinnerA20/config.cmake index 9032a248d6..5c78dcee98 100644 --- a/src/plat/allwinnerA20/config.cmake +++ b/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 ) diff --git a/src/plat/apq8064/config.cmake b/src/plat/apq8064/config.cmake index 67a01f5db2..9a1fea7534 100644 --- a/src/plat/apq8064/config.cmake +++ b/src/plat/apq8064/config.cmake @@ -25,7 +25,6 @@ if(KernelPlatformAPQ8064) declare_default_headers( TIMER_FREQUENCY 7000000 MAX_IRQ 283 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h ) diff --git a/src/plat/bcm2711/config.cmake b/src/plat/bcm2711/config.cmake index 6cf7cc4bdb..8c9a3de3f6 100644 --- a/src/plat/bcm2711/config.cmake +++ b/src/plat/bcm2711/config.cmake @@ -49,7 +49,6 @@ if(KernelPlatformRpi4) declare_default_headers( TIMER_FREQUENCY 54000000 MAX_IRQ 216 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 5337599559llu diff --git a/src/plat/bcm2837/config.cmake b/src/plat/bcm2837/config.cmake index 88679e1ad4..53b9a7833c 100644 --- a/src/plat/bcm2837/config.cmake +++ b/src/plat/bcm2837/config.cmake @@ -21,7 +21,6 @@ if(KernelPlatformRpi3) declare_default_headers( TIMER_FREQUENCY 19200000 MAX_IRQ 127 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER drivers/irq/bcm2836-armctrl-ic.h CLK_MAGIC 458129845llu diff --git a/src/plat/exynos4/config.cmake b/src/plat/exynos4/config.cmake index 4df8383fe5..b1ab8b31ad 100644 --- a/src/plat/exynos4/config.cmake +++ b/src/plat/exynos4/config.cmake @@ -19,7 +19,6 @@ if(KernelPlatformExynos4) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 159 - NUM_PPI 32 TIMER drivers/timer/exynos4412-mct.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 2863311531llu diff --git a/src/plat/exynos5/config.cmake b/src/plat/exynos5/config.cmake index d092e3bb0f..0f4986e77c 100644 --- a/src/plat/exynos5/config.cmake +++ b/src/plat/exynos5/config.cmake @@ -54,7 +54,6 @@ if(KernelPlatExynos5) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 254 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 2863311531llu diff --git a/src/plat/imx6/config.cmake b/src/plat/imx6/config.cmake index 98dc70c86c..43222062ab 100644 --- a/src/plat/imx6/config.cmake +++ b/src/plat/imx6/config.cmake @@ -68,7 +68,6 @@ if(KernelPlatImx6) TIMER_FREQUENCY 498000000 MAX_IRQ 159 INTERRUPT_CONTROLLER arch/machine/gic_v2.h - NUM_PPI 32 TIMER ${timer_file} CLK_SHIFT 41llu CLK_MAGIC 4415709349llu diff --git a/src/plat/imx7/config.cmake b/src/plat/imx7/config.cmake index 5bd606db2f..c64bf1babe 100644 --- a/src/plat/imx7/config.cmake +++ b/src/plat/imx7/config.cmake @@ -20,7 +20,6 @@ if(KernelPlatImx7) declare_default_headers( TIMER_FREQUENCY 8000000 MAX_IRQ 159 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 1llu diff --git a/src/plat/imx8m-evk/config.cmake b/src/plat/imx8m-evk/config.cmake index bae963e403..6dae11e441 100644 --- a/src/plat/imx8m-evk/config.cmake +++ b/src/plat/imx8m-evk/config.cmake @@ -37,7 +37,6 @@ if(KernelPlatformImx8mq-evk OR KernelPlatformImx8mm-evk OR KernelPlatformImx8mp- MAX_IRQ ${IMX8M_MAX_IRQ} TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h - NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u ) diff --git a/src/plat/maaxboard/config.cmake b/src/plat/maaxboard/config.cmake index 108ad21f60..0c29369cd0 100644 --- a/src/plat/maaxboard/config.cmake +++ b/src/plat/maaxboard/config.cmake @@ -28,7 +28,6 @@ if(KernelPlatformMaaxboard) MAX_IRQ 160 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h - NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u ) diff --git a/src/plat/odroidc2/config.cmake b/src/plat/odroidc2/config.cmake index eef4995ab1..0a515abefe 100644 --- a/src/plat/odroidc2/config.cmake +++ b/src/plat/odroidc2/config.cmake @@ -19,7 +19,6 @@ if(KernelPlatformOdroidc2) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 250 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 375299969u diff --git a/src/plat/odroidc4/config.cmake b/src/plat/odroidc4/config.cmake index d5fbf9e2c8..229fe5e9dd 100644 --- a/src/plat/odroidc4/config.cmake +++ b/src/plat/odroidc4/config.cmake @@ -19,7 +19,6 @@ if(KernelPlatformOdroidc4) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 255 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 375299969u diff --git a/src/plat/qemu-arm-virt/config.cmake b/src/plat/qemu-arm-virt/config.cmake index e1b50d49ba..6ce8fbd886 100644 --- a/src/plat/qemu-arm-virt/config.cmake +++ b/src/plat/qemu-arm-virt/config.cmake @@ -254,7 +254,6 @@ if(KernelPlatformQEMUArmVirt) declare_default_headers( TIMER_FREQUENCY 62500000 MAX_IRQ 159 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 4611686019llu diff --git a/src/plat/quartz64/config.cmake b/src/plat/quartz64/config.cmake index 03a37e5238..cd5264f420 100644 --- a/src/plat/quartz64/config.cmake +++ b/src/plat/quartz64/config.cmake @@ -20,7 +20,6 @@ if(KernelPlatformQuartz64) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 231 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h ) diff --git a/src/plat/rockpro64/config.cmake b/src/plat/rockpro64/config.cmake index 69bee63e94..5c093da8e8 100644 --- a/src/plat/rockpro64/config.cmake +++ b/src/plat/rockpro64/config.cmake @@ -20,7 +20,6 @@ if(KernelPlatformRockpro64) declare_default_headers( TIMER_FREQUENCY 24000000 MAX_IRQ 181 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v3.h ) diff --git a/src/plat/tk1/config.cmake b/src/plat/tk1/config.cmake index ad5aef8927..2c2053fef6 100644 --- a/src/plat/tk1/config.cmake +++ b/src/plat/tk1/config.cmake @@ -21,7 +21,6 @@ if(KernelPlatformTK1) TIMER_FREQUENCY 12000000 MAX_IRQ 191 INTERRUPT_CONTROLLER arch/machine/gic_v2.h - NUM_PPI 32 TIMER drivers/timer/arm_generic.h SMMU plat/machine/smmu.h CLK_MAGIC 2863311531llu diff --git a/src/plat/tqma8xqp1gb/config.cmake b/src/plat/tqma8xqp1gb/config.cmake index 3a43827a2f..d7c841bc6d 100644 --- a/src/plat/tqma8xqp1gb/config.cmake +++ b/src/plat/tqma8xqp1gb/config.cmake @@ -24,7 +24,6 @@ if(KernelPlatformTqma8xqp1gb) TIMER drivers/timer/arm_generic.h TIMER_OVERHEAD_TICKS 1 INTERRUPT_CONTROLLER arch/machine/gic_v3.h - NUM_PPI 32 CLK_MAGIC 1llu CLK_SHIFT 3u ) diff --git a/src/plat/tx1/config.cmake b/src/plat/tx1/config.cmake index 6c580323c1..4f0bf42de1 100644 --- a/src/plat/tx1/config.cmake +++ b/src/plat/tx1/config.cmake @@ -20,7 +20,6 @@ if(KernelPlatformTx1) TIMER_FREQUENCY 12000000 MAX_IRQ 224 INTERRUPT_CONTROLLER arch/machine/gic_v2.h - NUM_PPI 32 TIMER drivers/timer/arm_generic.h CLK_MAGIC 2863311531llu CLK_SHIFT 35u diff --git a/src/plat/tx2/config.cmake b/src/plat/tx2/config.cmake index ae7351efeb..da8786c680 100644 --- a/src/plat/tx2/config.cmake +++ b/src/plat/tx2/config.cmake @@ -23,7 +23,6 @@ if(KernelPlatformTx2) TIMER_FREQUENCY 31250000 MAX_IRQ 383 INTERRUPT_CONTROLLER arch/machine/gic_v2.h - NUM_PPI 32 TIMER drivers/timer/arm_generic.h CLK_SHIFT 57u CLK_MAGIC 4611686019u diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake index e5433607bf..364fc5a310 100644 --- a/src/plat/zynq7000/config.cmake +++ b/src/plat/zynq7000/config.cmake @@ -27,7 +27,6 @@ if(KernelPlatformZynq7000) # SCHED0011), but may not be the correct number. TIMER_FREQUENCY 320000000 MAX_IRQ 92 - NUM_PPI 32 INTERRUPT_CONTROLLER arch/machine/gic_v2.h TIMER ${timer_file} CLK_SHIFT 40llu diff --git a/src/plat/zynqmp/config.cmake b/src/plat/zynqmp/config.cmake index b2dfb2b381..f30d70b7ad 100644 --- a/src/plat/zynqmp/config.cmake +++ b/src/plat/zynqmp/config.cmake @@ -58,7 +58,6 @@ if(KernelPlatformZynqmp) declare_default_headers( TIMER_FREQUENCY 100000000 MAX_IRQ 187 - NUM_PPI 32 TIMER drivers/timer/arm_generic.h INTERRUPT_CONTROLLER arch/machine/gic_v2.h CLK_MAGIC 1374389535llu From a35c2e9c1a63c0f99a50605236c2b0e04d420d7e Mon Sep 17 00:00:00 2001 From: Axel Heider Date: Thu, 23 Nov 2023 22:16:46 +0100 Subject: [PATCH 10/10] avoid redundancy --- src/object/interrupt.c | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/object/interrupt.c b/src/object/interrupt.c index bf5604a03a..cc1bed857c 100644 --- a/src/object/interrupt.c +++ b/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)),