Hi Sathya, If you are asking about paging with RISC-V I think I can help some. You can find more information in the RISC-V manual [1] where - Chapter 4.3 is for sv32 virtual addresses - Chapter 4.4 is for sv39 virtual addresses - Chapter 4.5 is for sv48 virtual addresses The mapping in the vspace.c file is very dependent on architecture. So this won't apply to other architectures like ARM. This is how the RISC-V priv 1.10 spec works though: What you do is make an array with page table entries in it that are offset by how big your page is. The page table entries (pte) are outlined in the manual there and have certain fields that need to be set. The pte_next function is used to take the physical address and make a page table entry If you want to map a 2MiB page instead of making an entry in your array you would put a pointer to the array that contains the addresses for the 2MiB page. A graphical representation might look like: Level 1 Page Table Level 2 Page Tables +----------------+ +---------------------------+ | Leaf PTE | | +-----------------------+ | +----------------+ +------->[0]| | | | | | | | Next Level PTE +----+ | +-----------------------+ | +----------------+ | +-----------------------+ | | Next Level PTE +------------>[1]| | | | | | | +----------------+ | +-----------------------+ | | | | +-----------------------+ | +----------------+ [...]| | | | | | | | | | +-----------------------+ | +----------------+ | +-----------------------+ | [NUM_2MiB_ENTRIES-1]| | | | | | | | +-----------------------+ | +---------------------------+ You can calculate the index that a given address will fall into with the "RISCV_GET_PT_INDEX" macro if you tell it the level and the virtual address (pptr). So you use the desired virtual address to calculate the index in the table and fill that with a page table entry made with the desired physical address. When you loop through the address ranges you increment by how big the pages are. The size of the pages are set by the addressing scheme you are using where sv39 has 1GiB level one pages, 2MiB level two pages, and 4KiB level three pages. You tell the processor that you want to use that table to do your mapping by writing a pointer to it to the SATP register. Like Chris said in another post, we submitted some updates to the mapping algorithm so that it would use the second level pages enabling you to use less than 1GiB pages for memory constrained risc-v hardware. The relevant code is at "kernel/src/arch/riscv/kernel/vspace.c" Hope that helps! [1] https://github.com/riscv/riscv-isa-manual/blob/master/release/riscv-privileg... Jesse Millwood DornerWorks Ltd On 08/09/2018 08:34 AM, Sathya Narayanan N wrote:

Hi Experts,

Could some one help me in understanding the paging in SEL4 ? the MMU architecture ? Is there any material to understand ?

--  regards, Sathya  

 

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Hi Sathya, For details on virtual memory in seL4, please see chapter 7 of the manual: http://sel4.systems/Info/Docs/seL4-manual-latest.pdf Thanks Anna. ________________________________ From: Devel on behalf of Sathya Narayanan N Sent: Thursday, 9 August 2018 10:34 PM To: devel@sel4.systems Subject: [seL4] Paging in SEL4 Hi Experts, Could some one help me in understanding the paging in SEL4 ? the MMU architecture ? Is there any material to understand ? -- regards, Sathya