Hello Ben, On 2024-10-29 03:08, Ben McCart wrote:

I have been working through the tutorials and doing some experimenting and ran into behavior that very much surprised me. I can seL4_X86_PageTable_Map & seL4_X86_Page_Map to virtual addresses starting at the 96 MB address (0x06000000) with no errors.

This implies that there is already a PD mapped, otherwise you would get a seL4_FailedLookup error when doing this.

  However, as soon as I try to seL4_X86_PageDirectory_Map that same virtual address I get the error seL4_DeleteFirst.

You either get an error here, or earlier, depending on the state of the page table.

I didn't think the kernel mapped anything for the root address above 64 MB virtual address range for the root address in these tutorials.  If it did I would have expected an error for seL4_X86_PageTable_Map & seL4_X86_Page_Map.

What is going on?  What am I missing?  How can I avoid expecting to map a virtual address in a range already mapped by the kernel for the root process on a given architecture?

See chapter 7 of the seL4 manual. On x64, the address bits covered are: PML4 39—47 PDPT 30—38 PageDirectory 21—29 PageTable 12—20 By default the rootserver has everything mapped starting from a low address, so there is always a PD present for the first 512 MB. If you want to fully manage your own PD, you need to start at address 0x20000000. Greetings, Indan