seL4
Change the way hierarchy works
Right now the notion of 'parent' and 'child' PDs means that the parent PD has access to the child PD's TCB capability and becomes the fault handler for the child.
This works well enough to enable things such as resetting PDs when they crash, VMMs, and our port of the GDB debugger.
However, there is a limitation with the current model that means that there can only be one parent per child. This makes sense for fault handling, but there could be cases where there is one fault handler for a PD but multiple PDs that need access to the child's TCB.
~~Unfortunately this will result in a breaking change.~~ Thinking about it further, we may want to keep the current model the same and just add the ability to just get TCB access without being a parent. So we may have to make a breaking change to the SDF, we'll see.
You don't have to shoehorn every use case into Microkit via explicit support. All you need is a way to pass specific caps to PDs.
(And if you add the option to create UTs and pass those too, people can build dynamic systems on top of a static Microkit systems. Some way to control the CSpace layout would be nice too.)
No? Camkes doesn't support any of that as far as I know. Perhaps you meant capDL. But Microkit is already re-inventing capDL as it does similar things.
I don't know how you're supposed to create advanced systems based on Microkit if you don't have access to caps and UTs and aren't able to call seL4 syscalls yourself. I'm not asking Microkit to create arbitrary kernel objects and pass those around, I'm asking to expose the caps to existing objects it creates, like you need for your TCB cap access.
The only exception is UTs: It would be good if Microkit can create empty UTs and pass those to PDs. This is much simpler than the shared memory Microkit already implements.
I see Microkit as a minimalistic base system that should be suitable as a building block for creating more complex or dynamic systems. If you don't build it like that, you will get feature creep and bloat over time when more and more functionality is added (like this issue, and you will keep running into limitation when using it for real systems). While if you expose caps now, you have a one-time complexity increase that covers pretty much all possible future cases (except CSpace management).
For CSpace management, minimally there are two things needed:
- Define the cap address range used by Microkit. This so the dynamic code knows which caps are already used.
- A way to reserve empty CNode slots. So the PD can create new objects (and switch to a 2-level CSpace if it wants).
For a 1-level CSpace, the above boils down to telling PDs the first free slot and adding the reserved empty slots to the CNode size calculation (and giving them the cap to their CNode, of course). If Microkit uses a 2-level CSpace, it makes more sense to create an empty sub-CNode of the requested size and only give the cap to that CNode. Either way, very simple to implement.
Once you have the above, Microkit has no limitations at all anymore and can be used for any kind of system. Think about that. (Including sel4test and sel4bench.)
Just to chime in; we really like microkit for its simplicity; ... and we opted to build on bare seL4 because of FOMO regarding dynamic cap handling.
Mat from Neutrality created some proof-of-concept patches a while back. Motivated by the summit talk he published them:
Main thing missing is exposing existing caps, but as far as building dynamic systems on top of Microkit, it's a good starting point to implement what's needed.
Edit: To be clear, Neutrality isn't using Microkit and don't have time and resources to pursue this feature, but are happy to share that hack if it can be useful to someone.
No? Camkes doesn't support any of that as far as I know. Perhaps you meant capDL. But Microkit is already re-inventing capDL as it does similar things.
I'm not a CAmkES expert but if you look at projects such as camkes-vm-examples they'll do things like have some configuration that setups up the initial system but then dynamically create objects for the VMs such as vCPUs etc and map memory on demand.
Once you have the above, Microkit has no limitations at all anymore and can be used for any kind of system. Think about that. (Including sel4test and sel4bench.)
Right now I imagine the majority of our users wouldn't know what to do if we gave them untypeds and access to CNodes, the whole reason they're using the Microkit is because they don't have to learn many of the seL4 concepts.
But you are right, if we do this then Microkit becomes more flexible for other use-cases.
At the moment it's not clear to me what the right direction is, it is my understanding that this kind of functionality clashes with all the verification work we have been doing.
I'll have to discuss this more internally before we make any decision.
Mat from Neutrality created some proof-of-concept patches a while back. Motivated by the summit talk he published them:
Thanks, I wasn't aware of these.
Right now I imagine the majority of our users wouldn't know what to do if we gave them untypeds and access to CNodes, the whole reason they're using the Microkit is because they don't have to learn many of the seL4 concepts.
And that's fine, that's how you lure people into using seL4. Over time they will learn more and understand how seL4 works better, and if they're creating real systems, sooner or later they will run into something that they need and isn't provided directly by Microkit.
Dynamic memory allocation is a good example. No one needs it straight away, but it's very reassuring that you can implement it later if you do need it (or use an existing dynamic memory component).
Same for multithreading. Now Microkit doesn't support it, but with UTs and CNodes people can create their own threads, if they want. Personally I think the strong point of seL4 systems is that you don't need multithreading for good performance, but it's something someone mentioned at the summit.
At the moment it's not clear to me what the right direction is, it is my understanding that this kind of functionality clashes with all the verification work we have been doing.
That's what Gernot said when I talked about this with him, but he couldn't make clear why or how exactly. To me it sounds like a bad excuse, because the whole point of a capability system is that you can safely give away some capabilities without compromising the whole system. Of course, if you proof timing properties, if you expose the schedcontrol cap that proof will go out of the window. But cases like these are easy to detect. Same for separation proofs and you give PDs access to each other's VSpace cap.
I'll have to discuss this more internally before we make any decision.
Mat from Neutrality created some proof-of-concept patches a while back. Motivated by the summit talk he published them:
Thanks, I wasn't aware of these.
They also have x86 support in this branch, in case you're interested.
I’m aware of the x86 patches since there’s a PR. We have our own x86 support that is on top of the move to using a capDL intialiser so we’ll probably end up merging that instead (aiming for later this month/early next month).