On 13 Apr 2020, at 15:19, Demi Obenour mailto:demiobenour@gmail.com> wrote:
If this sounds crazy and complex, then that’s what it is. It just means that the seL4 abstractions, which are meant to be minimal wrappers around hardware, are just not at the right abstraction level for such a manycore system. Which is not surprising: it’s what you get if you pretend that a system where a message takes 1,000 cycle to get from one end to the other is just a simple multicore. Such a manycore is effectively a distributed system and should be treated as one.
If I may ask, why is this? What prevents the SMP kernel from scaling to manycore systems? Is it the complexity of verifying fine-grained locking, the cost of atomic operations, or something else I missed?
You can make an SMP model scale to large number of cores (see Linux). However, this violates several of the microkernel design principles:
- you’d be paying overheads of such an implementation even when you don’t use it - violation of “don’t pay for what you don’t use"
- you’d embedding a lot of policy into the kernel, a gross violation of policy-freedom
- all that for little benefit, as you can achieve the same thing with a user-level implementation – violation of minimality
See https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/
Gernot
