More Multiprocessing on seL4: Are Efficient SMP Virtual Machines Possible on Verifiable seL4 Kernels?

Moderators: Matthew Brecknell
Speakers: Kent McLeod
Multicore systems with verified seL4 is just around the corner with multikernels - kernel state is isolated on each core and avoid kernel-mode concurrency for easier verification. Does this mean that it's not possible to support multicore at user level? Let's find out by investigating whether it's possible to efficiently support virtualizing SMP virtual machines
with small core counts using our multikernel mechanisms.

This talk will detail how to construct such a system, the work involved and examples of how it can be used.