diff --git a/include/arch/arm/arch/32/mode/object/structures.bf b/include/arch/arm/arch/32/mode/object/structures.bf
index 4bc683ca9..7d04d3d44 100644
--- a/include/arch/arm/arch/32/mode/object/structures.bf
+++ b/include/arch/arm/arch/32/mode/object/structures.bf
@@ -102,6 +102,19 @@ block vcpu_cap {
}
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+
+block sgi_signal_cap {
+ field capSGITarget 32
+
+ padding 20
+ field capSGIIRQ 4
+ field capType 8
+}
+
+#endif
+
+
#ifdef CONFIG_TK1_SMMU
-- IO space caps
-- each module has an engine that can be enabled
@@ -179,6 +192,9 @@ tagged_union cap capType {
tag io_space_cap 0x1f
tag io_page_table_cap 0x2f
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ tag sgi_signal_cap 0x3f
+#endif
}
---- Arm specific fault types
diff --git a/include/arch/arm/arch/32/mode/object/structures.h b/include/arch/arm/arch/32/mode/object/structures.h
index f6bb938df..1478f00d6 100644
--- a/include/arch/arm/arch/32/mode/object/structures.h
+++ b/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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ 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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ 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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ return NULL;
+#endif
#ifdef CONFIG_TK1_SMMU
case cap_io_page_table_cap:
diff --git a/include/arch/arm/arch/64/mode/object/structures.bf b/include/arch/arm/arch/64/mode/object/structures.bf
index 1c0436be6..176577ef5 100644
--- a/include/arch/arm/arch/64/mode/object/structures.bf
+++ b/include/arch/arm/arch/64/mode/object/structures.bf
@@ -87,6 +87,18 @@ block vcpu_cap {
}
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+
+block sgi_signal_cap {
+ padding 32
+ field capSGITarget 32
+
+ field capType 5
+ field capSGIIRQ 4
+ padding 55
+}
+
+#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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ tag sgi_signal_cap 27
+#endif
}
---- Arch-independent object types
diff --git a/include/arch/arm/arch/64/mode/object/structures.h b/include/arch/arm/arch/64/mode/object/structures.h
index 781aff151..d727fe9f2 100644
--- a/include/arch/arm/arch/64/mode/object/structures.h
+++ b/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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ 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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ 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
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ return NULL;
+#endif
default:
/* Unreachable, but GCC can't figure that out */
diff --git a/include/arch/arm/arch/machine.h b/include/arch/arm/arch/machine.h
index 1f6dee636..eb7707b2a 100644
--- a/include/arch/arm/arch/machine.h
+++ b/include/arch/arm/arch/machine.h
@@ -23,6 +23,8 @@ void setIRQTrigger(irq_t irq, bool_t trigger);
#ifdef ENABLE_SMP_SUPPORT
void setIRQTarget(irq_t irq, seL4_Word target);
#endif
+bool_t plat_SGITargetValid(word_t target);
+void plat_sendSGI(word_t irq, word_t target);
static inline void plat_cleanL2Range(paddr_t start, paddr_t end);
static inline void plat_invalidateL2Range(paddr_t start, paddr_t end);
diff --git a/include/arch/arm/arch/machine/gic_common.h b/include/arch/arm/arch/machine/gic_common.h
index 584d1b508..5a218ef5c 100644
--- a/include/arch/arm/arch/machine/gic_common.h
+++ b/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
diff --git a/include/arch/arm/arch/machine/gic_v2.h b/include/arch/arm/arch/machine/gic_v2.h
index b426606b4..3a852020c 100644
--- a/include/arch/arm/arch/machine/gic_v2.h
+++ b/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_NUM_TARGETS 8
+
/* Helpers for VGIC */
#define VGIC_HCR_EOI_INVALID_COUNT(hcr) (((hcr) >> 27) & 0x1f)
#define VGIC_HCR_VGRP1DIE (1U << 7)
diff --git a/include/arch/arm/arch/machine/gic_v3.h b/include/arch/arm/arch/machine/gic_v3.h
index ec41922dd..6e5802fd1 100644
--- a/include/arch/arm/arch/machine/gic_v3.h
+++ b/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_NUM_TARGETS 16
+
/* Register bits */
#define GICD_CTLR_RWP BIT(31)
#define GICD_CTLR_ARE_NS BIT(5)
diff --git a/include/arch/arm/arch/object/interrupt.h b/include/arch/arm/arch/object/interrupt.h
index b6b24a6da..69ba77e73 100644
--- a/include/arch/arm/arch/object/interrupt.h
+++ b/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)
{
diff --git a/include/smp/ipi.h b/include/smp/ipi.h
index 64b6cd6f0..d0828034e 100644
--- a/include/smp/ipi.h
+++ b/include/smp/ipi.h
@@ -143,4 +143,3 @@ exception_t handle_SysDebugSendIPI(void);
#endif
#endif /* ENABLE_SMP_SUPPORT */
-
diff --git a/libsel4/arch_include/arm/interfaces/object-api-arch.xml b/libsel4/arch_include/arm/interfaces/object-api-arch.xml
index 9c268e648..a7269c8d2 100644
--- a/libsel4/arch_include/arm/interfaces/object-api-arch.xml
+++ b/libsel4/arch_include/arm/interfaces/object-api-arch.xml
@@ -783,6 +783,59 @@
+
+
+
+ Create a software generated interrupt (SGI) signal capability.
+
+
+ Create an SGISignal capability and place it in the specific target CSpace slot. The
+ capability can be used to raise an SGI with a specific ID on a specific target core.
+ Currently this feature is supported on GICv2 and GICv3 hardware. Only available on
+ non-SMP configurations.
+
+ The resulting capability can be invoked like a notification capability that supports
+ only signal/send. SGIs can be received by IRQ notification objects on the target
+ core like other IRQs. See also .
+
+
+
+
+
+
+
+
+
+ The destination slot contains a capability.
+
+
+
+
+ The or is invalid (see ).
+ Or, is a CPtr to a capability of the wrong type.
+
+
+
+
+ The is a CPtr to a capability of the wrong type.
+
+
+
+
+ The is a CPtr to a capability of the wrong type.
+
+
+
+
+ The value of or is out of range.
+ Or, is invalid (see ).
+
+
+
diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index d7ab6e763..63eaae369 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -649,8 +649,8 @@ 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
+#endif /* CONFIG_DEBUG_BUILD */
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (* userfn)(void *), void *userarg)
diff --git a/libsel4/arch_include/arm/sel4/arch/types.h b/libsel4/arch_include/arm/sel4/arch/types.h
index 5882343fc..571400d44 100644
--- a/libsel4/arch_include/arm/sel4/arch/types.h
+++ b/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,
diff --git a/libsel4/include/api/syscall.xml b/libsel4/include/api/syscall.xml
index 5b62ac24e..48a32e127 100644
--- a/libsel4/include/api/syscall.xml
+++ b/libsel4/include/api/syscall.xml
@@ -50,12 +50,7 @@
-
-
-
-
-
-
+
diff --git a/src/arch/arm/32/object/objecttype.c b/src/arch/arm/32/object/objecttype.c
index 035871738..2d4c9fefa 100644
--- a/src/arch/arm/32/object/objecttype.c
+++ b/src/arch/arm/32/object/objecttype.c
@@ -87,6 +87,13 @@ deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
return ret;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ ret.cap = cap;
+ ret.status = EXCEPTION_NONE;
+ return ret;
+#endif
+
#ifdef CONFIG_TK1_SMMU
case cap_io_space_cap:
ret.cap = cap;
@@ -225,6 +232,13 @@ finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
break;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ // do nothing
+ break;
+#endif
+
+
#ifdef CONFIG_TK1_SMMU
case cap_io_space_cap:
if (final) {
@@ -300,6 +314,18 @@ bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
break;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ if (cap_get_capType(cap_b) == cap_sgi_signal_cap) {
+ return (cap_sgi_signal_cap_get_capSGIIRQ(cap_a) ==
+ cap_sgi_signal_cap_get_capSGIIRQ(cap_b) &&
+ cap_sgi_signal_cap_get_capSGITarget(cap_a) ==
+ cap_sgi_signal_cap_get_capSGITarget(cap_b));
+ }
+ break;
+#endif
+
+
#ifdef CONFIG_TK1_SMMU
case cap_io_space_cap:
if (cap_get_capType(cap_b) == cap_io_space_cap) {
@@ -553,7 +579,7 @@ exception_t Arch_decodeInvocation(word_t invLabel, word_t length, cptr_t cptr,
/* The C parser cannot handle a switch statement with only a default
* case. So we need to do some gymnastics to remove the switch if
* there are no other cases */
-#if defined(CONFIG_TK1_SMMU) || defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
+#if defined(CONFIG_TK1_SMMU) || defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || !defined(CONFIG_ENABLE_SMP_SUPPORT)
switch (cap_get_capType(cap)) {
#ifdef CONFIG_TK1_SMMU
case cap_io_space_cap:
@@ -565,6 +591,11 @@ exception_t Arch_decodeInvocation(word_t invLabel, word_t length, cptr_t cptr,
case cap_vcpu_cap:
return decodeARMVCPUInvocation(invLabel, length, cptr, slot, cap, call, buffer);
#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ return decodeSGISignalInvocation(invLabel, length, cap, buffer);
+#endif /* end of !CONFIG_ENABLE_SMP_SUPPORT */
+
default:
#else
{
diff --git a/src/arch/arm/64/object/objecttype.c b/src/arch/arm/64/object/objecttype.c
index fb4ea77c4..51a1afbb3 100644
--- a/src/arch/arm/64/object/objecttype.c
+++ b/src/arch/arm/64/object/objecttype.c
@@ -73,6 +73,13 @@ deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
ret.status = EXCEPTION_NONE;
return ret;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ ret.cap = cap;
+ ret.status = EXCEPTION_NONE;
+ return ret;
+#endif
+
#ifdef CONFIG_ARM_SMMU
case cap_sid_control_cap:
case cap_cb_control_cap:
@@ -177,6 +184,13 @@ finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
}
break;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ // do nothing
+ break;
+#endif
+
+
#ifdef CONFIG_ARM_SMMU
case cap_cb_cap:
if (cap_cb_cap_get_capBindSID(cap) != SID_INVALID) {
@@ -249,6 +263,17 @@ bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
}
break;
#endif
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ if (cap_get_capType(cap_b) == cap_sgi_signal_cap) {
+ return (cap_sgi_signal_cap_get_capSGIIRQ(cap_a) ==
+ cap_sgi_signal_cap_get_capSGIIRQ(cap_b) &&
+ cap_sgi_signal_cap_get_capSGITarget(cap_a) ==
+ cap_sgi_signal_cap_get_capSGITarget(cap_b));
+ }
+ break;
+#endif
+
#ifdef CONFIG_ARM_SMMU
case cap_sid_control_cap:
if (cap_get_capType(cap_b) == cap_sid_control_cap ||
@@ -470,12 +495,16 @@ exception_t Arch_decodeInvocation(word_t label, word_t length, cptr_t cptr,
/* The C parser cannot handle a switch statement with only a default
* case. So we need to do some gymnastics to remove the switch if
* there are no other cases */
-#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_ARM_SMMU) || defined(CONFIG_ALLOW_SMC_CALLS)
+#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_ARM_SMMU) || defined(CONFIG_ALLOW_SMC_CALLS) || !defined(CONFIG_ENABLE_SMP_SUPPORT)
switch (cap_get_capType(cap)) {
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
case cap_vcpu_cap:
return decodeARMVCPUInvocation(label, length, cptr, slot, cap, call, buffer);
#endif /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ case cap_sgi_signal_cap:
+ return decodeSGISignalInvocation(label, length, cap, buffer);
+#endif /* end of !CONFIG_ENABLE_SMP_SUPPORT */
#ifdef CONFIG_ARM_SMMU
case cap_sid_control_cap:
return decodeARMSIDControlInvocation(label, length, cptr, slot, cap, call, buffer);
diff --git a/src/arch/arm/machine/gic_v2.c b/src/arch/arm/machine/gic_v2.c
index 40a7e5521..664e94b24 100644
--- a/src/arch/arm/machine/gic_v2.c
+++ b/src/arch/arm/machine/gic_v2.c
@@ -175,6 +175,16 @@ BOOT_CODE void cpu_initLocalIRQController(void)
cpu_iface_init();
}
+bool_t plat_SGITargetValid(word_t target)
+{
+ return target < GIC_SGI_NUM_TARGETS;
+}
+
+void plat_sendSGI(word_t irq, word_t target)
+{
+ gic_dist->sgi_control = (BIT(target) << (GICD_SGIR_CPUTARGETLIST_SHIFT)) | (irq << GICD_SGIR_SGIINTID_SHIFT);
+}
+
#ifdef ENABLE_SMP_SUPPORT
/*
* 25-24: target lister filter
diff --git a/src/arch/arm/machine/gic_v3.c b/src/arch/arm/machine/gic_v3.c
index d99783921..3621059c4 100644
--- a/src/arch/arm/machine/gic_v3.c
+++ b/src/arch/arm/machine/gic_v3.c
@@ -28,6 +28,9 @@
#define ICC_SGI1R_INTID_SHIFT (24)
#define ICC_SGI1R_AFF1_SHIFT (16)
+#define ICC_SGI1R_AFF2_SHIFT (32)
+#define ICC_SGI1R_AFF3_SHIFT (48)
+#define ICC_SGI1R_RS_SHIFT (44)
#define ICC_SGI1R_IRM_BIT (40)
#define ICC_SGI1R_CPUTARGETLIST_MASK 0xffff
@@ -74,6 +77,17 @@ static inline uint64_t mpidr_to_gic_affinity(void)
return affinity;
}
+static inline uint64_t sgir_word_from_args(word_t irq, word_t target)
+{
+ uint64_t t = target; /* make sure shifts below are on 64 bit */
+ return (uint64_t) irq << ICC_SGI1R_INTID_SHIFT
+ | (1llu << (t & 0xf)) // AFF0 base
+ | ((t >> 4) & 0x0f) << ICC_SGI1R_RS_SHIFT // AFF0 Range select
+ | ((t >> 8) & 0xff) << ICC_SGI1R_AFF1_SHIFT // AFF1
+ | ((t >> 16) & 0xff) << ICC_SGI1R_AFF2_SHIFT // AFF2
+ | ((t >> 24) & 0xff) << ICC_SGI1R_AFF2_SHIFT; // AFF3
+}
+
/* Wait for completion of a distributor change */
/** DONT_TRANSLATE */
static uint32_t gicv3_do_wait_for_rwp(volatile uint32_t *ctlr_addr)
@@ -343,6 +357,18 @@ BOOT_CODE void cpu_initLocalIRQController(void)
cpu_iface_init();
}
+bool_t plat_SGITargetValid(word_t target)
+{
+ return target < GIC_SGI_NUM_TARGETS;
+}
+
+void plat_sendSGI(word_t irq, word_t target)
+{
+ uint64_t sgi1r_base = sgir_word_from_args(irq, target);
+ SYSTEM_WRITE_64(ICC_SGI1R_EL1, sgi1r_base);
+ isb();
+}
+
#ifdef ENABLE_SMP_SUPPORT
#define MPIDR_MT(x) (x & BIT(24))
diff --git a/src/arch/arm/object/interrupt.c b/src/arch/arm/object/interrupt.c
index d9c719ac9..9b759bc6b 100644
--- a/src/arch/arm/object/interrupt.c
+++ b/src/arch/arm/object/interrupt.c
@@ -18,6 +18,17 @@ static exception_t Arch_invokeIRQControl(irq_t irq, cte_t *handlerSlot, cte_t *c
return invokeIRQControl(irq, handlerSlot, controlSlot);
}
+
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+
+static exception_t Arch_invokeIssueSGISignal(word_t irq, word_t target, cte_t *sgiSlot, cte_t *controlSlot)
+{
+ cteInsert(cap_sgi_signal_cap_new(target, irq), controlSlot, sgiSlot);
+ return EXCEPTION_NONE;
+}
+
+#endif
+
exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
cte_t *srcSlot, word_t *buffer)
{
@@ -77,6 +88,52 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
return Arch_invokeIRQControl(irq, destSlot, srcSlot, trigger);
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+ } else if (invLabel == ARMIRQIssueSGISignal) {
+ if (length < 3 || current_extra_caps.excaprefs[0] == NULL) {
+ userError("IRQControl: IssueSGISignal: Truncated message.");
+ current_syscall_error.type = seL4_TruncatedMessage;
+ return EXCEPTION_SYSCALL_ERROR;
+ }
+ word_t irq = getSyscallArg(0, buffer);
+ word_t target = getSyscallArg(1, buffer);
+ word_t index = getSyscallArg(2, buffer);
+ word_t depth = getSyscallArg(3, buffer);
+
+ cap_t cnodeCap = current_extra_caps.excaprefs[0]->cap;
+
+ if (irq >= NUM_SGIS) {
+ current_syscall_error.type = seL4_RangeError;
+ current_syscall_error.rangeErrorMin = 0;
+ current_syscall_error.rangeErrorMax = NUM_SGIS -1;
+ userError("IRQControl: IssueSGISignal: Invalid SGI IRQ 0x%lx.", irq);
+ return EXCEPTION_SYSCALL_ERROR;
+ }
+
+ if (!plat_SGITargetValid(target)) {
+ current_syscall_error.type = seL4_InvalidArgument;
+ userError("IRQControl: IssueSGISignal: Invalid SGI Target 0x%lx.", target);
+ return EXCEPTION_SYSCALL_ERROR;
+ }
+
+ lookupSlot_ret_t lu_ret = lookupTargetSlot(cnodeCap, index, depth);
+ if (lu_ret.status != EXCEPTION_NONE) {
+ userError("IRQControl: IssueSGISignal: Target slot for new ARM_SGI_Signal cap invalid: cap %lu.",
+ getExtraCPtr(buffer, 0));
+ return lu_ret.status;
+ }
+ cte_t *destSlot = lu_ret.slot;
+
+ exception_t status = ensureEmptySlot(destSlot);
+ if (status != EXCEPTION_NONE) {
+ userError("IRQControl: IssueSGISignal: Target slot for new ARM_SGI_Signal cap not empty: cap %lu.",
+ getExtraCPtr(buffer, 0));
+ return status;
+ }
+ setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
+ return Arch_invokeIssueSGISignal(irq, target, destSlot, srcSlot);
+
+#endif
#ifdef ENABLE_SMP_SUPPORT
} else if (invLabel == ARMIRQIssueIRQHandlerTriggerCore) {
word_t irq_w = getSyscallArg(0, buffer);
@@ -135,3 +192,24 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
return EXCEPTION_SYSCALL_ERROR;
}
}
+
+#ifndef CONFIG_ENABLE_SMP_SUPPORT
+
+static exception_t invokeSGISignalGenerate(word_t irq, word_t target)
+{
+ plat_sendSGI(irq, target);
+ return EXCEPTION_NONE;
+}
+
+
+exception_t decodeSGISignalInvocation(word_t invLabel, word_t length,
+ cap_t cap, word_t *buffer)
+{
+
+ word_t irq = cap_sgi_signal_cap_get_capSGIIRQ(cap);
+ word_t target = cap_sgi_signal_cap_get_capSGITarget(cap);
+
+ setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
+ return invokeSGISignalGenerate(irq, target);
+}
+#endif /* !CONFIG_ENABLE_SMP_SUPPORT */
diff --git a/src/object/objecttype.c b/src/object/objecttype.c
index ca796a5da..4bb2598c3 100644
--- a/src/object/objecttype.c
+++ b/src/object/objecttype.c
@@ -342,6 +342,9 @@ bool_t CONST sameRegionAs(cap_t cap_a, cap_t cap_b)
case cap_irq_control_cap:
if (cap_get_capType(cap_b) == cap_irq_control_cap ||
+#if CONFIG_MAX_NUM_NODES == 1
+ cap_get_capType(cap_b) == cap_sgi_signal_cap ||
+#endif
cap_get_capType(cap_b) == cap_irq_handler_cap) {
return true;
}
@@ -389,6 +392,12 @@ bool_t CONST sameObjectAs(cap_t cap_a, cap_t cap_b)
cap_get_capType(cap_b) == cap_irq_handler_cap) {
return false;
}
+#if CONFIG_MAX_NUM_NODES == 1
+ if (cap_get_capType(cap_a) == cap_irq_control_cap &&
+ cap_get_capType(cap_b) == cap_sgi_signal_cap) {
+ return false;
+ }
+#endif
if (isArchCap(cap_a) && isArchCap(cap_b)) {
return Arch_sameObjectAs(cap_a, cap_b);
}