Add new APIs for generating SGIs

include/arch/arm/arch/32/mode/object/structures.bf

@@ -102,6 +102,20 @@ block vcpu_cap {
 }
 #endif
 
+#if CONFIG_MAX_NUM_NODES == 1
+
+block sgi_signal_cap {
+    field capSGIIRQ         16
+    field capSGITarget      4
+    padding                 12
+
+    padding        24
+    field capType  8
+}
+
+#endif
+
+
 #ifdef CONFIG_TK1_SMMU
 -- IO space caps
 -- each module has an engine that can be enabled
@@ -179,6 +193,9 @@ tagged_union cap capType {
     tag io_space_cap            0x1f
     tag io_page_table_cap       0x2f
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    tag sgi_signal_cap          0x3f
+#endif
 }
 
 ---- Arm specific fault types

include/arch/arm/arch/32/mode/object/structures.h

@@ -298,6 +298,10 @@ static inline word_t CONST cap_get_archCapSizeBits(cap_t cap)
     case cap_vcpu_cap:
         return VCPU_SIZE_BITS;
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return 0;
+#endif
 #ifdef CONFIG_TK1_SMMU
     case cap_io_page_table_cap:
         return seL4_IOPageTableBits;
@@ -339,6 +343,10 @@ static inline bool_t CONST cap_get_archCapIsPhysical(cap_t cap)
     case cap_vcpu_cap:
         return true;
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return false;
+#endif
 
 #ifdef CONFIG_TK1_SMMU
     case cap_io_page_table_cap:
@@ -379,6 +387,10 @@ static inline void *CONST cap_get_archCapPtr(cap_t cap)
     case cap_vcpu_cap:
         return VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap));
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return NULL;
+#endif
 
 #ifdef CONFIG_TK1_SMMU
     case cap_io_page_table_cap:

include/arch/arm/arch/64/mode/object/structures.bf

@@ -87,6 +87,18 @@ block vcpu_cap {
 }
 #endif
 
+#if CONFIG_MAX_NUM_NODES == 1
+
+block sgi_signal_cap {
+    padding        44
+    field capSGIIRQ         16
+    field capSGITarget      4
+
+    field capType  5
+    padding        59
+}
+
+#endif
 #ifdef CONFIG_ARM_SMMU
 
 block sid_control_cap {
@@ -172,6 +184,9 @@ tagged_union cap capType {
 #ifdef CONFIG_ALLOW_SMC_CALLS
     tag smc_cap                     25
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    tag sgi_signal_cap              27
+#endif
 }
 
 ---- Arch-independent object types

include/arch/arm/arch/64/mode/object/structures.h

@@ -107,6 +107,10 @@ static inline word_t CONST cap_get_archCapSizeBits(cap_t cap)
     case cap_vcpu_cap:
         return seL4_VCPUBits;
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return 0;
+#endif
 
     default:
         /* Unreachable, but GCC can't figure that out */
@@ -141,6 +145,10 @@ static inline bool_t CONST cap_get_archCapIsPhysical(cap_t cap)
     case cap_vcpu_cap:
         return true;
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return false;
+#endif
 
     default:
         /* Unreachable, but GCC can't figure that out */
@@ -174,6 +182,10 @@ static inline void *CONST cap_get_archCapPtr(cap_t cap)
     case cap_vcpu_cap:
         return VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap));
 #endif
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return NULL;
+#endif
 
     default:
         /* Unreachable, but GCC can't figure that out */

include/arch/arm/arch/machine/gic_common.h

@@ -22,6 +22,7 @@
 /* CPU specific IRQ's */
 #define SGI_START         0u
 #define PPI_START         16u
+#define NUM_SGIS          16u
 
 /* Shared Peripheral Interrupts */
 #define SPI_START         32u

include/arch/arm/arch/machine/gic_v2.h

@@ -23,6 +23,8 @@
 #define IRQ_MASK MASK(10u)
 #define GIC_VCPU_MAX_NUM_LR 64
 
+#define GIC_SGI_TARGET_MASK_BITS 8
+
 /* Helpers for VGIC */
 #define VGIC_HCR_EOI_INVALID_COUNT(hcr) (((hcr) >> 27) & 0x1f)
 #define VGIC_HCR_VGRP1DIE               (1U << 7)

include/arch/arm/arch/machine/gic_v3.h

@@ -30,6 +30,8 @@
 #define IRQ_MASK MASK(16u)
 #define GIC_VCPU_MAX_NUM_LR 16
 
+#define GIC_SGI_TARGET_MASK_BITS 16
+
 /* Register bits */
 #define GICD_CTL_ENABLE 0x1
 #define GICD_CTLR_RWP                BIT(31)

include/arch/arm/arch/object/interrupt.h

@@ -15,6 +15,9 @@
 exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
                                             cte_t *srcSlot, word_t *buffer);
 
+exception_t decodeSGISignalInvocation(word_t invLabel, word_t length,
+                                      cap_t cap, word_t *buffer);
+
 /* Handle a platform-reserved IRQ. */
 static inline void handleReservedIRQ(irq_t irq)
 {

include/arch/arm/arch/object/objecttype.h

@@ -29,3 +29,52 @@ word_t Arch_getObjectSize(word_t t);
 static inline void Arch_postCapDeletion(cap_t cap)
 {
 }
+
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+#if CONFIG_MAX_NUM_NODES == 1
+    return cap_get_capType(cap) == cap_sgi_signal_cap;
+#else
+    return false;
+#endif
+}
+
+/**
+ * isMDBParentOf for architecture caps. For most arch caps, this just returns
+ * true, but if there are badged versions of arch caps, this functions should
+ * perform the necessary checks.
+ *
+ * Called by the generic isMDBParentOf after the revocable bit has been checked
+ * and sameRegionAs has been established. This means we can assume both as true
+ * inside Arch_isMDBParentOf.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+    switch (cap_get_capType(cap_a)) {
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return !firstBadged;
+        break;
+#endif
+
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    case cap_smc_cap: {
+        word_t badge;
+
+        badge = cap_smc_cap_get_capSMCBadge(cap_a);
+        if (badge == 0) {
+            return true;
+        }
+        return (badge == cap_smc_cap_get_capSMCBadge(cap_b)) &&
+               !firstBadged;
+        break;
+    }
+#endif
+
+    default:
+        return true;
+    }
+}

include/arch/arm/arch/object/structures.h

@@ -12,17 +12,20 @@
 
 static inline bool_t CONST Arch_isCapRevocable(cap_t derivedCap, cap_t srcCap)
 {
-#ifdef CONFIG_ALLOW_SMC_CALLS
     switch (cap_get_capType(derivedCap)) {
+
+#if CONFIG_MAX_NUM_NODES == 1
+    case cap_sgi_signal_cap:
+        return cap_get_capType(srcCap) == cap_irq_control_cap;
+#endif
+
+#ifdef CONFIG_ALLOW_SMC_CALLS
     case cap_smc_cap:
         return (cap_smc_cap_get_capSMCBadge(derivedCap) !=
                 cap_smc_cap_get_capSMCBadge(srcCap));
+#endif
 
     default:
         return false;
     }
-#endif
-    return false;
 }
-
-

include/arch/riscv/arch/object/objecttype.h

@@ -30,3 +30,18 @@ static inline void Arch_postCapDeletion(cap_t cap)
 {
 }
 
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+    return false;
+}
+
+/**
+ * isMDBParentOf for architecture caps. See Arm version for more detailed docs.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+    return true;
+}

include/arch/x86/arch/object/objecttype.h

@@ -37,3 +37,18 @@ word_t Mode_getObjectSize(word_t t);
 
 void Arch_postCapDeletion(cap_t cap);
 
+/**
+ * Return true if the given arch cap can be a descendant of an IRQControlCap.
+ */
+static inline CONST bool_t Arch_isIRQControlDescendant(cap_t cap)
+{
+    return false;
+}
+
+/**
+ * isMDBParentOf for architecture caps. See Arm version for more detailed docs.
+ */
+static inline CONST bool_t Arch_isMDBParentOf(cap_t cap_a, cap_t cap_b, bool_t firstBadged)
+{
+    return true;
+}

include/smp/ipi.h

@@ -54,8 +54,6 @@ void generic_ipi_send_mask(irq_t ipi, word_t mask, bool_t isBlocking);
  */
 void ipi_send_mask(irq_t ipi, word_t mask, bool_t isBlocking);
 
-/* Hardware implementation for sending IPIs */
-void ipi_send_target(irq_t irq, word_t cpuTargetList);
 
 /* This function switches the core it is called on to the idle thread,
  * in order to avoid IPI storms. If the core is waiting on the lock, the actual
@@ -156,9 +154,11 @@ static void inline doRemoteOp3Arg(IpiRemoteCall_t func, word_t data1, word_t dat
 void doMaskReschedule(word_t mask);
 
 
-#ifdef CONFIG_DEBUG_BUILD
-exception_t handle_SysDebugSendIPI(void);
-#endif
 
 #endif /* ENABLE_SMP_SUPPORT */
 
+#ifdef CONFIG_DEBUG_BUILD
+exception_t handle_SysDebugSendIPI(void);
+#endif
+/* Hardware implementation for sending IPIs */
+void ipi_send_target(irq_t irq, word_t cpuTargetList);

libsel4/arch_include/arm/interfaces/sel4arch.xml

@@ -772,6 +772,49 @@
                 </description>
             </error>
         </method>
+        <method id="ARMIRQIssueSGISignal" name="IssueSGISignal" manual_name="IssueSGISignal"
+           manual_label="irq_controlissuesgisignal">
+            <condition><not><config var="CONFIG_ENABLE_SMP_SUPPORT"/></not></condition>
+            <brief>
+                Create an SGI signal capability.
+            </brief>
+            <description>
+            </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."/>
+
+            <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."/>
+            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
+            <error name="seL4_DeleteFirst">
+                <description>
+                    The destination slot contains a capability.
+                </description>
+            </error>
+            <error name="seL4_FailedLookup">
+                <description>
+                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
+                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
+                </description>
+            </error>
+            <error name="seL4_IllegalOperation">
+                <description>
+                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
+                </description>
+            </error>
+            <error name="seL4_InvalidCapability">
+                <description>
+                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
+                </description>
+            </error>
+            <error name="seL4_RangeError">
+                <description>
+                    The value of <texttt text="irq"/> or <texttt text="target"/> is out of range.
+                    Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
+                </description>
+            </error>
+        </method>
+
     </interface>
     <interface name="seL4_ARM_SIDControl" manual_name="SID Control" cap_description="A SIDControl capability. This gives you the authority to make this call.">
        <method id="ARMSIDIssueSIDManager" name="GetSID" manual_name="Get SID" manual_label="sid_controlgetsid">

libsel4/arch_include/arm/sel4/arch/syscalls.h

@@ -644,12 +644,10 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
     arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
 }
 
-#if CONFIG_ENABLE_SMP_SUPPORT
 LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)
 {
     arm_sys_send(seL4_SysDebugSendIPI, target, irq, 0, 0, 0, 0);
 }
-#endif /* CONFIG_ENABLE_SMP_SUPPORT */
 #endif
 
 #ifdef CONFIG_DANGEROUS_CODE_INJECTION

libsel4/arch_include/arm/sel4/arch/types.h

@@ -23,6 +23,7 @@ typedef seL4_CPtr seL4_ARM_SID;
 typedef seL4_CPtr seL4_ARM_CBControl;
 typedef seL4_CPtr seL4_ARM_CB;
 typedef seL4_CPtr seL4_ARM_SMC;
+typedef seL4_CPtr seL4_ARM_SGI_Signal;
 
 typedef enum {
     seL4_ARM_PageCacheable = 0x01,

libsel4/include/api/syscall.xml

@@ -50,12 +50,7 @@
             <syscall name="DebugNameThread"/>
         </config>
         <config>
-            <condition>
-                <and>
-                    <config var="CONFIG_DEBUG_BUILD"/>
-                    <config var="CONFIG_ENABLE_SMP_SUPPORT"/>
-                </and>
-            </condition>
+            <condition><config var="CONFIG_DEBUG_BUILD"/></condition>
             <syscall name="DebugSendIPI"/>
         </config>
         <config>