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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
