Skip to content

Draft: Memory Cap Sharing #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
cazb2 wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

Draft: Memory Cap Sharing #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b1eda39
CapMap: Remove the root cnode upper bound
cazb2 Jul 23, 2026
c53eaaa
MapPerms: Consistency between map and iomap
cazb2 Jul 23, 2026
32dc2f9
WIP: Draft Memory Cap Impl
cazb2 Jul 23, 2026
0f440e4
WIP: Support PageTable
cazb2 Jul 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 2 additions & 1 deletion docs/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -959,7 +959,8 @@ Stop the PD from switching to guest execution mode when a Microkit entrypoint re
Converts the slot identifier of the `<cspace>`'s capability element into an
`seL4_CPtr` value to be used in `libsel4` calls by the PD.

If the slot exceeds the valid range of inputs (`0 <= slot < MICROKIT_MAX_USER_CAPS`), it returns the value `seL4_CapNull`.
If the slot is not in the valid range of inputs (`0 < slot < (1 << microkit_max_user_caps_bits)`), it returns the value `seL4_CapNull`.
The value of `microkit_root_cnode_size_bits` is determined based on the largest slot specified in the `<cspace>`.

# System Description File {#sysdesc}

Expand Down
3 changes: 3 additions & 0 deletions example/cap_sharing/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,12 @@ $(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)
ifeq ($(ARCH),x86_64)
qemu: $(KERNEL_32B) $(IMAGE_FILE)
qemu-system-x86_64 \
-machine q35 \
-cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \
-m "1G" \
-display none \
-device intel-iommu,intremap=off,aw-bits=39 \
-device edu,dma_mask=0xffffffffffffffff,bus=pcie.0,addr=0x04.0 \
-serial mon:stdio \
-kernel $(KERNEL_32B) \
-initrd $(IMAGE_FILE)
Expand Down
186 changes: 182 additions & 4 deletions example/cap_sharing/cap_sharing.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,38 @@
#define CH_SECONDARY ((microkit_channel)0)

// As per cap_sharing.system
#define CAP_SECONDARY_SC (microkit_cspace_root_slot_to_cptr(1))
#define CAP_SECONDARY_TCB (microkit_cspace_root_slot_to_cptr(2))
#define CAP_MY_SC (microkit_cspace_root_slot_to_cptr(3))
#define CAP_MY_TCB (microkit_cspace_root_slot_to_cptr(4))
#define CAP_SECONDARY_SC (microkit_cspace_root_slot_to_cptr(1))
#define CAP_SECONDARY_TCB (microkit_cspace_root_slot_to_cptr(2))
#define CAP_MY_SC (microkit_cspace_root_slot_to_cptr(3))
#define CAP_MY_TCB (microkit_cspace_root_slot_to_cptr(4))
#define CAP_MY_VSPACE (microkit_cspace_root_slot_to_cptr(5))
#define CAP_MR (microkit_cspace_root_slot_to_cptr(6))
#define CAP_IOSPACE (microkit_cspace_root_slot_to_cptr(7))
#define CAP_SECONDARY_STACK (microkit_cspace_root_slot_to_cptr(9))
#define CAP_SECONDARY_IPCBUF (microkit_cspace_root_slot_to_cptr(10))
#define CAP_SECONDARY_ELF (microkit_cspace_root_slot_to_cptr(11))

#define SLOT_SECONDARY_STACK 9
#define SLOT_SECONDARY_IPCBUF 10
#define SLOT_SECONDARY_ELF 11

#define MR_SIZE 0xa000
#define MR_PAGE_SIZE 0x1000
#define STACK_SIZE 0x2000

#define DMA_BUFFER_VADDR 0x10001000
#define IOVA 0x100000
#define RUNTIME_IOVA (IOVA + MR_SIZE)

#if defined(CONFIG_ARCH_X86_64)
#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_X86_Default_VMAttributes
#elif defined(CONFIG_ARCH_AARCH64)
#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_ARM_Default_VMAttributes
#elif defined(CONFIG_ARCH_RISCV)
#define MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES seL4_RISCV_Default_VMAttributes
#else
#error "Unsupported architecture"
#endif

static void halt(void)
{
Expand All @@ -25,12 +53,162 @@ static void halt(void)
while (1) { }
}

static void put_hex64(seL4_Word value)
{
static const char hex[] = "0123456789abcdef";

microkit_dbg_puts("0x");
for (int i = 15; i >= 0; i--) {
microkit_dbg_putc(hex[(value >> (i * 4)) & 0xf]);
}
}

static void check_cap(const char *name, seL4_CPtr cap)
{
if (cap == seL4_CapNull) {
microkit_dbg_puts("|primary | missing cap: ");
microkit_dbg_puts(name);
microkit_dbg_puts("\n");
halt();
}
}

static void print_frame_info(const char *name, seL4_CPtr cap, seL4_Word vaddr)
{
seL4_Word paddr;
seL4_Error err = microkit_page_get_address(cap, &paddr);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error retrieving physical address for ");
microkit_dbg_puts(name);
microkit_dbg_puts("\n");
halt();
}

microkit_dbg_puts("|primary | ");
microkit_dbg_puts(name);
microkit_dbg_puts(" frame vaddr ");
put_hex64(vaddr);
microkit_dbg_puts(" paddr ");
put_hex64(paddr);
microkit_dbg_puts("\n");
}

static void validate_frame_metadata(void)
{
seL4_Word secondary_stack_bottom;
if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_STACK, &secondary_stack_bottom)) {
microkit_dbg_puts("|primary | error retrieving secondary stack metadata\n");
halt();
}
print_frame_info("secondary stack bottom", CAP_SECONDARY_STACK, secondary_stack_bottom);
for (seL4_Word i = 1; i < STACK_SIZE / MICROKIT_BIT(seL4_PageBits); i++) {
print_frame_info("stack frame", CAP_SECONDARY_STACK | i,
secondary_stack_bottom + i * MICROKIT_BIT(seL4_PageBits));
}

seL4_Word secondary_ipcbuf;
if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_IPCBUF, &secondary_ipcbuf)) {
microkit_dbg_puts("|primary | error retrieving secondary IPC buffer metadata\n");
halt();
}
print_frame_info("secondary IPC buffer", CAP_SECONDARY_IPCBUF, secondary_ipcbuf);

seL4_Word secondary_elf_metadata;
if (!microkit_root_slot_to_metadata(SLOT_SECONDARY_ELF, &secondary_elf_metadata)) {
microkit_dbg_puts("|primary | error retrieving secondary ELF metadata\n");
halt();
}
microkit_dbg_puts("|primary | secondary ELF metadata at ");
put_hex64(secondary_elf_metadata);
microkit_dbg_puts("\n");

seL4_Word secondary_elf_frame_count = 0;
for (seL4_Word i = 0;; i++) {
seL4_Word secondary_elf_frame_vaddr;
seL4_Bool found =
microkit_root_slot_to_nested_metadata(SLOT_SECONDARY_ELF, i, &secondary_elf_frame_vaddr);
if (!found) {
break;
}

print_frame_info("secondary ELF", CAP_SECONDARY_ELF | i, secondary_elf_frame_vaddr);
secondary_elf_frame_count++;
}
if (secondary_elf_frame_count == 0) {
microkit_dbg_puts("|primary | error: secondary ELF metadata has no frame entries\n");
halt();
}
}

static void validate_mr_frame_caps(void)
{
for (seL4_Word i = 0; i < MR_SIZE / MR_PAGE_SIZE; i++) {
seL4_CPtr frame = CAP_MR | i;
seL4_Word paddr;
seL4_Error err = microkit_page_get_address(frame, &paddr);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error invoking MR frame capability\n");
halt();
}

microkit_dbg_puts("|primary | dma_buffer frame ");
put_hex64(i);
microkit_dbg_puts(" paddr ");
put_hex64(paddr);
microkit_dbg_puts("\n");

err = microkit_page_map(frame, CAP_MY_VSPACE, DMA_BUFFER_VADDR + i * MR_PAGE_SIZE, seL4_ReadWrite,
MICROKIT_EXAMPLE_DEFAULT_VM_ATTRIBUTES);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error mapping MR frame into VSpace\n");
halt();
}

volatile uint8_t *buf = (volatile uint8_t *)(DMA_BUFFER_VADDR + i * MR_PAGE_SIZE);
*buf = (uint8_t)(i + 1);

err = microkit_page_unmap(frame);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error unmapping MR frame from VSpace\n");
halt();
}

#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_IOMMU)
err = microkit_io_page_map(frame, CAP_IOSPACE, seL4_ReadWrite, RUNTIME_IOVA + i * MR_PAGE_SIZE);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error mapping MR frame into IOSpace\n");
halt();
}

err = microkit_page_unmap(frame);
if (err != seL4_NoError) {
microkit_dbg_puts("|primary | error unmapping MR frame from IOSpace\n");
halt();
}
#endif
}
}

void init(void)
{
seL4_Error err;

microkit_dbg_puts("|primary | hello, world\n");

check_cap("secondary SC", CAP_SECONDARY_SC);
check_cap("secondary TCB", CAP_SECONDARY_TCB);
check_cap("my SC", CAP_MY_SC);
check_cap("my TCB", CAP_MY_TCB);
check_cap("my VSpace", CAP_MY_VSPACE);
check_cap("dma_buffer frames", CAP_MR);
check_cap("QEMU EDU IOSpace", CAP_IOSPACE);
check_cap("secondary stack frames", CAP_SECONDARY_STACK);
check_cap("secondary IPC buffer frame", CAP_SECONDARY_IPCBUF);
check_cap("secondary ELF frames", CAP_SECONDARY_ELF);

validate_frame_metadata();
validate_mr_frame_caps();

/* Notify the secondary. This will print output from secondary as it is
higher priority. */
microkit_dbg_puts("|primary | notifying secondary\n");
Expand Down
19 changes: 18 additions & 1 deletion example/cap_sharing/cap_sharing.system
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,15 @@
SPDX-License-Identifier: BSD-2-Clause
-->
<system>

@cazb2 cazb2 Jul 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sample API.

<memory_region name="dma_buffer" size="0xa000" page_size="0x1000" />

<io_address_space name="QEMU EDU" peripheral_id="0:4.0" domain_id="1">
<io_page_table iovaddr="0x10_a000" size="0xa000" page_size="0x1000" />
</io_address_space>

<protection_domain name="primary" priority="1">
<program_image path="cap_sharing.elf" />
<page_table vaddr="0x1000_1000" size="0xa000" page_size="0x1000" />

<cspace>
<!-- You can have the SC or TCB of another PD -->
Expand All @@ -16,10 +23,20 @@
<!-- You can also have it of yourself -->
<cap_sc slot="3" pd="primary" />
<cap_tcb slot="4" pd="primary" />

<!-- You can access your VSpace, memory-region frames, and an IOSpace. -->
<cap_vspace slot="5" pd="primary" />
<cap_mr slot="6" mr_name="dma_buffer" perms="rw" />
<cap_iospace slot="7" io_address_space="QEMU EDU" />

<!-- You can access frames belonging to another PD. -->
<cap_stack slot="9" pd="secondary" perms="r" />
<cap_ipcbuf slot="10" pd="secondary" perms="r" />
<cap_elf slot="11" pd="secondary" perms="r" />

@ZGwtao ZGwtao Aug 11, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 cazb2 Aug 11, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ZGwtao Aug 11, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 joep Aug 11, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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(n2) 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 dreamliner787-9 Aug 11, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ZGwtao Aug 11, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 cazb2 Aug 12, 2026 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 cazb2 Aug 12, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ZGwtao Aug 12, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 cazb2 Aug 12, 2026 •
edited
Loading

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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>

</cspace>
</protection_domain>

<protection_domain name="secondary" priority="2">
<protection_domain name="secondary" priority="2" stack_size="0x2000">
<program_image path="secondary.elf" />
</protection_domain>

Expand Down
Loading