Greetings
I’d consider doing a hashed lookup (HPT), either as a cache or with internal chaining, similar to Itanium’s long format. You would remove PD’s and PT from the API and their management complexity…
thank you for your comment.
For alignment with other seL4 variants, just keep the two-level page table and do a software lookup.
To decrease uncertainty (seL4 arch and MIPS arch, both of them are new for me) I have used ARM HAL as reference, and add software-loaded TLB on top of existing memory management design in following way: threadRoot = TCB_PTR_CTE_PTR(ksCurThread, tcbVTable)->cap; <..> pd = PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(threadRoot)); asid = cap_page_directory_cap_get_capPDMappedASID(threadRoot); find_ret = findPDForASID(asid); <..> resolve_ret = resolveVAddr(find_ret.pd, v); <..> add_tlb2(pageBase(v, resolve_ret.frameSize), addrFromPPtr(resolve_ret.frameBase), 0,asid,flags,0); In fact, I have two implementation of TLB support. Another implementation is absolutely independent from ARM source. I am storing array of structures each of which describes memory map for each ASID, and on-fault I just look up into this array. Now I am using both of them and compare values, just to be sure that everything works well. I am going redesign this completely somewhere in the future when current prototype will take off and I will switch from emulator to real hardware.
Using the context register and VLA might be tricky, as “no in-kernel VM faults” is baked into the design, and off the top of my head, I don’t know how much work it would be to un-bake that assumption – might not be too hard (i.e. TLB refill handling might be made somewhat transparent to the kernel).
I have some ideas
Was there an answer for this? How is your MIPS port going, Vasily?
I am using seL4 tutorials as user-space programs. Now I am working with «hello-4». Previous programs are ok, thus, now my port supports creation of threads, context switching, messaging and syscalls and more. There are some issues with PD creation. So, before the end of September, alpha version of seL4/MIPS will be done, I hope. -- Vasily A. Sartakov sartakov@ksyslabs.org