Hi Jeff, 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 Multicore pull requests are being generated internally, things should become visible soon Gernot

On Fri, Sep 30, 2016 at 3:01 PM, 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.abstrac... [2] https://ts.data61.csiro.au/publications/nictaabstracts/vonTessin:phd.abstrac...

On Tue, Oct 4, 2016 at 1:43 PM, wrote:

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

Right, so as core count and cache grows, and coupling between a single CPU's cores becomes looser, it'll be worth having more than one partition per socket. Is the closest thing to loosely coupled cores at mobile (or at least sub-server) scale right now big.LITTLE? Interesting that Apple's A10 Fusion "fixes" big.LITTLE by sharing its L2 between both pairs of cores. Thanks, Jeff