Re: [seL4] Cross-core thread migration
Hi Demi,
If I have a manycore machine, what is the best way to migrate a thread from one core to another? Similarly, how can I send a capability (such as to memory)? Cryptography is an option for the second one, but seems inelegant and inefficient.
When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core.
Alternatively, are future versions of seL4 expected to scale to manycore systems without needing a multikernel? That would presumably make the answer trivial.
IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis
If I have a manycore machine, what is the best way to migrate a thread from one core to another? Similarly, how can I send a capability (such as to memory)? Cryptography is an option for the second one, but seems inelegant and inefficient.
I suspect Curtis didn’t quite give the answer the question Demi was after. Yes, in an SMP configuration, nothing special is needed. (And you don’t need nor should use cross-core IPC – that feature may go away). But if you are running a (clustered) multikernel and want to run a single system image (SSI) across clusters (eg to support a virtualised NUMA-aware Linux on top) then it’s no different from a distributed system (except that cross-cluster communication should be reliable, so a fair amount of complexity in the protocols goes away. Basically you have a bunch of separate systems, and the SSI is a higher-level software abstraction. Eg to have an abstraction of an object that is valid across the whole system, each node in has to provide its own copy of that object, and you need protocols to keep them coherent. This applies whether the object looks like an seL4 kernel object (address space, endpoint) or a Linux-style higher-level abstraction such as a file. And no, you can’t send caps across such a cluster, an seL4 cap has no meaning outside its kernel. You could have a similar cap-protected object abstraction, but both the distributed object and its caps will map to objects of the local kernel (and the abstraction layer would be responsible keeping the various local representations coherent). If this sounds crazy and complex, then that’s what it is. It just means that the seL4 abstractions, which are meant to be minimal wrappers around hardware, are just not at the right abstraction level for such a manycore system. Which is not surprising: it’s what you get if you pretend that a system where a message takes 1,000 cycle to get from one end to the other is just a simple multicore. Such a manycore is effectively a distributed system and should be treated as one. Gernot
On Fri, Apr 10, 2020, 4:12 AM Heiser, Gernot (Data61, Kensington NSW) < Gernot.Heiser@data61.csiro.au> wrote:
If I have a manycore machine, what is the best way to migrate a thread from one core to another? Similarly, how can I send a capability (such as to memory)? Cryptography is an option for the second one, but seems inelegant and inefficient.
I suspect Curtis didn’t quite give the answer the question Demi was after.
Yes, in an SMP configuration, nothing special is needed. (And you don’t need nor should use cross-core IPC – that feature may go away).
But if you are running a (clustered) multikernel and want to run a single system image (SSI) across clusters (eg to support a virtualised NUMA-aware Linux on top) then it’s no different from a distributed system (except that cross-cluster communication should be reliable, so a fair amount of complexity in the protocols goes away.
Basically you have a bunch of separate systems, and the SSI is a higher-level software abstraction. Eg to have an abstraction of an object that is valid across the whole system, each node in has to provide its own copy of that object, and you need protocols to keep them coherent. This applies whether the object looks like an seL4 kernel object (address space, endpoint) or a Linux-style higher-level abstraction such as a file.
And no, you can’t send caps across such a cluster, an seL4 cap has no meaning outside its kernel. You could have a similar cap-protected object abstraction, but both the distributed object and its caps will map to objects of the local kernel (and the abstraction layer would be responsible keeping the various local representations coherent).
If this sounds crazy and complex, then that’s what it is. It just means that the seL4 abstractions, which are meant to be minimal wrappers around hardware, are just not at the right abstraction level for such a manycore system. Which is not surprising: it’s what you get if you pretend that a system where a message takes 1,000 cycle to get from one end to the other is just a simple multicore. Such a manycore is effectively a distributed system and should be treated as one.
If I may ask, why is this? What prevents the SMP kernel from scaling to manycore systems? Is it the complexity of verifying fine-grained locking, the cost of atomic operations, or something else I missed? Gernot
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 13 Apr 2020, at 15:19, Demi Obenour
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
participants (3)
-
Demi Obenour -
Heiser, Gernot (Data61, Kensington NSW) -
Millar, Curtis (Data61, Kensington NSW)