Skip to content

Commit bb712a4

Browse files
lsf37lsf37
committed
import RFC-17
See https://sel4.atlassian.net/browse/RFC-17 Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
1 parent 565cb38 commit bb712a4

File tree

1 file changed

+185
-0
lines changed

1 file changed

+185
-0
lines changed

‎src/active/0170-multikernel-ipi-api.md

+185
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
<!--
2+
SPDX-License-Identifier: CC-BY-SA-4.0
3+
Copyright 2024 Kry10
4+
-->
5+
6+
# seL4 multikernel IPI API
7+
8+
- Author: Kent McLeod
9+
- Proposed: 2024-02-13
10+
11+
- Implementation PR: [seL4/seL4#1222]
12+
- Verification PR: [seL4/l4v#733]
13+
14+
## Summary
15+
16+
Proposal to add an seL4 capability to generate interprocessor interrupts (IPIs).
17+
18+
## Motivation
19+
20+
There's a proposed approach for enabling multicore seL4 while still using
21+
verified single-core configurations -- a partitioned multikernel.
22+
23+
As part of this approach, we need a way to both send and receive asynchronous
24+
signals between different cores in a system. Receiving IPIs from other cores is
25+
currently supported by existing IRQ handling mechanisms. We need to add a new
26+
mechanism for sending asynchronous signals to another core by generating IPIs.
27+
28+
It's desirable for this mechanism to have minimal verification effort to add to
29+
the baseline verified kernel implementations.
30+
31+
It could also be desirable for this mechanism to be able to scale from a couple
32+
of cores up to very large multicore systems with tens or even hundreds of cores.
33+
34+
## Guide-level explanation
35+
36+
There are already hardware IPI mechanisms present on all supported platforms
37+
that the SMP kernel uses for sending and receiving signals between multiple
38+
cores. We can use the same mechanisms but give user level more direct access via
39+
additional APIs for generating and receiving IPIs directly. This would allow
40+
each single-core kernel instance to be able to send interrupts to other kernels
41+
and receive interrupts from other kernels while having zero shared kernel state
42+
between cores. Each kernel can think of the other kernels as just devices that
43+
they can send and receive interrupts between each other, and delegate any shared
44+
memory access to user level.
45+
46+
Breaking this new API up into two parts:
47+
48+
- we need a way to send interrupts to a remote core from user space,
49+
50+
- and we need a way to receive interrupts from a remote core and deliver them to
51+
user space.
52+
53+
Sending interrupts involves creating a new capability type, an IPI cap, that can
54+
be created from an IRQ control cap.
55+
56+
- The IRQControl invocation to create the new IPI cap encodes any
57+
hardware-specific configuration that will be used whenever the IPI cap is
58+
invoked.
59+
60+
- The IPI Cap is invoked in the same way as a notification send cap. The sender
61+
cannot be blocked and the kernel is expected to deliver at-most-one event to
62+
the target receiver.
63+
64+
- The target receiver is going to be running in user space on a remote core.
65+
66+
- For the first implementation we'll only support unicast signalling, but
67+
broadcast and multicast functionality can be added later via extensions to the
68+
IRQControl invocation that creates the IPI cap.
69+
70+
It is already possible to register send-notification-caps that are invoked when
71+
an interrupt is received so receiving IPIs doesn't require adding any new caps
72+
and only requires limited `IRQControlCap` invocation changes on some platforms.
73+
74+
- The architecture specific IRQControl invocation for creating IRQ handler caps
75+
will need to allow creating IRQ caps for receiving IPIs.
76+
77+
- Then these will work with notification objects the same as all other IRQ
78+
handler caps.
79+
80+
- On Arm it's already possible to request IRQ caps to the IPI interrupt IDs so
81+
no changes are required.
82+
83+
- On RISC-V the IRQControl invocation will need to be extended to allow the SWI
84+
interrupt to be delivered to user level.
85+
86+
- On x86 it should already be possible to receive IRQs for a specified vector
87+
and so changes to the IRQControl invocation shouldn't be required.
88+
89+
## Reference-level explanation
90+
91+
A quick note on terminology, since each architecture uses a different name for
92+
inter-processor interrupts:
93+
94+
- x86 = IPI (Inter-processor interrupts)
95+
96+
- Arm = SGI (Software generated interrupts)
97+
98+
- RISC-V = SI/SWI (Software interrupts)
99+
100+
So while this RFC will use IPI to refer to all three, I expect that the new
101+
invocations we add for creating the caps will use the arch specific names as
102+
IRQs are currently all handled by arch specific invocations.
103+
104+
Sending IPIs is dependent on the platform's interrupt controller.
105+
106+
- on Arm cores that use the Generic Interrupt Controller, there are 16 different
107+
interrupt IDs that can be used to receive IPIs on. A core can thus send up to
108+
16 different signals to each target. Once more signals are required, the
109+
interrupt IDs must be reused and a user-space shared memory protocol is needed
110+
to distinguish between messages.
111+
112+
- on RISC-V cores there is only one interrupt ID for an IPI. A core can send
113+
IPIs to multiple cores at once using the SBI API.
114+
115+
- on x86 cores IPIs can have an arbitrary vector ID between 0 and 255 (excluding
116+
reserved vectors). Sending an IPI can be to any target and with any vector.
117+
118+
At a minimum this is sufficient to build a user level component that implements
119+
more sophisticated software signal multiplexing over a single hardware
120+
interrupt. This approach creates no shared kernel state and avoids concurrency.
121+
122+
## Drawbacks
123+
124+
Some scalability limitations include:
125+
126+
- Using different interrupt lines to distinguish cores requires there's at least
127+
as many IRQ lines available for IPIs as there are cores in the system. This is
128+
not typically the case. When there's more cores than IRQ lines, distinguishing
129+
cores apart requires an additional shared memory protocol that must be
130+
implemented at user level.
131+
132+
## Rationale and alternatives
133+
134+
Platform specific extensions:
135+
136+
On Arm, the GICv2 and GICv3 have 16 lines reserved for SGI. This allows 16
137+
different channels to be supported on each core. This may be helpful for systems
138+
that want to support direct software signalling without having to implement a
139+
user level component assuming their requirements are simple enough.
140+
141+
Future steps may involve seeking to use a method that involves direct memory
142+
access between cores allowing shared memory to be used for more information to
143+
be associated with each interrupt. However this leads to increased complexity
144+
around designing and implementing protocols that can guarantee at-least-once
145+
delivery of all signals with reasonable scalability overhead.
146+
147+
## Prior art
148+
149+
– `seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)` has existed for several
150+
years as a debug function for generating SGIs on ARM platforms. The current
151+
proposal takes this functionality and adds capability management for it. (As
152+
well as adding support for interrupting multiple targets as supported by GICv2
153+
and GICv3).
154+
155+
## Unresolved questions
156+
157+
The current proposed implementation is here, but it’s awaiting a minor update to
158+
the revoke paths as part of some ongoing verification work:
159+
<https://github.com/seL4/seL4/commit/7fda970d382c034c4e9b6d49b10bfbe33d4f815f>
160+
161+
## Disposition
162+
163+
The TSC approved the RFC with the following conditions:
164+
165+
- The RFC should be updated to remove the API for broadcast and multicast for
166+
now. Until we have figured out a good general model for multicast, we want to
167+
keep the API small so that conservative extensions are possible. The rationale
168+
is that for the current use case of a low number (2-16) of cores, it is cheap
169+
to simulate multicast and broadcast in user space via a loop over caps to each
170+
of the core, whereas it will be hard to change the API later if we commit to a
171+
specific multicast model too early. This means, the `SGISignalCap` (on Arm)
172+
should authorise sending to a single core (and store a single SGI number).
173+
174+
- The API for Arm should be updated to include higher affinity bits for GICv3 to
175+
support sending to more cores. For platforms that do not support these bits
176+
(e.g. GICv2), the corresponding `IRQControl` invocation should fail if those
177+
bits are attempted to be set.
178+
179+
- The TSC confirmed that we want the API for invoking `SGISignalCaps` to be like
180+
notifications, that is, the invocation should not take any parameters beside
181+
the `SGISignal` cap itself. The current (not yet updated) pull request for this
182+
RFC is [seL4/seL4#1222].
183+
184+
[seL4/seL4#1222]: https://github.com/seL4/seL4/pull/1222
185+
[seL4/l4v#733]: https://github.com/seL4/l4v/pull/733

0 commit comments

Comments
 (0)