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.)

Paper is here: https://arxiv.org/abs/1609.08372

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).

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.

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

Thanks,

Jeff

[1] https://ts.data61.csiro.au/publications/nictaabstracts/Peters_DEH_15.abstract.pml

[2] https://ts.data61.csiro.au/publications/nictaabstracts/vonTessin:phd.abstract.pml