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)

[cazb2]

I think that’s clean ^, one minor consideration is the stack size vs memory region size. Maybe it is cleanest to leave it up to the user to specify the stack size of a pd and use that for any stack memory regions?

Would you want to bind the memory region to a protection domain ipcbuff/stack/elf as attributes on the memory region though, otherwise you allow and have to handle multiple pds trying to bind to it?

[cazb2]

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_2) 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.

Yeah I agree, thanks for the feedback too. This probably should be provided to a PD as a memory region. It seems like that is becoming the mechanism to provide tool metadata to PDs e.g. the x86 prefills & the suggestion from @ZGwtao.

If a PD has access to this data directly then having a sentinel / NULL entry avoids having to provide the size all together and we could get rid of the bit packing and keep it simply the virtual address of each frame for the other pd. Which is nice since that is all a PD actually needs so shouldn't need to change later in future... in theory. This would enforce a O(n) loop to begin with but the user could establish a constant time mapping etc during init.

[ZGwtao]

I think that’s clean ^, one minor consideration is the stack size vs memory region size. Maybe it is cleanest to leave it up to the user to specify the stack size of a pd and use that for any stack memory regions?

I am not sure about the design, do you mean something like this?

<system>
    <memory_region name="stack_frame" size="0x2000" />
    <protection_domain name="debuggee" priority="2" stack_mr="stack_frame" >
        <program_image path="debuggee.elf" />
    </protection_domain>
</system>

Would you want to bind the memory region to a protection domain ipcbuff/stack/elf as attributes on the memory region though, otherwise you allow and have to handle multiple pds trying to bind to it?

I would prefer to treat it like the above example, as stack seems to contain a semantic which describes a piece of virtual memory of a PD. A memory region (to me) is the abstraction of a chunk of physical memory, so...

Regarding multi-pds binding conflict, probably a simple way to do is letting the sdf parser enforce an implicit one-on-one relationship. Looking forward to others' ideas.

[cazb2]

Yeah I agree with keeping memory regions a physical memory abstraction :)

I was thinking very roughly like:

<memory_region name="debugee_stack_frame" size="0x2000" pd_stack="debugee”/>

<memory_region name="debugee_elf" pd_elf="debugee”/>

<memory_region name="debugee_ipc_buf" pd_ipc_buf="debugee”/>

<protection_domain name="debuggee" priority="2"" >
    <program_image path="debuggee.elf" />
</protection_domain>

<protection_domain name="debugger" priority="2"" >
<program_image path="debugger.elf" />
(put the MAP ELEMENTS HERE)
</protection_domain>

[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.

[cazb2]

What's the benefit of creating child cnodes or re-using the microkit cnode for the cap sharing features though?

[ZGwtao]

I guess the reason we want to expand or re-using the microkit cnode is not for cap sharing, but just for holding more caps for the child (e.g., more child means more caps for child TCB and SC).

Being able to adjust the size of CSpace is useful in that case, as the child number varies within a huge range (u64?).

[cazb2]

I see, maybe with cap sharing the issue with child caps can just be solved intrinsically to the ability to specify a slot to put a cap to any pds kernel objects?

[ZGwtao]

I see, maybe with cap sharing the issue with child caps can just be solved intrinsically to the ability to specify a slot to put a cap to any pds kernel objects?

oh I think you are correct, the caps which now live in microkit cnode can use cap sharing and be put into a cap at the root cnode instead, whose size adjusts automatically.

[joep]

This still grows the SDF schema to solve what's really a "give PD A a cap to PD B's frames" problem, not a memory-layout problem.

The tool already computes every PD's stack/ipcbuf/ELF frame addresses at generation time. Rather than implementing new <memory_region> or <protection_domain> binding attributes, the existing generic cap_mr element could just be extended to reference another PD's stack/ipcbuf/ELF region by kind — e.g. something like <cap_mr slot="N" pd="debuggee" kind="stack" perms="r"/>. That would avoid needing any new <memory_region> or <protection_domain> attributes at all — the tool resolves pd+kind to the frames it already tracks internally and shares those caps, same as it does for named memory regions now.

That keeps the only new SDF surface to "let a cap-sharing element point at another PD's frames". In our case, this is all we needed to fully implement GDB and a PD profiler and complexity beyond this actually complicates our current tooling. In our opinion, everything else belongs in the tooling rather than in the schema or in each PD's runtime code. To me, this feels much closer to Microkit's minimalist philosophy.

[cazb2]

That would work but currently the IPC buffer, stack and elf frames are not classified as a memory region, so using cap_mr seems like a hack.

Alternatively if the stack, IPC buffer and elf can be bound to a memory region you have the ability to then map them into other pds using the existing map operations without being given the frames, or if you need the frames the new cap_mr operation. Isn’t that cleaner than having to deal with non consistent cap_mrs?

Then the additional cases to handle would be how a PD can learn about the virtual address another pd has its stack, IPC buffer and elf frames mapped?

[midnightveil]

I don't think we have a cap_mr element at this time. (I also don't see how it would work, do you mean "cap_frame" or something? An MR can have multiple frMes)

Anyhow, something like this - especially as we don't know a good solution to it and there are lots of valid solutions - should definitely go through a proper RFC (whether or not that means seL4 foundation RFC, IDK, but probably), but it definitely needs a written RFC document.

I've mentioned before that I want to figure out some kind of generic "metadata" passing mechanism: because we have been slowly adding a variety of ad-hoc ways (mostly via a sprinkling of setvars) or proposing various solutions, such as the GDB vspace mapping one (see PR on Microkit). @Indanz has at various points proposed instead giving each cap a unique name according to some scheme and then just being able to insert those caps instead of adding more code here for different cases (I'm not convinced that this is easily possible without being very ugly; however).

(I'm also inclined to go back on what we implemented earlier with the <cspace> element which @lsf37 so rightly pointed out should have gone through an RFC in practice; I don't know if it will actually be useful enough to not have to change in future. Maybe it will be fine.)

[cazb2]

I'm all for an RFC, this was done as an internal experiment and to get feedback.
It would also be good to include in the RFC if the current approach for passing metadata on x86 via the prefilled memory region is the way to go?

[joep]

That would work but currently the IPC buffer, stack and elf frames are not classified as a memory region, so using cap_mr seems like a hack.

Alternatively if the stack, IPC buffer and elf can be bound to a memory region you have the ability to then map them into other pds using the existing map operations without being given the frames, or if you need the frames the new cap_mr operation. Isn’t that cleaner than having to deal with non consistent cap_mrs?

Then the additional cases to handle would be how a PD can learn about the virtual address another pd has its stack, IPC buffer and elf frames mapped?

Microkit is a completely static system. Read the SDF and you can learn every detail a GDB RSP needs to know, either from the SDF itself or from the files the SDF refers to. No runtime discovery is needed for anything. Read the SDF, read the ELF files it refers to, and embed all that information into the GDB RSP and a GDB script so they cooperate to give you a coherent debugging session. The tooling we have for this is completely automated and it just reads the SDF and produces everything necessary for a debugging session. It works exactly the same across all potential hardware targets and the only thing that changes is specification of the actual communication channel (i.e., what hardware device are you using to communicate between the RSP and the GDB host session?)

The only ability Microkit didn't provide for to allow our entire debugging flow to work out of the box was the ability to peek and poke at the child PDs virtual addresses. We honestly don't care what the mechanism is that allows us to do that. When we made our own modification to Microkit to do it, we just did it in the easiest way we could. Our hope is that we can abandon those changes for some officially supported way to do it.

[midnightveil]

I am curious about your changes. Obviously you say they are hacky but "simplest" is also a nice property. Any chance of sharing those?