Draft: Memory Cap Sharing

[cazb2]

Sharing this as one possible design for the memory cap sharing discussions. Emphasising that it is only a sample approach that is almost certainly not the best. However there are so many possible approaches to implementing this functionality it seems like implementing different approaches and comparing each of them is one way to reach a good final design.

This approach allows the sharing of frame capabilities. This can be used to implement designs such as gdb, dynamic dma protection (the ability to make memory temporarily reachable via dma) and have pre allocated page table regions of memory where frames can be mapped at runtime once the physical addresses are known which is useful in x86 contexts (will require access to device untyped).

In terms of what it offers: support for accessing frames of any memory region, accessing iospace caps required for mapping and unmapping frames in an IO address space, accessing frames of any PDs stack along with the base virtual address (the size can be discovered from the sdf), accessing the frame for the ipc buffer of any PD, accessing the frames of a PDs elf along with the virtual address each frame is mapped at.

It also supports a new page table / io page table concept which will allocate the page tables but not the frames for a given virtual address region. This cleanly supports the actual mapping and unmapping of frames in an address space since currently the only way to ensure that the upper levels of page table are present is either through mapping a memory region and then overmapping it, or relying on the fact that by mapping in one 4KiB we know there will be room for 511 4KiB pages consecutive to it.

[cazb2]

Sample API.

[ZGwtao]

Being able to access frames of other PDs is cool, but I don't see why a PD needs to read/modify the stack/ipcbuffer of others? Regarding cap_elf, the semantic of "executable file" seem to mismatch with the semantic with other cap_xxs, which are mostly hardware oriented or kernel abstractions (e.g., mr. iospace, sc, tcb)

Maybe cap_mr has covered what we need?

[cazb2]

Yeah the sdf name and grouping with the other caps is clunky? I wasn’t sure where else to put them.

Reading the stack and IPC buffer was to support gdb.

[ZGwtao]

That makes sense, though I can't think of any better solution at sdf level.

How about this: Add a pair of attributes like debugger vs debuggee to a pair of PDs. The debugger must be the parent of the debuggee and it's a one-on-one relationship. The debugger automatically receives mappings for the stack/ipcbuffer of the debuggee, and locations of the RO stack/ipcbuffer on the debugger side are patched as setvar values (e.g., microkit_debuggee_stack, microkit_debuggee_ipcbuffer)?

[joep]

Yes, we have been following this and adding arbitrary limits when you can already dip your fingers into a PD and alter pretty much anything you want seems just that...arbitrary.

I know this is a WIP but I will mention something we noticed while reviewing the design to see if it supports everything we need for gdb (and it seems to on paper):

In the example the PD iterates over the frames by calling microkit_root_slot_to_nested_metadata for each frame n. That function then validates the requested frame by iterating from 0 up to n checking each frame's presence bit along the way. This is an O(n²) operation across potentially hundreds of pages for each user of the API.

The tool already knows the frame count, so why not embed it in the metadata? Then expose it to the PD, use it internally in the library, and both layers of probing go away.

[dreamliner787-9]

Add a pair of attributes like debugger vs debuggee to a pair of PDs.

I don't think this is a good idea. The Microkit should only expose generic mechanisms for users to do what they want. Rather than putting every possible use case in.

[ZGwtao]

Add a pair of attributes like debugger vs debuggee to a pair of PDs.

I don't think this is a good idea. The Microkit should only expose generic mechanisms for users to do what they want. Rather than putting every possible use case in.

Right.

How about allowing PDs to bind their ipc buffer or stack to a memory region? The debugger can use the cap_mr mechanism to access the frame cap of the ipc buffer and the stack of the debuggee. In such an example, the sdf would look like this:

<system>
    <memory_region name="ipc_buffer_frame" size="0x1000" />
    <memory_region name="stack_frame" size="0x2000" />

    <protection_domain name="debugger" priority="25">
        <program_image path="debugger.elf" />
        <cspace>
            <cap_mr slot="5" mr_name="ipc_buffer_frame" perms="r" />
            <cap_mr slot="6" mr_name="stack_frame" perms="r" />
        </cspace>
    </protection_domain>

    <protection_domain name="debuggee" priority="2" stack_size="0x2000">
        <program_image path="debuggee.elf" />
        <ipc_buffer mr="ipc_buffer_frame" />
        <stack_frame mr="stack_frame" />
    </protection_domain>
</system>

The elements ipc_buffer and stack_frame are similar to what a program image means for a PD. (Although this is a bit similar to our previous approach which assigns ipc buffer to the __sel4_ipc_buffer_obj symbol defined in linker script of libmicrokit)

[ZGwtao]

I guess this is useful, in some ways, especially when unlimited number of child PDs becomes a reality seL4#526, although in that case we might want to expand the microkit cnode instead of the root cnode.