Add new APIs for generating SGIs #1222

lsf37 · 2024-03-14T13:45:21Z

This is work by @kent-mcleod, with an additional commit on top from myself with verification tweaks for this new API.

For design rationale and background on the API in this PR see RFC-17.

Edit: this also fixes a bug in the evaluation of XML condition expressions for the manual, which gets triggered by this PR.

lsf37 · 2024-03-14T13:46:10Z

@kent-mcleod could you please add the sign-off to your commit?

Allow SGIs to be generated from non-SMP kernels. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

- introduce arch interface for IRQControlCap dependencies as well as for isMDBParentOf (Arch_isIRQControlDescendant, Arch_isMDBParentOf). This mirrors the corresponding interface in the proofs and Haskell and avoids #ifdef proliferation in generic code. - Arch_isIRQControlDescendant is currently only used for SGISignalCaps - Arch_isMDBParentOf is used for SGISignalCaps and SMCCaps - fix argument checking in Arch_decodeIRQControlInvocation (+ style tweak) - Arch_sameObjectAs must return false for SGISignalCaps to align with finality definition of caps, i.e. SGISignalCaps are always final. This has no behaviour change, because finality doesn't matter for behaviour for SGISignalCaps, but we require for the proofs that the concept of finality aligns with the spec. - simplify checks for IRQControlCap in sameObjectAs: sameObjectAs can never be true for IRQControlCap. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Indanz

I can't think of any useful use case where the user would want to send IPIs to multiple cores and knows which those are beforehand, with the only exception being all other cores.

I don't think supporting sending multiple IPIs at once is necessary or worth the added complexity. But if it is added, it should fully expose the hardware in a useful way. The current implementation is limited to systems with one cluster of at most 16 cores.

With that in mind, I propose the API is changed to either allowing only one target core, or:

Add a mask parameter to the call which is ANDed with the configured mask.
Configure Aff1, Aff2 and Aff3 at creation time (but good luck to user space figuring out what they need to fill in though).
Give an option to send to all other cores (IRM = 1).
Expose RS.

Then at least the API is future proof for a while, till ARM comes with a new interface for sending multiple IPIs. Mind that with the above changes it probably doesn't make any sense to share ipi_send_target().

Indanz · 2024-03-14T14:07:16Z

src/arch/arm/machine/gic_v3.c

-        }
-    }
+
+    SYSTEM_WRITE_64(ICC_SGI1R_EL1, sgi1r_base | cpuTargetList);


This seems to assume zero aff1, aff2 and aff3? Probably true for currently supported platforms, but it doesn't seem future proof.

Indanz · 2024-03-14T14:30:17Z

src/arch/arm/object/interrupt.c

@@ -77,6 +90,54 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,

        setThreadState(NODE_STATE(ksCurThread), ThreadState_Restart);
        return Arch_invokeIRQControl(irq, destSlot, srcSlot, trigger);
+#if CONFIG_MAX_NUM_NODES == 1
+    } else if (invLabel == ARMIRQIssueSGISignal) {


I would add this to the end of the function, after ARMIRQIssueIRQHandlerTriggerCore, perhaps as an #else for ENABLE_SMP_SUPPORT?

I like it slightly better here. The case is very close in content (which checks it does) to ARMIRQIssueIRQHandlerTrigger. Moving it further away will mean they will diverge more easily.

Fair enough.

Having both ENABLE_SMP_SUPPORT and CONFIG_MAX_NUM_NODES == 1 next to each other is very weird though. What about #ifnde ENABLE_SMP_SUPPORT and then an else?

Also, wouldn't it make more sense to test for #ifndef ENABLE_SMP_SUPPORT everywhere? CONFIG_MAX_NUM_NODES == 1 is used nowhere else.

Indanz · 2024-03-14T14:55:24Z

libsel4/arch_include/arm/interfaces/sel4arch.xml

+        <method id="ARMIRQIssueSGISignal" name="IssueSGISignal" manual_name="IssueSGISignal"
+           manual_label="irq_controlissuesgisignal" condition="CONFIG_MAX_NUM_NODES == 1">
+            <brief>
+                Create an SGI signal capability.


Suggested change

Create an SGI signal capability.

Create a software generated interrupt (SGI) signal capability.

Indanz · 2024-03-14T15:18:46Z

libsel4/arch_include/arm/interfaces/sel4arch.xml

+            <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."/>


Suggested change

<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="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."/>

Fix condition syntax; comparison operators are currently not supported in the XML description conditions. Use `!CONFIG_ENABLE_SMP_SUPPORT` instead, which equivalent to `CONFIG_MAX_NUM_NODES == 1`. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

When evaluating XML condition expressions, properly treat undefined values as undefined, not as False. Otherwise, the negation of an undefined value may make an entire expression true and incorrectly label some methods as MCS methods. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 · 2024-03-14T16:19:21Z

It's a bit early to review the PR (should have left it on draft). We should sort out the API in the RFC discussion first.

lsf37 · 2024-03-14T16:21:13Z

@kent-mcleod there are a few Arm platforms that don't use gic_v2.h or gic_v3.h, which means they are currently not defining the right interface functions. If the RFC is accepted, these will need to be added.

Indanz · 2024-03-14T16:33:08Z

It's a bit early to review the PR (should have left it on draft). We should sort out the API in the RFC discussion first.

The RFC is higher level and doesn't propose a specific API though, it actually says:

For the first implementation we'll only support unicast signalling, but broadcast and multicast functionality can be added later via extensions to the IRQControl invocation that creates the IPI cap.

lsf37 · 2024-03-14T19:42:36Z

It's a bit early to review the PR (should have left it on draft). We should sort out the API in the RFC discussion first.

The RFC is higher level and doesn't propose a specific API though, it actually says:

For the first implementation we'll only support unicast signalling, but broadcast and multicast functionality can be added later via extensions to the IRQControl invocation that creates the IPI cap.

Fair enough, the code actually has slightly more than the RFC proposes. We should update the RFC then, the API decisions need to be there.

kent-mcleod · 2024-03-14T23:09:36Z

* Add a mask parameter to the call which is ANDed with the configured mask.

This was in the earliest iteration of the design, but was taken out in favor of having 0 arguments to the call so that the capability could be interchanged with a regular Notification capability with send rights.

* Configure `Aff1`, `Aff2` and `Aff3` at creation time (but good luck to user space figuring out what they need to fill in though).

* Give an option to send to all other cores (`IRM = 1`).

In principle, the capabilities of the hardware should be exposed, so I agree that higher order affinities and IRM could be configured at cap creation time, and equivalent for GICv2 (which doesn't support affinity routing but does support broadcast). There's also potentially a future need to select a different interrupt group or security state, which is encoded by which SGIR is used. There's enough spare bits in the capability to encode all of these options, but we don't have an easy setup to test the different combinations.

* Expose `RS`.

I'm not sure what RS refers to.

axel-h · 2024-03-14T23:57:31Z

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

@@ -102,6 +102,22 @@ block vcpu_cap {
 }
 #endif

+#if CONFIG_MAX_NUM_NODES == 1


Why don't we check CONFIG_SMP_ENABLED here and in the other places? Or add a dedicated feature define for this, so using CONFIG_MAX_NUM_NODES directly is avoided. On RISC-V I have been running into some use cases now where having certain multi core feature available even with just one seL4 core comes handy and the checks for CONFIG_MAX_NUM_NODES are a pain then.

Indanz · 2024-03-15T09:27:31Z

Fair enough, the code actually has slightly more than the RFC proposes. We should update the RFC then, the API decisions need to be there.

I'm happy to move the discussion to the RFC.

I'm not sure what RS refers to.

It enables range selector, in case max 256 cores at Aff0 are supported.

The only future proof way is to store the full 64 bits, then the API doesn't need to change if ARM uses one of the reserved bits in the future. 32-bit ARM should be stable enough by now.

kent-mcleod · 2024-03-22T04:08:19Z

It enables range selector, in case max 256 cores at Aff0 are supported.

Ah, I've only been working off of the gicv3.0 manual because we don't have any plans for platforms with the higher revisions at this stage.

kent-mcleod and others added 2 commits March 14, 2024 14:48

arm: Add new APIs for generating SGIs

b2bc0e4

Allow SGIs to be generated from non-SMP kernels. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 force-pushed the lsf37/arm-sgi branch from 0d4fe26 to 870c81b Compare March 14, 2024 13:48

lsf37 mentioned this pull request Mar 14, 2024

Proofs for SGI API seL4/l4v#733

Draft

lsf37 added verification Needs formal verification input/change, or is motivated by verification enhancement hw-test sel4test hardware builds + runs for this PR labels Mar 14, 2024

Indanz requested changes Mar 14, 2024

View reviewed changes

lsf37 added 2 commits March 14, 2024 17:00

lsf37 marked this pull request as draft March 14, 2024 16:19

axel-h reviewed Mar 14, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add new APIs for generating SGIs #1222

Add new APIs for generating SGIs #1222

lsf37 commented Mar 14, 2024 •

edited

lsf37 commented Mar 14, 2024

Indanz left a comment •

edited

Indanz Mar 14, 2024

Indanz Mar 14, 2024

lsf37 Mar 14, 2024

Indanz Mar 14, 2024 •

edited

Indanz Mar 14, 2024

Indanz Mar 14, 2024

lsf37 commented Mar 14, 2024

lsf37 commented Mar 14, 2024

Indanz commented Mar 14, 2024

lsf37 commented Mar 14, 2024

kent-mcleod commented Mar 14, 2024

axel-h Mar 14, 2024

Indanz commented Mar 15, 2024

kent-mcleod commented Mar 22, 2024

	Create an SGI signal capability.
	Create a software generated interrupt (SGI) signal capability.

		<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."/>

Add new APIs for generating SGIs #1222

Are you sure you want to change the base?

Add new APIs for generating SGIs #1222

Conversation

lsf37 commented Mar 14, 2024 • edited

lsf37 commented Mar 14, 2024

Indanz left a comment • edited

Choose a reason for hiding this comment

Indanz Mar 14, 2024

Choose a reason for hiding this comment

Indanz Mar 14, 2024

Choose a reason for hiding this comment

lsf37 Mar 14, 2024

Choose a reason for hiding this comment

Indanz Mar 14, 2024 • edited

Choose a reason for hiding this comment

Indanz Mar 14, 2024

Choose a reason for hiding this comment

Indanz Mar 14, 2024

Choose a reason for hiding this comment

lsf37 commented Mar 14, 2024

lsf37 commented Mar 14, 2024

Indanz commented Mar 14, 2024

lsf37 commented Mar 14, 2024

kent-mcleod commented Mar 14, 2024

axel-h Mar 14, 2024

Choose a reason for hiding this comment

Indanz commented Mar 15, 2024

kent-mcleod commented Mar 22, 2024

lsf37 commented Mar 14, 2024 •

edited

Indanz left a comment •

edited

Indanz Mar 14, 2024 •

edited