On 4 Oct 2016, at 12:13 , Jeff Waugh <jdub@bethesignal.org> wrote:

On Fri, Sep 30, 2016 at 3:01 PM, <Gernot.Heiser@data61.csiro.au> wrote:
Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support?

(I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.)


Cool, so your further analysis of the big lock [1] supports the clustered multikernel [2] approach, with the smallest worthwhile partition being the socket (at least on current many-core CPUs, like the 14 core CPU used in testing).

I wouldn’t conclude that the socket is the smallest worthwhile partition. I think we’re lucky that we got the BKL to work across a socket, but you can argue whether that is even too big. I think the smallest worthwhile partition is where you physically share a cache. (Latest-generation Intel boxes have a distributed L3 that is made to look like a shared one.)

That's great news, as smaller systems (arguably most, in this age of IoT, mobile, and virtual guests!) won't have to swallow the complexity of the multikernel.

Correct.

All of this leaves me curious about API. :-)

Good point ;-) And ATM we haven’t got a complete AP. However, it seems clear that the way to handle threat affinity is with scheduling contexts, so the model should really build on the RT kernel. 

Gernot