From 3cbd3b2e952ad219ca1dc9d032e69f63bd774828 Mon Sep 17 00:00:00 2001
From: Indan Zupancic <indan@nul.nu>
Date: Thu, 13 Nov 2025 11:55:34 +0000
Subject: [PATCH] SGI, GICv3: Fix plat_SGITargetValid

Otherwise it is not possible to send SGIs to all cores on platforms
with non-contiguous Affinity values or more than 16 cores.

16 is the limit of the target list, which is only relevant when
sending an SGI to multiple targets at once.

Update the API documentation to reflect what's actually happening.

Signed-off-by: Indan Zupancic <indan@nul.nu>
---
 include/arch/arm/arch/machine/gic_v3.h                  | 2 --
 libsel4/arch_include/arm/interfaces/object-api-arch.xml | 8 ++++----
 src/arch/arm/machine/gic_v3.c                           | 4 +++-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h
index b1f5a1d82..45c8267f7 100644
--- a/include/arch/arm/arch/machine/gic_v3.h
+++ b/include/arch/arm/arch/machine/gic_v3.h
@@ -35,8 +35,6 @@
 #define IRQ_MASK MASK(16u)
 #define GIC_VCPU_MAX_NUM_LR 16
 
-#define GIC_SGI_NUM_TARGETS 16
-
 /* Register bits */
 
 /**
diff --git a/libsel4/arch_include/arm/interfaces/object-api-arch.xml b/libsel4/arch_include/arm/interfaces/object-api-arch.xml
index a7269c8d2..619bf5fa5 100644
--- a/libsel4/arch_include/arm/interfaces/object-api-arch.xml
+++ b/libsel4/arch_include/arm/interfaces/object-api-arch.xml
@@ -800,10 +800,10 @@
                 core like other IRQs. See also <autoref label="sec:interrupts"/>.
             </description>
             <param dir="in" name="irq" type="seL4_Word" description="The SGI INTID (0-15) that can be signalled."/>
-            <param dir="in" name="target" type="seL4_Word" description="The node ID that will be
-            targeted. 0-7 for GICv2 and 0-31 for GICv3. Targets within that range that are not
-            supported by the hardware will be ignored. For example, on a GICv3 board with 4 CPUs, the
-            capability for target 13 can be created, but signals to it will have no effect."/>
+            <param dir="in" name="target" type="seL4_Word" description="The node ID that will be targeted.
+            0-7 for GICv2 and the affinity value for GICv3 (concatenation of Aff3+Aff2+Aff1+Aff0 from MPIDR).
+            Targets within that range that are not supported by the hardware will be ignored. For example, on a GICv2
+            board with 4 CPUs, the capability for target 5 can be created, but signals to it will have no effect."/>
 
             <param dir="in" name="root" type="seL4_CNode" description="CPtr to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
             <param dir="in" name="index" type="seL4_Word" description="CPtr to the destination slot. Resolved from the root of the destination CSpace."/>
diff --git a/src/arch/arm/machine/gic_v3.c b/src/arch/arm/machine/gic_v3.c
index 3621059c4..a30ba78e0 100644
--- a/src/arch/arm/machine/gic_v3.c
+++ b/src/arch/arm/machine/gic_v3.c
@@ -359,7 +359,9 @@ BOOT_CODE void cpu_initLocalIRQController(void)
 
 bool_t plat_SGITargetValid(word_t target)
 {
-    return target < GIC_SGI_NUM_TARGETS;
+    /* Aff0+Aff1+Aff2+Aff3 values are not guaranteed to be contiguous
+     * and the first core may have a non-zero affinity value. */
+    return target <= UINT32_MAX;
 }
 
 void plat_sendSGI(word_t irq, word_t target)