RFC-25: Add post-initialiser to Microkit #40
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,165 @@ | ||
| # 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. | ||
|
Comment on lines
+8
to
+10
Member
There was a problem hiding this comment. It is not fully clear to me if this is an accurate summary of below. We seem to be declaring multiple PDs? (for post-initialisation). I'm also hazy on what the phases mean exactly. Do they declare a sequential execution oder of a set of PDs? And everything else that is not declared implicitly runs only after? If that is the intent, how does it interact with Microkit's current init phase? (not the capDL initialiser, but the component init code) Should post-initialisation be an official part of that init phase instead? This would avoid the additional concept of post initialisation and "just" give more structure to the initialisation phase in general. Might just be a renaming of concepts. There was a problem hiding this comment. The Microkit PD's I'll let Terry comment on the other aspect here.
Member
There was a problem hiding this comment. So the post-initialisation phase would be running before
Author
There was a problem hiding this comment.
A post-initialiser might need to be executed after its dependencies are ready, e.g., the PCIe driver needs the extracted resource configurations and the corresponding capabilities from the ACPI driver. Therefore, on single core, the sequential execution model is the simplest way to schedule the post-initialisers if there are no cyclic dependencies. The idea was to have the parameter
Yes, the drawback here is that all the PDs would have to wait all the post-initialisers to be done, even if some of PDs are not dependent on any post-initialiser. Ideally, independent post-initialisers can be parallelly executed on different cores, and a normal PD can start once its dependent post-initialisers complete. Also, the ACPI AML has
A post-initialiser should be a different type of (non-?)protected domains which have its own programming model, probably just a I think making post-initialisation a part of PD's initialisation phase does not help constrain the capability transfer among components but significantly increase the trusted computing base of each PD. |
||
|
|
||
| ## 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, | ||
|
Comment on lines
+16
to
+18
Member
There was a problem hiding this comment. This assertion "have to figure things out by interacting with the ACPI tables possibly located anywhere in memory" is not actually true. There are plenty of current x86 systems that do not do this and work fine. For instance, you can boot the system once, figure out what resources there are and then statically specify them. The real motivation (I think, I might be wrong) is that we want a single unchanged piece of software to run on any x86 system. That is a departure from the design principle that one should know what system one is building for, and it has a few consequences beyond this RFC (i.e. are we aiming for more changes in this direction or not). Personally I'm Ok with making that departure, it makes sense for x86 (it is very awkward not to) and maybe it will make sense for AArch64 in the future as well, but this is the thing that really changes and that the @seL4/tsc should be thinking about. There was a problem hiding this comment.
Yes.
Yes, this is strictly speaking, possible, but it is really annoying (minor changes to BIOS versions or placement of cards physically can change things); Peter also says that sometimes the locations can change on every boot.
Yes, one of the designs that I think could have been discussed further in the evaluation is whether or not we could make the capDL initialiser do all of this. It's possible that it would make sense to make capDL spec specify PCI deviceId + vendorID instead of bus:dev.func. ACPI is a harder sell because it requires an entire AML interpreter.
Member
There was a problem hiding this comment. I don't think the capDL initialiser as it is now is a good place to do this, but one design that this suggests is that there could be a separate phase of the capDL initialiser or some kind of plugin system where the capDL initialiser theorem holds for the state just before any custom phases are running. The main drawback to running more code in the capDL initialiser is that this initialiser is the root task with full authority over the entire system. The principle of least privilege would suggest that authority should be dropped to just what is necessary to do this ACPI task. So maybe the CSpace of the initialiser could be swapped out before this phase runs, so that it is then constrained. This would need no change in Microkit and would make that kind of boot phase available to other kinds of systems as well. It's very similar to the post initialisation idea, just in a different framework. It would be a bit fiddly to correctly place this in the capDL init flow. It should probably run before other threads can run, but after the distribution theorem holds. So we'd be missing that one final step (threads start) of the current theorem if we use it, but that's not a complex or failure prone step, so I think that would be fine.
Author
There was a problem hiding this comment. Zoltan proposed another similar idea that the post-initialiser threads are created and executed sequentially by the capDL initialiser, so each post-initialiser would have the minimum set of capabilities to finish its job. One of the difficulties is that we will need a sort of interfaces to dynamically declare required resources for next post-initialiser, e.g., the ACPI driver tells the capDL initialiser what the PCIe driver needs for its configurations. Surely, we can also integrate the ACPI and PCIe drivers together, but I prefer to have a generic solution for the users to define custom boot phases tasks. |
||
| 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. | ||
|
Comment on lines
+24
to
+30
Member
There was a problem hiding this comment. Surely it does not need access to all remaining untypeds? That could be enormous amounts of memory. I can understand that it may need a statically unknown amount of memory, though. This is a separate issue for the capDL initialiser: "give all remaining untypeds" to some CSpace is not a declarative statement about the initial state of the system, it's a procedural interpretation of how the initialiser works. Not sure we need a full separate RFC for this, but it does need discussion on how that should be expressed statically and what it means formally. I.e. what is the correctness property that you want to hold after the initialiser is done with this? Just "this set of CNode slots contains only untyped caps that are distinct from other untyped caps in the system"? Is an initialiser that just gives you 0 or 1 of them correct or incorrect? Does it have to be all that are mentioned in boot info? How do you know how many of these will be needed for the other objects? What if you haven't provided enough slots? Is the initialiser supposed to dynamically create more CNodes? Where do the caps go for those? What if the initialiser just fills as many as it can? Is that correct? What if those are not enough for your system? Most of these are probably not so hard to answer, but they should have an answer.
Author
There was a problem hiding this comment.
The ACPI tables should be located on device-type memory, and the intermediate paging structures of elf image can be reused for table mapping, so ideally no normal untypeds are required.
yes, I have been thinking about this and prefer to have more thoughts from the verification people.
For the ACPI driver specifically, it would be very complex to evaluate. The AML has almost all of what we have in a high-level programming language, such as variables (NameOp/FieldOp), functions (MethodOp), algorithmic and logical operators. This means the data that we extract from the tables can change due to different function invocation (called In this case, returning 0 can only tell that the capabilities are available regarding to extracted resource configurations, but cannot tell if the interpretation is correct or not.
ye, all of these also confused me. This should be solvable if the post-initialisers are created and executed by the capDL initialiser. |
||
|
|
||
| - 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. | ||
|
Comment on lines
+38
to
+43
Member
There was a problem hiding this comment. This should be replaced by text about what the verification problem is so that the RFC is self contained. |
||
|
|
||
| ## 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. | ||
|
Comment on lines
+47
to
+49
Member
There was a problem hiding this comment. This is very specific to the example you are thinking about right now. The RFC should be proposing a general mechanism. One that also solves your current need, of course, but one that makes sense in more than strictly one situation. So this shouldn't be motivated by "this driver does this", but by what is a good design in general. Do we need everything to be sequential in phases in such a generalised initialisation phase or should these two drivers implement the phasing amongst themselves with notifications? I.e. should it be framework or implementation? Are there other situations we can think of where phasing is particularly good/natural or some where it is bad? What if we're doing multicore? Do we want other components to be doing their own initialisation while this is going on or do we want the framework to be able to allow/prevent that or to always prevent that?
Author
There was a problem hiding this comment.
As I mentioned in another comment, a directed dependency model might be more proper when we consider on multi-core cases. The primary issue is that I still cannot come up with other use cases to generalise the solution. A clock/pinmux driver is expected to dynamically adjust the hardware as requested at run time. |
||
|
|
||
| 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. | ||
|
Comment on lines
+51
to
+55
Member
There was a problem hiding this comment. An RFC shouldn't be a story of what happened but a description of a desired design and its rationale. Please rephrase as that. I think the idea is good. Not entirely clear if post-initialisation should be part of initialisation or not. (Maybe not, IIRC communication is not supposed to happen during initialisation, so maybe the component init phase is not the right place)
Author
There was a problem hiding this comment. it refers to the post-initialisation phase of the whole system, i.e. after the capDL initialiser, rather than the initialisation phase of a PD. |
||
|
|
||
| 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: | ||
|
|
||
| ``` | ||
| <system> | ||
| <post_initialisation> | ||
| <cnode name="post_capdl_untypeds" slot_count_bits="9" /> | ||
| <cnode name="pcie_resources" slot_count_bits="8" /> | ||
|
|
||
| <post_initialiser name="acpi_driver" phase="1" /> | ||
| <cap_cnode name="post_capdl_untypeds" slot="2" /> | ||
| <cap_cnode name="pcie_resources" slot="3" /> | ||
| </post_initialiser> | ||
|
Comment on lines
+68
to
+71
Member
There was a problem hiding this comment. Does this define a PD? Or is it just a thread? What VSpace would it get?
Author
There was a problem hiding this comment. It should be a thread but also wants a small subset of features of PDs. It should has its own VSpace, which will be released after the post-initialiser completes. |
||
|
|
||
| <post_initialiser name="pcie_driver" phase="2" /> | ||
| <cap_cnode name="pcie_resources" slot="2" /> | ||
| </post_initialiser> | ||
| </post_initialisation> | ||
|
|
||
| <protection_domain name="ixgbe_driver" priority="100" /> | ||
| ... | ||
| </protection_domain> | ||
|
|
||
| ... | ||
| </system> | ||
| ``` | ||
|
|
||
| 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. | ||
|
Comment on lines
+91
to
+93
Member
There was a problem hiding this comment. When you say "for centralised resource allocation and configurations", what does that mean exactly? Does the PCIe driver consist of multiple components? Does it have to hand out resources to other parts of the system or does it remain a single central component for anything PCIe related?
Author
There was a problem hiding this comment. The PCIe driver aims to allocate memory regions and I/O Ports from the resource window, which is handed off by the ACPI driver. The resource window of each device (including PCIe bus) on hardware is written on the ACPI tables by the firmware. Interrupt routing information of I/O APIC is also formatted in the ACPI tables. |
||
|
|
||
| This feature is useful when ther are some components running at only the init | ||
| 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 | ||
|
Comment on lines
+95
to
+97
Member
There was a problem hiding this comment. Should be rephrased a bit, but I understand that this is saying the |
||
| 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. | ||
|
Comment on lines
+98
to
+100
Member
There was a problem hiding this comment. Is it required that this is linear? E.g. pos-initialiser phase and the rest could run interleaved/concurrent. Not sure if that is a good idea, but I think we should have rationale on why the design is this way and what pro/con aspects we have considered. The RFC text will serve as documentation in the future for why things are the way they are, in particular to document what we have thought about and what not. If a new idea comes along we want to know if it is actually new or if it was considered and rejected (and why). |
||
|
|
||
| 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. | ||
|
Member
There was a problem hiding this comment. I do think this needs to be resolved in this discussion. It doesn't have to be a final unchangeable solution, i.e. with more experience we might go back and change it, but we need to decide on one design now and document why we thought it is the way to go. |
||
|
|
||
| ## 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: | ||
|
Member
There was a problem hiding this comment. This section should define the full syntax and meaning for the new feature, ideally as it will appear in the manual. An "includes" list is not enough. |
||
| - `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. | ||
|
Comment on lines
+125
to
+127
Member
There was a problem hiding this comment. The planned layout of the differences should be specified. |
||
|
|
||
| ## 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. | ||
|
Comment on lines
+131
to
+132
Member
There was a problem hiding this comment. What would be an alternative/tweak to this design that makes a generalisation later easy? I'm not sure what exactly template PDs are, and if they will spark joy, but if you already have something in mind and future change can easily be reduced by more thinking now, then that seems worth doing. (But if template PDs need shared CNodes, then they do break the Microkit design, so maybe it is better if they do not fit). |
||
|
|
||
| ## 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? | ||
|
Member
There was a problem hiding this comment. In terms of principle of least privilege, it is better if such code runs in an already authority-constrained environment. Then at least it can be verified without needing to preserve invariants about the entire rest of the system (e.g. in the loader about what it has done to kernel code, memory, page tables etc). So from that perspective, I think the design proposed here is strictly better. In terms of implementation, doing this before the kernel loads might be the simplest option. But doing everything in privileged mode is always the simplest option, i.e. that doesn't mean we should do it. |
||
|
|
||
| ### Alternative 2: Pass capabilities via IPC | ||
|
|
||
| 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. | ||
|
Comment on lines
+146
to
+148
Member
There was a problem hiding this comment. It should of course only pass 1 capability per call, and do that in a loop. I'm not sure there is any substantive difference to the shared CNode feature, apart that it is easier to break the authority link temporally. I.e. after the cap transfer via grant is done, the grant right can be removed (or even the entire endpoint cap), and the components are from then on separate according to authority confinement. (Edit: I'm not necessarily pushing for this alternative. If shared CNodes are easier or the same, we can just do that, but it's not clear to me that it is in fact easier or better, so we should not just dismiss it) This reminds me: the RFC does currently not describe what happens to the post-initialisation non-PDs after they are finished. Are they inert? How do we show that? Does the monitor explicitly kill everything that should no longer run? Can/should their resources be reclaimed? (probably not in a static system). There was a problem hiding this comment. (Right, |
||
|
|
||
| ### 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. | ||
|
Member
There was a problem hiding this comment. (Discussion ongoing in a separate comment thread). If done right, this may actually be not a bad option either. |
||
|
|
||
| ## 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? | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We do generally want full names for the RFCs. If there is a problem with that, we can discuss.