On Mon, Apr 13, 2020, 2:02 AM Heiser, Gernot (Data61, Kensington NSW) < gernot.hei...@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 > _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
