template-pd: introduce 'template' attribute in sdf

[ZGwtao]

This commmit allows users to create a type of PD that has no 'program_image'. Such a mechanism is helpful for loading application payloads into a microkit PD dynamically.

The requirements of using a template PD are:

• template PD should be a child PD of a PD who has no parent
• template PD should not have children, VMs, program images
• template PD should always be active (or their parents need to perform SchedContext unbound operations)

Ref:

• Ch.4., Evolving seL4CP Into a Dynamic OS, Leslie and Heiser, 2022
• https://trustworthy.systems/projects/microkit/2203-report-dynamic.pdf

[ZGwtao]

Something needs discussing is the PD information generated by microkit (e.g., pd_name, ppc bitmaps), which are not provided to the template PDs, as the template PDs have no program image to patch with.

This issue may affect the payloads that use libmicrokit as their runtime, which checks channel ids using the generated channel bitmaps.

A solution is adding a region to the image of the parent PD, which can and should record the microkit-generated PD information of the template PDs. We can provide an object file that contains a region, and put it in libmicrokit.a. PDs that use the region can conditionally link with the object file when building with libmicrokit. The parent PD can pass the microkit-generated info to the template PDs by patching the payload during late-loading.

[lsf37]

I'm sorry, but evolving the Microkit into a dynamic OS is not approved by the TSC and needs a wider RFC discussion. Just because Benno and Gernot wrote a paper once does not mean this should be done.

I don't like this feature creep of undiscussed additions that all diverge from the Microkit's original design.

If this is something that UNSW wants to be doing as a wider roadmap, then this needs an actual plan, a goal, and agreement by the TSC.

[midnightveil]

@ZGwtao For now I will be maintaining a fork of Microkit locally so that we can keep these features up-to-date in a 'main' branch

Please open this PR instead on: https://github.com/au-ts/dynamic-microkit and I will review it .

[Indanz]

The custom_* code is stolen from musl libs which is Copyright © 2005-2020 Rich Felker, et al. and released under the MIT license.

Never copy existing code without proper attribution! This is like the third time this has happened than I'm aware of, please stop doing this.

If you want a proper libc, then add one properly instead of stealing bits and pieces. Newlib is very easy to integrate and comes with the gcc toolchains. And if you want just memcpy/memset, do a simple for loop version please.

[ZGwtao]

thanks for the remindar, sorry, I will double check next time to make sure everything is alright.

[Indanz]

I'm sorry, but evolving the Microkit into a dynamic OS is not approved by the TSC and needs a wider RFC discussion. Just because Benno and Gernot wrote a paper once does not mean this should be done.

I don't like this feature creep of undiscussed additions that all diverge from the Microkit's original design.

If you don't add some kind of dynamic support to Microkit, then that will lead to huge feature creep in the future, because that's what's happening already: Currently everything needs to be explicitly supported by Microkit. And people will keep running into things that are currently not supported, so will keep adding them one by one to cover more and more use cases. This will keep going on forever except if you add basic dynamic infrastructure support. Once you have that, people can implement missing features themselves using that infrastructure without modifying Microkit.

So in my opinion, adding the necessary dynamic infrastructure provides a clear boundary between the static features you want to support and the dynamic ones you don't. If you don't do this, there will be a constant push to add more complex features to Microkit (like pd-templates) to make it usable for real-world systems, while this is a once-off complexity increase that solves all such future issues.

As for the pd-template feature as proposed here: It would work, is very simple to add, but also limited in usability. The implementation could be further simplified (e.g. the restriction that the PD can't be passive seems arbitrary). Long-term, having proper composable systems seems like a better approach, where you can define the interface between multiple Microkit systems. And then dynamically load whole Microkit subsystems, instead of just one PD. But if there is a proper dynamic infrastructure, you can already build that on top of Microkit and there is no need for pd-templates. A static PD with enough cap rights to dynamically load code can do that and setup the caps properly already.

I think it's good to realise that Microkit consists of multiple parts:

• A runtime API.
• A system description.
• Implementation of a tool to create a system image.
• Implementation of a loader.
• Implementation of the monitor, the runtime ABI.

If you want Microkit to be used widespread, you need to add an escape hatch in the form of dynamic infrastructure support. Otherwise people will keep having to re-implement their whole system instead of adding a small dynamic part to an otherwise static system. And there is always something in real systems.

[lsf37]

If you want Microkit to be used widespread, you need to add an escape hatch in the form of dynamic infrastructure support. Otherwise people will keep having to re-implement their whole system instead of adding a small dynamic part to an otherwise static system. And there is always something in real systems.

Maybe, yes (although that is a straight contradiction to how the Microkit RFC was sold to the TSC), but that should be properly planned, agreed on, and designed in a way that doesn't randomly kill formal guarantees, and not in a series of pull requests that make incremental changes without any agreed goal or plan or a plan that is only known to some people at UNSW.

There is a process for that (RFC) and it would actually be very good process for this purpose that forces explicit design discussion and design pressure from different perspectives, not just the systems implementation side. Clearly nobody has thought through the verification angle of template PDs and what the impact is when you use them anyway and if/how that should be communicated to people. And this matters, because there is a whole lot of marketing and claims of verification around this code base and I will not stand for false claims and the kind of bullshit over-claimed verification stories that regularly come out of academia. (Edit: to clarify, I'm not saying we're making false claims now, I'm saying features like this invalidate the basis these verifications are made under and through that those claims. You need to know exactly what you're doing if you want to be able to use them and not just be back to hand waving).

If the TSC and the foundation are supposed to take on long term maintenance and responsibility for the Microkit and its verification story, then these developments need to be made with foundation processes and the agreement of the TSC and not some after the fact "oops we already implemented this".

I have no problem with people doing experiments and prototype implementations etc to figure out designs, and what works and what doesn't work, but as soon as features become public release API they will be very hard to remove in the future if those experiments don't quite work out the people wanted them and the people who implemented them will be long gone.

RFCs are annoying to write and they take skill to write well, but they force documentation and rationale. That can be hard work, but that work needs to be done.

[Indanz]

If you want Microkit to be used widespread, you need to add an escape hatch in the form of dynamic infrastructure support. Otherwise people will keep having to re-implement their whole system instead of adding a small dynamic part to an otherwise static system. And there is always something in real systems.

Maybe, yes (although that is a straight contradiction to how the Microkit RFC was sold to the TSC),

It's what I've heard from people at the summit, and it's also predictable. Especially companies look
at what's available and what is supported, and decide on what to use based on that. If Microkit is
a development dead end because it misses a critical feature, then it won't be used. (And what that
particular feature is depends on the user of course.)

I don't know how Microkit was sold to the TSC, but my impression from the beginning has been that
it's main goal was to lower the barrier to entry of using seL4. It's not good to lower the barrier if there
is a stone wall behind it, but it's fine if there are some steep stairs. My strong opinion has always
been that Microkit should have a way to expose the underlying raw seL4 API so people can create
things on top of Microkit. This includes giving a way for CNode management and access to UT.

https://trustworthy.systems/projects/microkit is all about creating a practical system for real use.
Yes, it focusses on static systems, but that doesn't imply the whole system needs to be static,
only the part Microkit concerns itself with.

but that should be properly planned, agreed on, and designed in a way that doesn't randomly kill formal guarantees, and not in a series of pull requests that make incremental changes without any agreed goal or plan or a plan that is only known to some people at UNSW.

Agreed with all this. But I'm not sure how much was known beforehand by UNSW. To me it's very predictable
that once people really start using Microkit, they run into limitations. Hence the need for an escape hatch,
which I've been gently pushing for for years. But it may be that people at UNSW just started using Microkit
more and are trying to find solutions for their immediate problems, instead of thinking long-term with an over
arching goal. (The immediate trigger being x86 support.)

There is a process for that (RFC) and it would actually be very good process for this purpose that forces explicit design discussion and design pressure from different perspectives, not just the systems implementation side. Clearly nobody has thought through the verification angle of template PDs and what the impact is when you use them anyway and if/how that should be communicated to people.

If that verification work is also happening at UNSW, then it's more an internal communication problem.
But even then it's good to do these kind of discussions via RFC, as it can reach a wider audience.

If the TSC and the foundation are supposed to take on long term maintenance and responsibility for the Microkit and its verification story, then these developments need to be made with foundation processes and the agreement of the TSC and not some after the fact "oops we already implemented this".

Well, currently there is no verification anything about Microkit, at least not on seL4's github, so all of this is a bit invisible at the moment. Verification of Microkit is not mentioned on the Microkit webpages either.

To me Microkit feels more like an UNSW project than a foundation project, just because all the people working on it are from there. And I think that's fine if it's co-owned like this, but it will lead to friction about control over it.

I have no problem with people doing experiments and prototype implementations etc to figure out designs, and what works and what doesn't work, but as soon as features become public release API they will be very hard to remove in the future if those experiments don't quite work out the people wanted them and the people who implemented them will be long gone.

RFCs are annoying to write and they take skill to write well, but they force documentation and rationale. That can be hard work, but that work needs to be done.

Agreed.

[gernotheiser]

Well, currently there is no verification anything about Microkit, at least not on seL4's github, so all of this is a bit invisible at the moment. Verification of Microkit is not mentioned on the Microkit webpages either.

That's actually not true: On https://trustworthy.systems/projects/microkit under “On-going work” is a section "Microkit Verification” (since Sep’23!) which points to a separate page https://trustworthy.systems/projects/microkit/verification. Most of that page hasn’t been changed for two years, but there’s a news item dated 2026-04-30 mentioning completion of the verification of the Pancake implementation. A report providing details is crrently being written…

In general terms: @Indanz is right in that the primary motivation for the microkit was to lower the barrier to entry, and I think it serves that purpose well. It achieves this by hiding the complexities of the seL4 API for the use cases where you don’t need it, which includes a large class of systems, pretty much the embedded space. And that’s not just “static systems*, it’s static architecture – we always envisioned that you should be able to replace component implementations at run time.

Moreover, it was never the intention of locking out functionalities not directly supported by the microkit.

The idea of template PDs is to provide more dynamism within the static architecture. In fact, @Ivan-Velickovic in his Summit’24 talk explicitly mentioned hot-plugging and template PDs, so that idea has been publicly discussed for at least two years.