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