Hello Jeff,
On 2024-03-08 19:17, Jeff wrote:
*Description:* Starting from the VSpace, map the page table object at
any unpopulated level
for the provided virtual address. If all paging structures and mappings
are present for
this virtual address, return an seL4_DeleteFirst error.
It says it maps the page table object at *any unpopulated *level for
the provided virtual
address. What does that necessarily mean?
You have a three level page table structure in your system, you are
building that tree
in user space with this function.
seL4_RISCV_PageTable_Map() will traverse the page table tree just like
hardware would
for a translation. At the leave node, if it finds a free spot, it will
add the page table
entry. If it find a mapped page or an existing page table entry, it will
return an error.
When you attempt to map the pages, how do you differentiate between the
different levels?
To be precise, you are mapping a page table object, not a page (or so
I'll assume).
User space either needs to remember at which level it's working, or map
page tables on-demand:
Try mapping a page with seL4_RISCV_Page_Map(). If that fails with
seL4_FailedLookup,
a page table node is missing. Then create a page table object and add it
to the tree
with seL4_RISCV_PageTable_Map(). Keep doing this till
seL4_RISCV_Page_Map() stops
returning seL4_FailedLookup().
Is it just based on the vaddr or do you have to point the vspace to one
of the lower level pages?
It's based on just the vaddr and the current topology of the page table.
Or does vspace have to be the root page table?
It always has to be the root page table.
The level normal pages are mapped depends on their size: Normal 4kb
pages are
mapped at the last level, large pages are mapped one level higher,
instead
of a page table entry.
Greetings,
Indan
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
