First, a disclaimer: My understanding of the new cap sharing system is recent and likely incomplete, so if anything I write here is wrong, please correct it.
The recent <cspace> addition to the SDF is going to do a fair amount to clean up the microkit changes we make that are required to support our GDB RSP PD. However, by far the most complex and fragile thing we do is mapping the child vspaces into the gdb PD. I don't know if this is something that hasn't been considered, already being considered but isn't quite there yet, or considered and rejected, but I would propose extending with a fourth capability type that installs existing Frame capabilities for a VA range of a target PD's VSpace into the granted PD's own CSpace, e.g.,
<cspace>
<cap_frame_range base_slot="10" pd="child" vaddr="0x200000" size="0x200000" />
</cspace>
- base_slot: first CSpace slot of a contiguous run (one slot per frame in range).
- pd: source PD name (as with the existing three types).
- vaddr/size: VA range in the source PD's VSpace to grant frame caps for, frame-aligned.
The microkit capDL builder already has the authoritative mapping of VA ranges to Frame objects for every PD, so it is a book-keeping issue, not requiring any changes to the kernel. The granted PD then uses its own VSpace cap and ordinary seL4_ARM_Page_Map/seL4_X86_Page_Map to map each copied frame cap into a VA of its own choosing.
As far as I can tell at the moment, such an addition would allow us to abandon all our changes to microkit, as well as eliminating a good deal of our own supporting code.
First, a disclaimer: My understanding of the new cap sharing system is recent and likely incomplete, so if anything I write here is wrong, please correct it.
The recent
<cspace>addition to the SDF is going to do a fair amount to clean up the microkit changes we make that are required to support our GDB RSP PD. However, by far the most complex and fragile thing we do is mapping the child vspaces into the gdb PD. I don't know if this is something that hasn't been considered, already being considered but isn't quite there yet, or considered and rejected, but I would propose extending with a fourth capability type that installs existing Frame capabilities for a VA range of a target PD's VSpace into the granted PD's own CSpace, e.g.,The microkit capDL builder already has the authoritative mapping of VA ranges to Frame objects for every PD, so it is a book-keeping issue, not requiring any changes to the kernel. The granted PD then uses its own VSpace cap and ordinary seL4_ARM_Page_Map/seL4_X86_Page_Map to map each copied frame cap into a VA of its own choosing.
As far as I can tell at the moment, such an addition would allow us to abandon all our changes to microkit, as well as eliminating a good deal of our own supporting code.