-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
4 changed files
with
721 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,153 @@ | ||
<!-- | ||
SPDX-License-Identifier: CC-BY-SA-4.0 | ||
Copyright 2024 Ben Leslie | ||
--> | ||
|
||
# The seL4 Microkit | ||
|
||
(Previous title: "seL4 Core Platform") | ||
|
||
- Author: Ben Leslie | ||
- Proposed: 2020-11-19 | ||
- Implementation repository: <https://github.com/seL4/microkit> | ||
- Current manual: <https://github.com/seL4/microkit/blob/main/docs/manual.md> | ||
|
||
## Summary | ||
|
||
The seL4 Microkit is an operating system (OS) personality for the seL4 | ||
microkernel. | ||
|
||
The purpose of seL4 Microkit is to: | ||
|
||
- provide a small and simple OS for a wide range of IoT, cyber physical and | ||
other embedded use cases; | ||
|
||
- provide a reasonable degree of application portability appropriate for the | ||
targeted use cases; | ||
|
||
- make seL4-based systems easy to develop and deploy within the target areas; | ||
|
||
## Motivation | ||
|
||
The seL4 microkernel provides a set of powerful and flexible mechanisms that can | ||
be used for building almost arbitrary systems. While minimising constraints on | ||
the nature of system designs and scope of deployments, this flexibility makes it | ||
challenging to design the best system for a particular use case, requiring | ||
extensive seL4 experience from developers. | ||
|
||
The seL4 software ecosystem currently provides various options for developing | ||
systems on seL4, however, such support is both overly broad (providing too many | ||
options) and simultaneously too limited for many developers. | ||
|
||
The seL4 Microkit addresses this challenge by constraining the system | ||
architecture and to one that provides enough features and power for this usage | ||
class, enabling a much simpler set of developer-visible abstractions. | ||
|
||
The goals of the microkit are to: | ||
|
||
- provide well-defined hardware interfaces to ease porting of the microkit; | ||
|
||
- support a high degree of code reuse between deployments; | ||
|
||
- provide well-defined internal interfaces to support diverse implementations of | ||
the same logical service to adapt to usage-specific trade-offs and ease | ||
compatibility between implementation of system services from different | ||
developers; | ||
|
||
- leverage seL4's strong isolation properties to support a near-minimal trusted | ||
computing base (TCB); | ||
|
||
- retain seL4's trademark performance for systems built with it; | ||
|
||
- be, in principle, amenable to formal analysis of system safety and security | ||
properties (although such analysis is beyond the initial scope). | ||
|
||
## Guide-level explanation | ||
|
||
The seL4 Microkit consists of: | ||
|
||
- an seL4 Microkit specification, which defines the key abstractions | ||
and Microkit API | ||
|
||
- an seL4 Microkit implementation, which provides implementations of the key | ||
abstractions and API | ||
|
||
- definitions of key OS service interfaces and implementations of these | ||
|
||
## Scope | ||
|
||
The initial focus and scope of this RFC is on defining the key seL4 Microkit | ||
abstractions, which build on seL4 abstractions. | ||
|
||
The seL4 Microkit abstractions are: | ||
|
||
- processor core (core) | ||
- protection domain (PD) | ||
- communication channel (CC) | ||
- memory region | ||
- notification | ||
- protected procedure call (PPC) | ||
- virtual machine (VM) | ||
|
||
More details about these abstractions, and how they build on seL4 abstractions, | ||
are available in | ||
<https://github.com/BreakawayConsulting/platform-sel4-docs/blob/master/sel4-platform.md> | ||
|
||
## Reference-level explanation | ||
|
||
While this RFC initially targets the main microkit abstractions, ultimately the | ||
microkit will provide an SDK (including interfaces, libraries, services, and | ||
tools) for building seL4 Microkit based systems. | ||
|
||
The microkit implementation (and SDK) could be based on, and incorporate, | ||
existing technology such as CAmkES, capDL, seL4 runtime, seL4 driver framework, | ||
etc. however this has not been decided yet. | ||
|
||
The seL4 Microkit will initially be limited to a small set of hardware | ||
platforms. This is to ensure that effort is focussed on fully supporting the | ||
microkit on this hardware. Ports to other hardware can be contributed by | ||
others. | ||
|
||
## Drawbacks | ||
|
||
The RFC currently only presents the seL4 Microkit concepts. These have not yet | ||
been implemented nor have they yet been used to build concrete systems. | ||
|
||
While the intention of the seL4 Microkit is to focus seL4 ecosystem and | ||
developer effort on a single (well defined and supported) model, the danger is | ||
that it adds yet another set of tools and platforms/frameworks to the mix making | ||
it even less clear what developers should use. | ||
|
||
## Rationale and alternatives | ||
|
||
The intention is that experience from building seL4-based systems and developing | ||
and using previous existing platforms/frameworks/libraries/tools will lead to a | ||
more suitable and usable platform definition that will supersede some of the | ||
earlier platforms/frameworks/libraries/tools and that new (and existing) | ||
developers will migrate to the seL4 Microkit. | ||
|
||
## Prior art | ||
|
||
Prior (and similar) art includes: | ||
|
||
- CAmkES | ||
- Genode | ||
- TRENTOS | ||
- AADL and HAMR | ||
- feL4 | ||
- various other (ad hoc) software | ||
|
||
## Unresolved questions | ||
|
||
This RFC addresses the first step towards defining the full seL4 Microkit. | ||
|
||
It does not provide a roadmap to the further steps. | ||
|
||
## Disposition | ||
|
||
The TSC has approved this RFC in its 12 Sep 2023 meeting and also approved | ||
a name change to the Microkit (or seL4 Microkit if context is needed). | ||
|
||
The design concerns from previous meetings have been addressed and | ||
implementation is expected to converge to that design. The repository will be | ||
moved to the seL4 GitHub organisation. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,185 @@ | ||
<!-- | ||
SPDX-License-Identifier: CC-BY-SA-4.0 | ||
Copyright 2024 Kry10 | ||
--> | ||
|
||
# seL4 multikernel IPI API | ||
|
||
- Author: Kent McLeod | ||
- Proposed: 2024-02-13 | ||
|
||
- Implementation PR: [seL4/seL4#1222] | ||
- Verification PR: [seL4/l4v#733] | ||
|
||
## Summary | ||
|
||
Proposal to add an seL4 capability to generate interprocessor interrupts (IPIs). | ||
|
||
## Motivation | ||
|
||
There's a proposed approach for enabling multicore seL4 while still using | ||
verified single-core configurations -- a partitioned multikernel. | ||
|
||
As part of this approach, we need a way to both send and receive asynchronous | ||
signals between different cores in a system. Receiving IPIs from other cores is | ||
currently supported by existing IRQ handling mechanisms. We need to add a new | ||
mechanism for sending asynchronous signals to another core by generating IPIs. | ||
|
||
It's desirable for this mechanism to have minimal verification effort to add to | ||
the baseline verified kernel implementations. | ||
|
||
It could also be desirable for this mechanism to be able to scale from a couple | ||
of cores up to very large multicore systems with tens or even hundreds of cores. | ||
|
||
## Guide-level explanation | ||
|
||
There are already hardware IPI mechanisms present on all supported platforms | ||
that the SMP kernel uses for sending and receiving signals between multiple | ||
cores. We can use the same mechanisms but give user level more direct access via | ||
additional APIs for generating and receiving IPIs directly. This would allow | ||
each single-core kernel instance to be able to send interrupts to other kernels | ||
and receive interrupts from other kernels while having zero shared kernel state | ||
between cores. Each kernel can think of the other kernels as just devices that | ||
they can send and receive interrupts between each other, and delegate any shared | ||
memory access to user level. | ||
|
||
Breaking this new API up into two parts: | ||
|
||
- we need a way to send interrupts to a remote core from user space, | ||
|
||
- and we need a way to receive interrupts from a remote core and deliver them to | ||
user space. | ||
|
||
Sending interrupts involves creating a new capability type, an IPI cap, that can | ||
be created from an IRQ control cap. | ||
|
||
- The IRQControl invocation to create the new IPI cap encodes any | ||
hardware-specific configuration that will be used whenever the IPI cap is | ||
invoked. | ||
|
||
- The IPI Cap is invoked in the same way as a notification send cap. The sender | ||
cannot be blocked and the kernel is expected to deliver at-most-one event to | ||
the target receiver. | ||
|
||
- The target receiver is going to be running in user space on a remote core. | ||
|
||
- 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. | ||
|
||
It is already possible to register send-notification-caps that are invoked when | ||
an interrupt is received so receiving IPIs doesn't require adding any new caps | ||
and only requires limited `IRQControlCap` invocation changes on some platforms. | ||
|
||
- The architecture specific IRQControl invocation for creating IRQ handler caps | ||
will need to allow creating IRQ caps for receiving IPIs. | ||
|
||
- Then these will work with notification objects the same as all other IRQ | ||
handler caps. | ||
|
||
- On Arm it's already possible to request IRQ caps to the IPI interrupt IDs so | ||
no changes are required. | ||
|
||
- On RISC-V the IRQControl invocation will need to be extended to allow the SWI | ||
interrupt to be delivered to user level. | ||
|
||
- On x86 it should already be possible to receive IRQs for a specified vector | ||
and so changes to the IRQControl invocation shouldn't be required. | ||
|
||
## Reference-level explanation | ||
|
||
A quick note on terminology, since each architecture uses a different name for | ||
inter-processor interrupts: | ||
|
||
- x86 = IPI (Inter-processor interrupts) | ||
|
||
- Arm = SGI (Software generated interrupts) | ||
|
||
- RISC-V = SI/SWI (Software interrupts) | ||
|
||
So while this RFC will use IPI to refer to all three, I expect that the new | ||
invocations we add for creating the caps will use the arch specific names as | ||
IRQs are currently all handled by arch specific invocations. | ||
|
||
Sending IPIs is dependent on the platform's interrupt controller. | ||
|
||
- on Arm cores that use the Generic Interrupt Controller, there are 16 different | ||
interrupt IDs that can be used to receive IPIs on. A core can thus send up to | ||
16 different signals to each target. Once more signals are required, the | ||
interrupt IDs must be reused and a user-space shared memory protocol is needed | ||
to distinguish between messages. | ||
|
||
- on RISC-V cores there is only one interrupt ID for an IPI. A core can send | ||
IPIs to multiple cores at once using the SBI API. | ||
|
||
- on x86 cores IPIs can have an arbitrary vector ID between 0 and 255 (excluding | ||
reserved vectors). Sending an IPI can be to any target and with any vector. | ||
|
||
At a minimum this is sufficient to build a user level component that implements | ||
more sophisticated software signal multiplexing over a single hardware | ||
interrupt. This approach creates no shared kernel state and avoids concurrency. | ||
|
||
## Drawbacks | ||
|
||
Some scalability limitations include: | ||
|
||
- Using different interrupt lines to distinguish cores requires there's at least | ||
as many IRQ lines available for IPIs as there are cores in the system. This is | ||
not typically the case. When there's more cores than IRQ lines, distinguishing | ||
cores apart requires an additional shared memory protocol that must be | ||
implemented at user level. | ||
|
||
## Rationale and alternatives | ||
|
||
Platform specific extensions: | ||
|
||
On Arm, the GICv2 and GICv3 have 16 lines reserved for SGI. This allows 16 | ||
different channels to be supported on each core. This may be helpful for systems | ||
that want to support direct software signalling without having to implement a | ||
user level component assuming their requirements are simple enough. | ||
|
||
Future steps may involve seeking to use a method that involves direct memory | ||
access between cores allowing shared memory to be used for more information to | ||
be associated with each interrupt. However this leads to increased complexity | ||
around designing and implementing protocols that can guarantee at-least-once | ||
delivery of all signals with reasonable scalability overhead. | ||
|
||
## Prior art | ||
|
||
– `seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)` has existed for several | ||
years as a debug function for generating SGIs on ARM platforms. The current | ||
proposal takes this functionality and adds capability management for it. (As | ||
well as adding support for interrupting multiple targets as supported by GICv2 | ||
and GICv3). | ||
|
||
## Unresolved questions | ||
|
||
The current proposed implementation is here, but it’s awaiting a minor update to | ||
the revoke paths as part of some ongoing verification work: | ||
<https://github.com/seL4/seL4/commit/7fda970d382c034c4e9b6d49b10bfbe33d4f815f> | ||
|
||
## Disposition | ||
|
||
The TSC approved the RFC with the following conditions: | ||
|
||
- The RFC should be updated to remove the API for broadcast and multicast for | ||
now. Until we have figured out a good general model for multicast, we want to | ||
keep the API small so that conservative extensions are possible. The rationale | ||
is that for the current use case of a low number (2-16) of cores, it is cheap | ||
to simulate multicast and broadcast in user space via a loop over caps to each | ||
of the core, whereas it will be hard to change the API later if we commit to a | ||
specific multicast model too early. This means, the `SGISignalCap` (on Arm) | ||
should authorise sending to a single core (and store a single SGI number). | ||
|
||
- The API for Arm should be updated to include higher affinity bits for GICv3 to | ||
support sending to more cores. For platforms that do not support these bits | ||
(e.g. GICv2), the corresponding `IRQControl` invocation should fail if those | ||
bits are attempted to be set. | ||
|
||
- The TSC confirmed that we want the API for invoking `SGISignalCaps` to be like | ||
notifications, that is, the invocation should not take any parameters beside | ||
the `SGISignal` cap itself. The current (not yet updated) pull request for this | ||
RFC is [seL4/seL4#1222]. | ||
|
||
[seL4/seL4#1222]: https://github.com/seL4/seL4/pull/1222 | ||
[seL4/l4v#733]: https://github.com/seL4/l4v/pull/733 |
Oops, something went wrong.