On Mon, Apr 13, 2020, 2:02 AM Heiser, Gernot (Data61, Kensington NSW) < Gernot.Heiser@data61.csiro.au> wrote:
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
How much overhead would a user-level implementation have over a kernel-level one, and what policy would need to be embedded in the implementation? I was not aware that a scalable SMP system could be implemented at user-level, but I am glad this is the case! That solves my biggest worry about using seL4. I hope to see seL4 become as ubiquitous as Linux is today. Gernot
Thank you, Demi