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 <Adrian.Danis@nicta.com.au>
Cc: Vasily A. Sartakov <sartakov@ksyslabs.org>; devel@sel4.systems; Kevin Elphinstone <Kevin.Elphinstone@nicta.com.au>
Subject: Re: [seL4] syscalls and tlb

On Mon, Jul 4, 2016 at 10:36 AM, Adrian Danis <adrian.danis@nicta.com.au> wrote:

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