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.