From ac2ac9aa36d26ed387fdc730583e1d66cfd2b58d Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Tue, 7 Jul 2026 13:41:10 +1000 Subject: [PATCH 1/3] extremely draft RFC: post-initialiser domain Signed-off-by: Terry Bai --- src/proposed/998-post-initialiser-rfc.md | 87 ++++++++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 src/proposed/998-post-initialiser-rfc.md diff --git a/src/proposed/998-post-initialiser-rfc.md b/src/proposed/998-post-initialiser-rfc.md new file mode 100644 index 0000000..436d04a --- /dev/null +++ b/src/proposed/998-post-initialiser-rfc.md @@ -0,0 +1,87 @@ +# Post-initialiser RFC + +- Author: Zoltan, Julia, Terry +- Proposed: 2026-07-08 + +## Summary + +This RFC proposes a solution that adds a post-initialisation domain to allow capabilities shared among +user-defined initialiser components without breaking the existing Microkit assumptions on protection domains. + +## Motivation + +On x86, there are two primary requirements for ACPI/PCIe driver: + +Unlike the ARM and RISC-V, x86 systems do not know the resource configurations at build time, and have to figure things out by interacting with the ACPI tables possibly located anywhere in memory. In previous internal meeting, we decided to have [an ACPI driver and a PCIe driver](https://github.com/au-ts/sddf/issues/622) to solve this problem, but the following use cases are not supported by the existing capDL initialiser/Microkit: + +- The ACPI driver needs access to most if not all of the remaining untypeds (and internal information from the capDL initialiser about the watermarks about UTs if used), because: + * It needs to be able to map in all the ACPI tables (the addresses are not fixed nor contiguous, so one needs to map-then-parse-then-map in a loop). , etc). + * It also likely needs to be able to create the (seL4 device) frames for PCIe config space and MMIO windows. + +- The PCIe driver needs the ability to create IO ports, frames, and IRQ capabilities corresponding to a certain PCI device ID; +it also needs to be able to access the PCIe config space (to itself) and parts of the PCIe MMIO window (for other device drivers); these are frames that can be determined by the ACPI driver (from device UT) + +The experimental implementation introduced a `cnode` tag in SDF to allow a custom CNode to be shared by PDs, but raised the [concerns from the verification experts](https://github.com/seL4/microkit/pull/539#issuecomment-4871178574). This feature brings more flexibility to the user CSpace management but breaks the Microkit's assumptions for the verification story. And it does not make sense to introduce a feature but disallow people to use it. + +## Proposals + +Given that both the ACPI driver and PCIe driver run only once before everything else, and they do not need most of features of protection domains in the current Microkit, it makes sense to be moved out from protection domains. + +Zoltan proposed to add an explicit `post-initialiser` feature to run the one-shot code straight after the capDL initialiser. This keeps the Microkit state after `post-initialisation` still same as the assumptions, so does not screw up the verification story. + +The solution could be: + +### 1. Wrapper around the capDL initialiser + +Use the capDL initialiser as a library and extend it with `post-initialisation` code. +(I @terryzbai personally don't think this is reasonable for the components that do not need the access to all the untypeds, e.g., the PCIe driver) + +### 2. Post-initialiser component + +New (non-protected) domains are executed after the capDL initialiser in the `phase` order, and the capabilities can be exchanged between the capDL initialisers. + +The options of capability passing mechanisms: + +1. Restricted CNode sharing between only `post-initialiser` + +CNodes can only be mapped into `post-initialiser` so it won't affect the assumptions on protection domains. The `post-initialiser` can be executed like a pipeline with one-way capability passing, which meets all the known requirements. The Microkit SDF Syntax design looks like: +``` + + + + + + + + + + + + + + + + + ... + + + ... + +``` + +2. Capability passing via IPC +Each IPC can only pass at most 3 capabilities, so this means two `post-initialiser` components need to be active during the capability passing process. + +## More potential use cases + +Apart from the ACPI/PCIe driver, there might be some other use cases where the new feature can help: +- Clock/Pinmux driver: configure things to a static state at post-initialisation phase, but need to reconsider if we want dynamic clock/pinmux configurations at run time. +- HPET driver: the HPET driver itself might not be a `post-initialiser` but the configuration interface (e.g., device memory and IRQs) are extracted from the ACPI tables. +- Djawula? + +## Unresolved questions + +1. Microkit SDF syntax of post-initialiser component +2. Capabilities passing mechanism between `post-initialiser`. +3. New feature to the capDL loader for handing off all the remaining untypeds. + From df9f8a8f9d0f3f563bd33c6c2f4f11eebec8298a Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Tue, 14 Jul 2026 14:58:19 +1000 Subject: [PATCH 2/3] add points from discussion Signed-off-by: Terry Bai --- src/proposed/998-post-initialiser-rfc.md | 159 ++++++++++++++++------- 1 file changed, 111 insertions(+), 48 deletions(-) diff --git a/src/proposed/998-post-initialiser-rfc.md b/src/proposed/998-post-initialiser-rfc.md index 436d04a..3ea9e93 100644 --- a/src/proposed/998-post-initialiser-rfc.md +++ b/src/proposed/998-post-initialiser-rfc.md @@ -5,59 +5,73 @@ ## Summary -This RFC proposes a solution that adds a post-initialisation domain to allow capabilities shared among -user-defined initialiser components without breaking the existing Microkit assumptions on protection domains. +This RFC proposes a solution that adds a post-initialisation domain to allow +capabilities shared among user-defined initialiser components without breaking +the existing Microkit assumptions on protection domains. ## Motivation On x86, there are two primary requirements for ACPI/PCIe driver: -Unlike the ARM and RISC-V, x86 systems do not know the resource configurations at build time, and have to figure things out by interacting with the ACPI tables possibly located anywhere in memory. In previous internal meeting, we decided to have [an ACPI driver and a PCIe driver](https://github.com/au-ts/sddf/issues/622) to solve this problem, but the following use cases are not supported by the existing capDL initialiser/Microkit: +Unlike the ARM and RISC-V, x86 systems do not know the resource configurations +at build time, and have to figure things out by interacting with the ACPI tables +possibly located anywhere in memory. In previous internal meeting, +we decided to have +[an ACPI driver and a PCIe driver](https://github.com/au-ts/sddf/issues/622) to +solve this problem, but the following use cases are not supported by the existing +capDL initialiser/Microkit: + +- The ACPI driver needs access to most if not all of the remaining untypeds (and +internal information from the capDL initialiser about the watermarks about UTs if +used), because: + * It needs to be able to map in all the ACPI tables (the addresses are not + fixed nor contiguous, so one needs to map-then-parse-then-map in a loop)., etc). + * It also likely needs to be able to create the (seL4 device) frames for PCIe + config space and MMIO windows. + +- The PCIe driver needs the ability to create IO ports, frames, and IRQ +capabilities corresponding to a certain PCI device ID; it also needs to be able +to access the PCIe config space (to itself) and parts of the PCIe MMIO window +(for other device drivers); these are frames that can be determined by the ACPI +driver (from device UT) + +An experimental implementation introduced a `cnode` tag in SDF to allow a custom +CNode to be shared by PDs, but raised the +[concerns from the verification folks](https://github.com/seL4/microkit/pull/539#issuecomment-4871178574). +The shared CNodes bring more flexibility to the user CSpace management but breaks +the Microkit's assumptions for the verification story. And it does not make sense +to introduce a feature but disallow people to use it. + +## Guide-level explanation + +Given that both the ACPI driver and PCIe driver run only once before everything +else, and they do not need most of features of protection domains in the current +Microkit, it makes sense to be moved out from protection domains. + +Zoltan proposed to add an explicit `post-initialiser` feature to run the +one-shot code straight after the capDL initialiser. This can make sure, after +the post-initialisation phase, the capabilities owned by protection domains are +still static (i.e., the staticity assumptions in Microkit proofs), so does not +screw up the verification story. + +The `post-initialisers` are executed in the `phase` order, and can pass +capabilities via the shared CNodes, which are restricted inside the +`post-initialisation` block. Take the ACPI/PCIe work as an example, the Microkit +SDF Syntax design would look like: -- The ACPI driver needs access to most if not all of the remaining untypeds (and internal information from the capDL initialiser about the watermarks about UTs if used), because: - * It needs to be able to map in all the ACPI tables (the addresses are not fixed nor contiguous, so one needs to map-then-parse-then-map in a loop). , etc). - * It also likely needs to be able to create the (seL4 device) frames for PCIe config space and MMIO windows. - -- The PCIe driver needs the ability to create IO ports, frames, and IRQ capabilities corresponding to a certain PCI device ID; -it also needs to be able to access the PCIe config space (to itself) and parts of the PCIe MMIO window (for other device drivers); these are frames that can be determined by the ACPI driver (from device UT) - -The experimental implementation introduced a `cnode` tag in SDF to allow a custom CNode to be shared by PDs, but raised the [concerns from the verification experts](https://github.com/seL4/microkit/pull/539#issuecomment-4871178574). This feature brings more flexibility to the user CSpace management but breaks the Microkit's assumptions for the verification story. And it does not make sense to introduce a feature but disallow people to use it. - -## Proposals - -Given that both the ACPI driver and PCIe driver run only once before everything else, and they do not need most of features of protection domains in the current Microkit, it makes sense to be moved out from protection domains. - -Zoltan proposed to add an explicit `post-initialiser` feature to run the one-shot code straight after the capDL initialiser. This keeps the Microkit state after `post-initialisation` still same as the assumptions, so does not screw up the verification story. - -The solution could be: - -### 1. Wrapper around the capDL initialiser - -Use the capDL initialiser as a library and extend it with `post-initialisation` code. -(I @terryzbai personally don't think this is reasonable for the components that do not need the access to all the untypeds, e.g., the PCIe driver) - -### 2. Post-initialiser component - -New (non-protected) domains are executed after the capDL initialiser in the `phase` order, and the capabilities can be exchanged between the capDL initialisers. - -The options of capability passing mechanisms: - -1. Restricted CNode sharing between only `post-initialiser` - -CNodes can only be mapped into `post-initialiser` so it won't affect the assumptions on protection domains. The `post-initialiser` can be executed like a pipeline with one-way capability passing, which meets all the known requirements. The Microkit SDF Syntax design looks like: ``` - + - + - - + + @@ -69,19 +83,68 @@ CNodes can only be mapped into `post-initialiser` so it won't affect the assumpt ``` -2. Capability passing via IPC -Each IPC can only pass at most 3 capabilities, so this means two `post-initialiser` components need to be active during the capability passing process. +In the above example, the ACPI drvier runs as the first post-initialiser and +receives all the leftover untypeds from the capDL initialiser via the shared +CNode `post_capdl_untypeds`, (which associates with another feature to capDL, +but is not included in this discussion). After mapping and parsing the ACPI +tables, it handoffs all the required capabilities to the PCIe driver via shared +CNode `pcie_resources` for centralised resource allocation and configurations. +Therefore, at the start point of PDs running, the memory, I/O Ports, and IRQs +of PCIe device drivers have been ready. + +This feature is useful when ther are some components running at only the init +phase and some other PDs waiting for them to start. Even if a component has no +requirements on shared CNodes, moving it into the `post-initialisation` block +also helps remove the startup signaling the waitings, as they are good to +go once get scheduled. + +## Reference-level explanation + +The introduced `post-initialiser` feature does not affect any existing features +supported by Microkit, and the users do not need to make changes to their +existing systems. + +The Microkit implementation for this RFC includes: +- `post-initialisation` block: provides a scope that the users can define +`post-initialisers` inside and map the resources to the `post-initialisers`. +- `cnode` tag: allows the users to define custom CNodes inside the +`post-initialisation` block and map them into `post-initialisers`. +- `post-initialiser` component: defines a non-PD component that runs after the +capDL initialiser in `phase` order, and has a subset of features of PD, including +(1) cap_sharing: access to capabilities of other PDs or `post-initialisers`; +and (2) memory mapping: access to MemoryRegions. The programming model of +a `post-initialiser` is slightly different from that of a PD, so it should have +the only program entry `main()` rather than `init()` and `notified()`. + +The Microkit maintainers might need to duplicate work when shared features of PD +and `post-initialiser` are changed or added, as a `post-initialiser` should +have different CSpace as well. + +## Drawbacks + +This RFC restricts the shared CNodes inside the `post-initialisation` block, but +they might be wanted for PDs in the future, e.g., in template PDs. + +## Rationale and alternatives + +### Alternative 1: ACPI tables relocation in a preloader + +Peter's thought: have a preloader runs in a pre-seL4 phase to relocate all the +ACPI tables at specific addresses and then the capDL initialiser can just map +the ACPI tables and pass only device memory untypeds rather than all the untypeds. + +Would it be better to just put the whole ACPI parser into the seL4 boot process? -## More potential use cases +### Alternative 2: Pass capabilities via IPC -Apart from the ACPI/PCIe driver, there might be some other use cases where the new feature can help: -- Clock/Pinmux driver: configure things to a static state at post-initialisation phase, but need to reconsider if we want dynamic clock/pinmux configurations at run time. -- HPET driver: the HPET driver itself might not be a `post-initialiser` but the configuration interface (e.g., device memory and IRQs) are extracted from the ACPI tables. -- Djawula? +Instead of passing capabilities via the shared CNode, one thread can pass at +most 3 capabilities in an IPC, but need a more complicated mechanism if there +are more than 3 capabilities to pass. ## Unresolved questions -1. Microkit SDF syntax of post-initialiser component -2. Capabilities passing mechanism between `post-initialiser`. -3. New feature to the capDL loader for handing off all the remaining untypeds. +1. Microkit SDF syntax of post-initialiser component? +2. Capabilities passing mechanism between `post-initialiser`? +3. Should post-initialiser run in a strict order? +4. Does this design actually not break the Microkit verification story? From 5aea5e4d9d42fdf519e0eac89e1ef9f6599ec8bb Mon Sep 17 00:00:00 2001 From: Terry Bai Date: Tue, 14 Jul 2026 17:22:32 +1000 Subject: [PATCH 3/3] Change suggestion for non-capability-required cases Signed-off-by: Terry Bai --- src/proposed/998-post-initialiser-rfc.md | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/src/proposed/998-post-initialiser-rfc.md b/src/proposed/998-post-initialiser-rfc.md index 3ea9e93..39cd60e 100644 --- a/src/proposed/998-post-initialiser-rfc.md +++ b/src/proposed/998-post-initialiser-rfc.md @@ -93,10 +93,16 @@ Therefore, at the start point of PDs running, the memory, I/O Ports, and IRQs of PCIe device drivers have been ready. This feature is useful when ther are some components running at only the init -phase and some other PDs waiting for them to start. Even if a component has no -requirements on shared CNodes, moving it into the `post-initialisation` block -also helps remove the startup signaling the waitings, as they are good to -go once get scheduled. +phase and some other PDs waiting for them to start. For a componet requiring +shared CNoes, it is a must to be put insde the post-initialisation block. For +a component that does not need shared CNodes, the system designer should take +initialisation time increase into consideration, as all the other PDs have to +wait until all the `post-initialisers` finish. + +For multi-core cases, the parameter `phase` might not be the best solution to +control the execution flow. Adding things into `post-initialisation` block +can hide the the signals for synchronisation but forces all the PDs to wait. +This is left as an unresolved question for discussion. ## Reference-level explanation @@ -141,10 +147,19 @@ Instead of passing capabilities via the shared CNode, one thread can pass at most 3 capabilities in an IPC, but need a more complicated mechanism if there are more than 3 capabilities to pass. +### Alternative 3: Make the capDL initialiser to do all of this + +Integrating the APCI/PCIe-related work into the capDL initialiser, including +the ACPI AML interpreter and PCIe resource configurations, so PCIe devices +would be ready after the Microkit starts scheduling PDs. + +This might not be the best solution but worth discussing on it. + ## Unresolved questions 1. Microkit SDF syntax of post-initialiser component? 2. Capabilities passing mechanism between `post-initialiser`? 3. Should post-initialiser run in a strict order? 4. Does this design actually not break the Microkit verification story? +5. How post-initialisers should be scheduled on multi-core systems?