Conversation
Add support for SGISignal caps on Arm. See also RFC-17: https://sel4.github.io/rfcs/implemented/0170-multikernel-ipi-api.html SGISignalCaps do not reference objects. IRQHandler caps solve this by pointing to an artificial IRQ node, but that IRQ node exists at least in some form in the seL4 implementation. For SGISignalCaps, we chose to use only cap parameters instead, reflecting their intended use in multikernel setups where the target IRQ and core are for a different kernel and have no further representation in the sender kernel apart from the capability. Support includes parsing with the cap syntax sgi_signal (target: <num>, irq: <num>) and printing to .cdl, XML, C, and Isabelle. Despite printing support for C, there is no support for SGISignalCap in the capdl-loader-app or python-capdl-tool yet. This commit also adds an SGISignalCap example to the AArch32 example for testing. 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>
lsf37
force-pushed
the
sgi-capdl-tool
branch
from
ad229cd to
13d2466
Compare
|
I just re-found @kent-mcleod initial implementation at https://github.com/kent-mcleod/capdl/tree/kent/multicore2. The main difference is that Kent's implementation uses an artificial object like we do for IRQ handlers. I don't think that works on the proof side for this one, though. On the upside, maybe I can port over the capdl-loader-app changes there relatively easily, need to check how badly that interacts with a cap-to-no-object. Will open a separate PR for that. |
|
Hm, all those allocation passes become really awkward without an object. Maybe it is easier to only work around this in the proofs instead of everywhere. Let me try this out first, I'm putting this on Draft for the time being. |
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
lsf37
force-pushed
the
sgi-capdl-tool
branch
from
13d2466 to
1459433
Compare
|
Closing this in favour of #77 (most work from here is included there) |
1 participant
Add support for SGISignal caps on Arm. See also RFC-17.
SGISignalCaps do not reference objects which is unusual in capDL. IRQHandler caps solve this by pointing to an artificial IRQ node, but that IRQ node exists at least in some form in the seL4 implementation. For SGISignalCaps, we chose to use only cap parameters instead, reflecting their intended use in multikernel setups where the target IRQ and core are for a different kernel and have no further representation in the sender kernel apart from the capability.
Support includes parsing with the cap syntax
and printing to .cdl, XML, C, and Isabelle.
Despite printing support for C, there is no support for SGISignalCap in the capdl-loader-app or python-capdl-tool yet.
I'm not planning to add support for these for now, but wait for demand first, since new systems are mostly using the Rust capDL loader instead.
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).