seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Generate channel identifiers from the system description #69

Open podhrmic opened 9 months ago

podhrmic commented 9 months ago

Currently we need to manually declare the relevant channel numbers for each PD, for example here. The microkit should generate an appropriate header with the channel numbers from the system manifest. Each PD can then include the generated file. Generating .h files should be trivial, Rust modules might need some more thought.

If there are concerns about sharing these channel IDs, perhaps a header file for each PD can be generated.

Ivan-Velickovic commented 9 months ago

My immediate thought on this is that, while useful and desirable in some cases, it is not the responsibility of Microkit itself. This kind of abstraction/auto-generation belongs in a separate tool that the user interacts with via their build system. Given this tool could vary a lot depending on the system your building and the system designer's priorities/goals, it would be very difficult for Microkit to provide something that is actually usable by everyone and does not restrict people.

For these reasons I do not think that it is appropriate for Microkit to do this. I have started making a tool for doing this kind of auto-generation, but again that it is a low-priority for now.

gernotheiser commented 9 months ago

I can see your point (particularly given that there needs to be a version of that tool for each language, and its use will depend on the build system), but if its completely separate, how do we ensure consistency in the evolution of the Microkit as well as the tool?

elmankku commented 9 months ago

I agree that this is not necessarily responsibility of the microkit, although I don't see having such tool part of the SDK as a problem. As long as it is a separate tool (AND build system and compiler agnostic). Any PD could then just run this tool as part of their configuration phase. And Rust bindings, for example, can be generated from .h with bindgen.

But we should remember that the tool we talking about here is about preprocessing before the PDs are built, and the microkit tool itself is about creating the system (after PDs are built). So we want to be careful for not mixing these two.

Even if such tool wouldn't be part of microkit, I think it would be helpful if parsing of system manifest to an intermediate representation would be in a library. This would help creating any language specific tooling.

podhrmic commented 9 months ago

I agree that having a separate utility tool deal with this is the best. IMHO if we had a JSON schema as I mentioned in #70 writing a little Rust tool for this would be very easy, but any schema would work as well (and help you manage changes, should the manifest format change over time).

Ivan-Velickovic commented 9 months ago

My current plan is to continue developing the tooling outside of Microkit, once it has received some internal use at TS (and possibly been made available to the community for feedback) we can evaluate whether it should be part of the Microkit SDK itself.

Much easier to bring things into the SDK rather than take out later.