SGI support for capDL-tool #77
Conversation
|
(The aarch64 test is just a copy of the aarch32 test with minor adjustments to pass the arch check tests) |
github-project-automation
bot
moved this to Todo
in seL4 release 14.0.0 (+ Microkit and others)
lsf37
moved this from Todo
to In progress
in seL4 release 14.0.0 (+ Microkit and others)
corlewis
left a comment
corlewis
left a comment
There was a problem hiding this comment.
Looks good! Thanks for updating the tests and fixing the AsidPool cap check as well.
Indanz
left a comment
Indanz
left a comment
There was a problem hiding this comment.
I don't like the pretending it's an object while it isn't thing, because I don't see how you can get the derivation tree right if you do, but it's done for other caps like IRQs too already.
Other than that and the extra params thing everything looks okay to me (compared to existing code), but I've no experience with any of this code, so can't really judge it for correctness.
| | ARMSMCCap { | ||
| capObj :: ObjID, | ||
| capBadge :: Word } | ||
| | ARMSGISignalCap { capObj :: ObjID } |
There was a problem hiding this comment.
So this is where the model deviates from reality and the properties are not part of the cap, but instead we pretend here they are elsewhere?
I don't understand what the advantage of that is, wouldn't that confuse object creation code when it creates zero sized SGI caps? Those won't be derivates of the UT cap either, so revoking the UT won't automatically clean up the SGI cap, which breaks normally valid assumptions. With this in mind, I really don't like pretending it's an object while it isn't.
There was a problem hiding this comment.
I agree with you, for these caps it'd be conceptually nicer not to do that. Since capDL already deals with the issue for a lot of other cap types, there is infrastructure for fake objects, but no infrastructure for caps with content but without objects (only the control caps have no object in capDL).
For the concrete concerns, they are both fine and dealt with by the existing infrastructure for fake objects: the caps are not created from Untypeds and the loader knows that, so their derivation tree is not confused and revocation on UT is not supposed to clean up the object (the sgi_signal objects should not be under any untyped cover in the spec -- maybe I should add an explicit check for that). You can still specify an original cap and a derived cap (there are only two levels for SGISignalCap) and that works fine in the loader as well, it has an explicit is_original flag that is used for this.
SGISignal caps can be revoked either by revoking on the IRQControl cap (which removes all of them, including IRQHandlers), or individually (that's what the second level is useful for) -- that's not specific to capDL, though, that's just how the IRQ-related caps work in the kernel.
So it does work fine with the right semantics, and in terms of capDL it does actually fit with how the rest is treated. It is awkward in the formalisation, because for other fake objects there is some kind of state in the kernel I can tie them to, but for these ones there is not, the data is only in the cap. So the indirection is going to be annoying in the proof. But it's better dealing with that only once than trying to build and debug a whole lot of infrastructure for creating caps in a different way to what the rest of the tools are used to.
The reserved input keywords are "trigger" and "target", without prefix. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems> Co-authored-by: Indan Zupancic <indan@nul.nu> Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The ASIDPool check on .cdl specs so far required PD caps for all architectures. This is only appropriate for 32 bit architectures. Instead, re-use the check for the VSpace slot in TCBs, which already has a case distinction over the architecture. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
For new autopep8 version Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
|
Rebased and implemented review suggestions. |
github-project-automation
bot
moved this from In progress
to Done
in seL4 release 14.0.0 (+ Microkit and others)
4 participants
Add support for SGISignal caps on Arm. See also RFC-17.
This is based on Kent's branch at https://github.com/kent-mcleod/capdl/tree/kent/multicore3 and does use an artificial object to represent the SGI destination. While this will be annoying in the proofs, support of the loader app and python tool becomes a good deal simpler. Support for printing specs with SGI caps to Isabelle is not yet included and will need an update to the capDL formalisation there first.
This PR also adds an SGISignalCap example to the AArch32 example for testing, and a new AArch64 test with a small fix for the ASIDPool cap check on 64 bit architectures (it looks like we generally do not specify ASID pools explicitly).