seL4 design principles

Heiser, Gernot (Data61, Kensington NSW)

11 Mar 2020 11 Mar '20

10:46 a.m.

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

Show replies by date

Demi Obenour

11 Mar 11 Mar

12:46 p.m.

On Tue, Mar 10, 2020, 7:47 PM Heiser, Gernot (Data61, Kensington NSW) < Gernot.Heiser@data61.csiro.au> wrote:

...

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use.

https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/

Gernot

1. Are high-level, hardware-independant libraries that wrap the low-level API planned? 2. Will it be possible to build a conventional (from an application perspective) OS on top of a multikernel, such that the application does not need to be aware that it is running on a multikernel? 3. What are the broken parts of POSIX mentioned? Sincerely, Demi

...

Heiser, Gernot (Data61, Kensington NSW)

6 p.m.

On 11 Mar 2020, at 12:46, Demi Obenour mailto:demiobenour@gmail.com> wrote: 1. Are high-level, hardware-independant libraries that wrap the low-level API planned? Not only planned, they already exist to a degree. For example, CAmkES abstracts architecture, our userlevel libraries (mostly) abstract architecture. 2. Will it be possible to build a conventional (from an application perspective) OS on top of a multikernel, such that the application does not need to be aware that it is running on a multikernel? In principle yes, a clustered multikernel would appear as a NUMA system. But presently we provide no user-level frameworks for this (as practically all of our present use cases are in the embedded space where multicores are closely clustered). 3. What are the broken parts of POSIX mentioned? I/O interfaces that force data copying. For other Posix brokenness, see eg https://dl.acm.org/doi/abs/10.1145/3317550.3321435?casa_token=k6pcqUKP1doAAA...https://dl.acm.org/doi/abs/10.1145/3317550.3321435?casa_token=k6pcqUKP1doAAA... Gernot

Demi M. Obenour

15 Mar 15 Mar

8:27 a.m.

On 2020-03-11 03:00, Heiser, Gernot (Data61, Kensington NSW) wrote:

...

On 11 Mar 2020, at 12:46, Demi Obenour mailto:demiobenour@gmail.com> wrote:

...
1. Are high-level, hardware-independant libraries that wrap the low-level API planned?

Not only planned, they already exist to a degree. For example, CAmkES abstracts architecture, our userlevel libraries (mostly) abstract architecture.

Good to know!

...

...
2. Will it be possible to build a conventional (from an application perspective) OS on top of a multikernel, such that the application does not need to be aware that it is running on a multikernel?

In principle yes, a clustered multikernel would appear as a NUMA system. But presently we provide no user-level frameworks for this (as practically all of our present use cases are in the embedded space where multicores are closely clustered).

What would the overhead of this be? I would prefer to allow direct sharing of user-level memory. Since the kernel does not rely on the integrity of user-level memory, this should be fine if this memory is reserved at system startup, unless I am missing something. How well would seL4 handle systems like the Ampere Altra, which have 80 tightly-coupled cores on a single die? This seems to be the worst-case scenario: a big lock limits scalability, while there is no natural cluster size that I can think of.

...

...
3. What are the broken parts of POSIX mentioned?

I/O interfaces that force data copying.

For other Posix brokenness, see eg https://dl.acm.org/doi/abs/10.1145/3317550.3321435?casa_token=k6pcqUKP1doAAA...

Is Linux’s new io_uring interface a better one? In my experience, avoiding copies across trust boundaries creates a high risk of double-fetch and TOCTOU security vulnerabilities. Some that come to mind are XSA-155, XSA-166, and QSB#23. A filesystem that checksums data must copy the data before creating the checksum, since a malicious applications cannot cause the filesystem to be corrupted. On single-core systems, it might be possible to prevent untrusted code from executing while the checksum is made, but that won’t work on multicore. Sincerely, Demi

Heiser, Gernot (Data61, Kensington NSW)

9:37 a.m.

On 15 Mar 2020, at 08:27, Demi M. Obenour mailto:demiobenour@gmail.com> wrote: In principle yes, a clustered multikernel would appear as a NUMA system. But presently we provide no user-level frameworks for this (as practically all of our present use cases are in the embedded space where multicores are closely clustered). What would the overhead of this be? I would prefer to allow direct sharing of user-level memory. Since the kernel does not rely on the integrity of user-level memory, this should be fine if this memory is reserved at system startup, unless I am missing something. that’s what a multikernel is. Each kernel has some private memory for its own use, everything else is managed at user level. How well would seL4 handle systems like the Ampere Altra, which have 80 tightly-coupled cores on a single die? This seems to be the worst-case scenario: a big lock limits scalability, while there is no natural cluster size that I can think of. The Altra is *not* closely coupled. It has a per-core L2 cache – the cluster size is 1. Gernot

1709

Age (days ago)

1713

Last active (days ago)

List overview

Download

4 comments

3 participants

participants (3)

Demi M. Obenour
Demi Obenour
Heiser, Gernot (Data61, Kensington NSW)