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