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
