diff --git a/config.cmake b/config.cmake
index 7d2c0bcbbe48ab602839407f541e0152e8d938b3..b6535fd5b3f09e03c32d44b4875715e9e8f8b06f 100644
--- a/config.cmake
+++ b/config.cmake
@@ -50,15 +50,25 @@ if(DEFINED CONFIGURE_MAX_IRQ)
# calculate the irq cnode size based on MAX_IRQ
if("${KernelArch}" STREQUAL "riscv")
set(MAX_IRQ "${CONFIGURE_PLIC_MAX_NUM_INT}")
- math(EXPR MAX_IRQ "${MAX_IRQ} + 2")
+ math(EXPR MAX_NUM_IRQ "${MAX_IRQ} + 2")
else()
- set(MAX_IRQ "${CONFIGURE_MAX_IRQ}")
+ if(
+ DEFINED KernelMaxNumNodes
+ AND CONFIGURE_NUM_PPI GREATER "0"
+ AND "${KernelArch}" STREQUAL "arm"
+ )
+ math(
+ EXPR MAX_NUM_IRQ
+ "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
+ )
+ else()
+ set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}")
+ endif()
endif()
set(BITS "0")
- set(MAX "${MAX_IRQ}")
- while(MAX GREATER "0")
+ while(MAX_NUM_IRQ GREATER "0")
math(EXPR BITS "${BITS} + 1")
- math(EXPR MAX "${MAX} >> 1")
+ math(EXPR MAX_NUM_IRQ "${MAX_NUM_IRQ} >> 1")
endwhile()
math(EXPR SLOTS "1 << ${BITS}")
if("${SLOTS}" LESS "${MAX_IRQ}")
diff --git a/configs/seL4Config.cmake b/configs/seL4Config.cmake
index f44db7bd4be988bc56133036fc13b3ac06e93ab2..0d8425be4d059edc3c417263c11b949702961453 100644
--- a/configs/seL4Config.cmake
+++ b/configs/seL4Config.cmake
@@ -98,6 +98,7 @@ endmacro()
unset(CONFIGURE_PLIC_MAX_NUM_INT CACHE)
unset(CONFIGURE_TIMER_FREQUENCY CACHE)
unset(CONFIGURE_MAX_IRQ CACHE)
+unset(CONFIGURE_NUM_PPI CACHE)
unset(CONFIGURE_INTERRUPT_CONTROLLER CACHE)
unset(CONFIGURE_TIMER CACHE)
unset(CONFIGURE_SMMU CACHE)
@@ -107,11 +108,12 @@ function(declare_default_headers)
0
CONFIGURE
""
- "TIMER_FREQUENCY;MAX_IRQ;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU"
+ "TIMER_FREQUENCY;MAX_IRQ;NUM_PPI;PLIC_MAX_NUM_INT;INTERRUPT_CONTROLLER;TIMER;SMMU"
""
)
set(CONFIGURE_TIMER_FREQUENCY "${CONFIGURE_TIMER_FREQUENCY}" CACHE INTERNAL "")
set(CONFIGURE_MAX_IRQ "${CONFIGURE_MAX_IRQ}" CACHE INTERNAL "")
+ set(CONFIGURE_NUM_PPI "${CONFIGURE_NUM_PPI}" CACHE INTERNAL "")
set(CONFIGURE_PLIC_MAX_NUM_INT "${CONFIGURE_PLIC_MAX_NUM_INT}" CACHE INTERNAL "")
set(CONFIGURE_INTERRUPT_CONTROLLER "${CONFIGURE_INTERRUPT_CONTROLLER}" CACHE INTERNAL "")
set(CONFIGURE_TIMER "${CONFIGURE_TIMER}" CACHE INTERNAL "")
diff --git a/include/arch/arm/arch/machine/gic_v2.h b/include/arch/arm/arch/machine/gic_v2.h
index c4ee50aed1685163096f628f9b221d7fc703e53c..489b0dcd1ff252165e246f5af41df12de3f19c73 100644
--- a/include/arch/arm/arch/machine/gic_v2.h
+++ b/include/arch/arm/arch/machine/gic_v2.h
@@ -42,6 +42,30 @@
#define IRQ_MASK MASK(10u)
#define IS_IRQ_VALID(X) (((X) & IRQ_MASK) < SPECIAL_IRQ_START)
+#define NUM_PPI 32
+#define HW_IRQ_IS_PPI(irq) ((irq) < NUM_PPI)
+#define IRQ_IS_PPI(irq) ((irq) < NUM_PPI*CONFIG_MAX_NUM_NODES)
+
+#if defined ENABLE_SMP_SUPPORT
+/* Takes a target core and an irq number and converts it to the intState index */
+#define CORE_IRQ_TO_IDX(tgt, irq) (HW_IRQ_IS_PPI(irq) ? \
+ (tgt)*NUM_PPI + (irq) : \
+ (CONFIG_MAX_NUM_NODES-1)*NUM_PPI + (irq))
+
+/* Takes an intSate index and extracts the hardware irq number */
+#define IDX_TO_IRQ(idx) (IRQ_IS_PPI(idx) ? \
+ (idx) - ((idx)/NUM_PPI)*NUM_PPI : \
+ (idx) - (CONFIG_MAX_NUM_NODES-1)*NUM_PPI)
+
+/* Takes an intState index and extracts the target CPU number */
+#define IDX_TO_CORE(idx) (IRQ_IS_PPI(idx) ? \
+ (idx) / NUM_PPI : 0)
+#else
+#define CORE_IRQ_TO_IDX(tgt, irq) ((irq_t) (irq))
+#define IDX_TO_IRQ(idx) (idx)
+#define IDX_TO_CORE(idx) 0
+#endif
+
/* Helpers for VGIC */
#define VGIC_HCR_EOI_INVALID_COUNT(hcr) (((hcr) >> 27) & 0x1f)
#define VGIC_HCR_VGRP1DIE (1U << 7)
@@ -188,7 +212,7 @@ static inline interrupt_t getActiveIRQ(void)
irq = irqInvalid;
}
- return irq;
+ return CORE_IRQ_TO_IDX(SMP_TERNARY(getCurrentCPUIndex(), 0), irq);
}
/*
@@ -203,19 +227,22 @@ static inline bool_t isIRQPending(void)
static inline void maskInterrupt(bool_t disable, interrupt_t irq)
{
+#if defined ENABLE_SMP_SUPPORT && defined CONFIG_ARCH_ARM
+ assert(!(IRQ_IS_PPI(irq)) || (IDX_TO_CORE(irq) == getCurrentCPUIndex()));
+#endif
if (disable) {
- dist_enable_clr(irq);
+ dist_enable_clr(IDX_TO_IRQ(irq));
} else {
- dist_enable_set(irq);
+ dist_enable_set(IDX_TO_IRQ(irq));
}
}
static inline void ackInterrupt(irq_t irq)
{
assert(IS_IRQ_VALID(active_irq[SMP_TERNARY(getCurrentCPUIndex(), 0)])
- && (active_irq[SMP_TERNARY(getCurrentCPUIndex(), 0)] & IRQ_MASK) == irq);
- if (is_irq_edge_triggered(irq)) {
- dist_pending_clr(irq);
+ && (active_irq[SMP_TERNARY(getCurrentCPUIndex(), 0)] & IRQ_MASK) == IDX_TO_IRQ(irq));
+ if (is_irq_edge_triggered(IDX_TO_IRQ(irq))) {
+ dist_pending_clr(IDX_TO_IRQ(irq));
}
gic_cpuiface->eoi = active_irq[SMP_TERNARY(getCurrentCPUIndex(), 0)];
active_irq[SMP_TERNARY(getCurrentCPUIndex(), 0)] = IRQ_NONE;
diff --git a/include/object/structures_32.bf b/include/object/structures_32.bf
index 6941846807d76da332f1c8d56dde7e5c1dc5be34..77ad3b31613046aae04d2a349989ed73b6f48f41 100644
--- a/include/object/structures_32.bf
+++ b/include/object/structures_32.bf
@@ -88,8 +88,12 @@ block irq_control_cap {
}
block irq_handler_cap {
- padding 24
- field capIRQ 8
+#ifdef ENABLE_SMP_SUPPORT
+ field capIRQ 32
+#else
+ padding 24
+ field capIRQ 8
+#endif
padding 24
field capType 8
diff --git a/include/object/structures_64.bf b/include/object/structures_64.bf
index a421b467aff971d9f12b5f5dd3637c226da29a17..d1de87c19274d85277b12366be3a57f63bd6757b 100644
--- a/include/object/structures_64.bf
+++ b/include/object/structures_64.bf
@@ -130,8 +130,12 @@ block irq_control_cap {
}
block irq_handler_cap {
+#ifdef ENABLE_SMP_SUPPORT
+ field capIRQ 64
+#else
padding 52
field capIRQ 12
+#endif
field capType 5
padding 59
diff --git a/src/arch/arm/machine/gic_v2.c b/src/arch/arm/machine/gic_v2.c
index 31f702df3041ed2c93840e55b3486d0ec5c3e914..af084e4090ba7e70885854a6b75f6f6a458bcb11 100644
--- a/src/arch/arm/machine/gic_v2.c
+++ b/src/arch/arm/machine/gic_v2.c
@@ -156,8 +156,8 @@ void setIRQTrigger(irq_t irq, bool_t trigger)
/* in the gic_config, there is a 2 bit field for each irq,
* setting the most significant bit of this field makes the irq edge-triggered,
* while 0 indicates that it is level-triggered */
- word_t index = irq / 16u;
- word_t offset = (irq % 16u) * 2;
+ word_t index = IDX_TO_IRQ(irq) / 16u;
+ word_t offset = (IDX_TO_IRQ(irq) % 16u) * 2;
if (trigger) {
/* set the bit */
gic_dist->config[index] |= BIT(offset + 1);
@@ -214,13 +214,14 @@ void setIRQTarget(irq_t irq, seL4_Word target)
{
uint8_t targetList = 1 << target;
uint8_t *targets = (void *)(gic_dist->targets);
+ word_t hwIRQ = IDX_TO_IRQ(irq);
/* Return early if PPI */
- if (irq < SPI_START) {
+ if (IRQ_IS_PPI(irq)) {
fail("PPI can't have designated target core\n");
return;
}
- targets[irq] = targetList;
+ targets[hwIRQ] = targetList;
}
#endif /* ENABLE_SMP_SUPPORT */
diff --git a/src/plat/allwinnerA20/config.cmake b/src/plat/allwinnerA20/config.cmake
index ac136b433b9214582aafc8cfd0b81a7e6d3ac648..18300ebfbe395ac36bab568c037417f7098c4baf 100644
--- a/src/plat/allwinnerA20/config.cmake
+++ b/src/plat/allwinnerA20/config.cmake
@@ -25,6 +25,7 @@ if(KernelPlatformAllwinnerA20)
declare_default_headers(
TIMER_FREQUENCY 24000000llu
MAX_IRQ 122
+ NUM_PPI 32
TIMER drivers/timer/allwinner.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/apq8064/config.cmake b/src/plat/apq8064/config.cmake
index e12f56be83884455717c794e63177e160906ba87..05cc96072a7bded6608700e665446d47112d0aea 100644
--- a/src/plat/apq8064/config.cmake
+++ b/src/plat/apq8064/config.cmake
@@ -26,6 +26,7 @@ if(KernelPlatformAPQ8064)
declare_default_headers(
TIMER_FREQUENCY 7000000llu
MAX_IRQ 283
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/exynos4/config.cmake b/src/plat/exynos4/config.cmake
index de18486bb18b2361768356a1dc02310068371b87..ec5343fdb9408aab4d3a98c5723c5f320261bb7f 100644
--- a/src/plat/exynos4/config.cmake
+++ b/src/plat/exynos4/config.cmake
@@ -25,6 +25,7 @@ if(KernelPlatformExynos4)
declare_default_headers(
TIMER_FREQUENCY 24000000llu
MAX_IRQ 159
+ NUM_PPI 32
TIMER drivers/timer/exynos4412-mct.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/exynos5/config.cmake b/src/plat/exynos5/config.cmake
index edb242e11ea5ca76d2f3bc958a97f76e1e775034..cd89193661bdaa15a9df9383231b1d4da80d69f1 100644
--- a/src/plat/exynos5/config.cmake
+++ b/src/plat/exynos5/config.cmake
@@ -70,6 +70,7 @@ if(KernelPlatExynos5)
declare_default_headers(
TIMER_FREQUENCY 24000000llu
MAX_IRQ 232
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/imx6/config.cmake b/src/plat/imx6/config.cmake
index b68aed0e6a0e8f1c77758ac957ce65511db44919..74a209150345755dd2064d803c0030c19b071c3b 100644
--- a/src/plat/imx6/config.cmake
+++ b/src/plat/imx6/config.cmake
@@ -44,6 +44,7 @@ if(KernelPlatImx6)
TIMER_FREQUENCY 400000000llu
MAX_IRQ 159
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
+ NUM_PPI 32
TIMER drivers/timer/arm_priv.h
)
endif()
diff --git a/src/plat/imx7/config.cmake b/src/plat/imx7/config.cmake
index bb0676c197ab286fae29c782b78538ee5e888262..0a2795130bf9ec9ccb8a13712f47d00ab746a049 100644
--- a/src/plat/imx7/config.cmake
+++ b/src/plat/imx7/config.cmake
@@ -25,6 +25,7 @@ if(KernelPlatImx7)
declare_default_headers(
TIMER_FREQUENCY 8000000llu
MAX_IRQ 159
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/odroidc2/config.cmake b/src/plat/odroidc2/config.cmake
index f1ad42263d6081b91a8e8e1b46e4fe07739950e4..39cef825493dca784d77d43698d0bca02d937238 100644
--- a/src/plat/odroidc2/config.cmake
+++ b/src/plat/odroidc2/config.cmake
@@ -24,6 +24,7 @@ if(KernelPlatformOdroidc2)
declare_default_headers(
TIMER_FREQUENCY 24000000llu
MAX_IRQ 250
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/tk1/config.cmake b/src/plat/tk1/config.cmake
index 5a089f236de9b132da8581da738840fc807d3f77..daad60762d628786374e0b8b750fdfc70d24d46c 100644
--- a/src/plat/tk1/config.cmake
+++ b/src/plat/tk1/config.cmake
@@ -35,6 +35,7 @@ if(KernelPlatformTK1)
TIMER_FREQUENCY 12000000llu
MAX_IRQ 191
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h SMMU plat/machine/smmu.h
)
endif()
diff --git a/src/plat/tx1/config.cmake b/src/plat/tx1/config.cmake
index 0f7e59470c6a70e2dcd1892267d7672539f99d0f..9fbed57b65c8b84a19fe210c143ac8c363567486 100644
--- a/src/plat/tx1/config.cmake
+++ b/src/plat/tx1/config.cmake
@@ -27,6 +27,7 @@ if(KernelPlatformTx1)
TIMER_FREQUENCY 19200000llu
MAX_IRQ 224
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
)
endif()
diff --git a/src/plat/tx2/config.cmake b/src/plat/tx2/config.cmake
index 94abfe59723ae039ed3334d2bc1f3446f0508b5d..fe0e1d157072bca2d7f61253360f1570cbce7e79 100644
--- a/src/plat/tx2/config.cmake
+++ b/src/plat/tx2/config.cmake
@@ -30,6 +30,7 @@ if(KernelPlatformTx2)
TIMER_FREQUENCY 31250000llu
MAX_IRQ 383
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
)
endif()
diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake
index 3c270b67472c6907ace658263aaf8be26990db23..d16a4e4f62a46bbbe16bff5231ea97194a8ea05f 100644
--- a/src/plat/zynq7000/config.cmake
+++ b/src/plat/zynq7000/config.cmake
@@ -24,6 +24,7 @@ if(KernelPlatformZynq7000)
declare_default_headers(
TIMER_FREQUENCY 400000000llu
MAX_IRQ 92
+ NUM_PPI 32
TIMER drivers/timer/arm_priv.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)
diff --git a/src/plat/zynqmp/config.cmake b/src/plat/zynqmp/config.cmake
index aff1e9afa377408913f0723511681d8313a50a00..571e1c0ffbda01bfb87e748009ff6eb132285a04 100644
--- a/src/plat/zynqmp/config.cmake
+++ b/src/plat/zynqmp/config.cmake
@@ -45,6 +45,7 @@ if(KernelPlatformZynqmp)
declare_default_headers(
TIMER_FREQUENCY 100000000llu
MAX_IRQ 187
+ NUM_PPI 32
TIMER drivers/timer/arm_generic.h
INTERRUPT_CONTROLLER arch/machine/gic_v2.h
)