Greetings. I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions. I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? thank you. -- Vasily A. Sartakov sartakov@ksyslabs.org
Hi Vasily, I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The reason all syscalls are directed through __sysinfo is that the 'service' that implements our syscalls is frequently ourselves (for example libsel4muslcsys). However, this service is C code that would also like to use parts of a C library. If muslc called directly into mulscsys then there would be a circular build dependency, having a late binding through __sysinfo resolves this. The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? Our current architectures (arm and x86) have hardware loaded TLBs and so this is a non issue for them. I am not sure how software loaded TLBs would best be supported on seL4. Unfortunately the best person to answer this, Dr Kevin Elphinstone, is away at the moment. Adrian ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
On Mon, Jul 4, 2016 at 10:36 AM, Adrian Danis
Our current architectures (arm and x86) have hardware loaded TLBs and so this is a non issue for them. I am not sure how software loaded TLBs would best be supported on seL4. Unfortunately the best person to answer this, Dr Kevin Elphinstone, is away at the moment.
Hi all, Was there an answer for this? How is your MIPS port going, Vasily? Thanks, Jeff
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…
For alignment with other seL4 variants, just keep the two-level page table and do a software lookup.
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).
- Kevin
From: Jeff Waugh [mailto:jdub@bethesignal.org]
Sent: Tuesday, 23 August 2016 9:45 AM
To: Adrian.Danis (NICTA) - Contact
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
On Wed, Aug 24, 2016 at 9:15 PM, Vasily A. Sartakov
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.
Cool, that's exciting work! (And thanks for your answers, Kevin.) Thanks, Jeff
participants (4)
-
Adrian Danis -
Jeff Waugh -
Kevin.Elphinstone＠data61.csiro.au -
Vasily A. Sartakov