Let me attempt a slightly different take on this. The primary objective of microkernel abstractions is to be “minimal” (and I’m not trying to define what I mean with this). This means that the kernel API is generally a very thin wrapper around the hardware, just enough to allow secure management/multiplexing by user-level policy implementations. This necessarily provides a degree of hardware abstraction, and as far as we can abstract the hardware in an architecture-independent way without putting policy into the kernel or hurting performance we do this, but the kernel isn’t meant to be a complete hardware abstraction. Page tables are a good example of this. Between ARM and x86, which have similar architecture-defined page tables, the abstraction of the HW is pretty good. But where the underlying architecture differs significantly, this will be reflected in the API. Specifically, x64 will be different, and ARM-64 will be different. If we ever ported to a PPC with inverted page tables, this would be reflected in the API. It’s an open question what we would do with an architecture with a software-loaded TLB (such as MIPS64). In the past we implemented a software-TLB (i.e. a PTE cache), but we probably wouldn’t do that with seL4. Gernot

On 1 Sep 2015, at 10:32 , Gerwin Klein wrote:

...

On 1 Sep 2015, at 10:06 am, Raymond Jennings wrote:

Hey, quick question.

This is just hypothetical, but would making management of pagetables/pagedirectories a low level literal operation hurt seL4's portability to other architectures that might not even use page tables?

I could be mistaken but I think there's some archs out there that only have software TLBs (openrisc IIRC among them)

Please forgive me if I'm mistaken but my recent question about memory abstraction reminded me about this.

Yes, there’s no attempt to provide abstraction for this, different architectures have different memory management mechanisms and seL4 will provide different APIs for them — they are in the arch-dependent part of the kernel. The currently supported architectures all happen to have page table structures, but we had an initial MIPS-like seL4 version with a software-loaded TCB that exposed a different API (reusing the CNode concept for virtual memory), and PPC would probably be different again.

The rationale is that abstracting memory management too early can severely hurt performance. Such abstractions should be provided at higher layers of the system software.

It doesn’t make porting seL4 harder (it would actually be harder to expose the same interface for all possibly MMU designs), but it does mean that the systems software on the next level up needs to know which architecture it is running on, which it should anyway if it wants to make use of the hardware efficiently.

Cheers, Gerwin

________________________________

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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel