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

Reply via email to