Unikernel vs SMP vs Multi-Kernel docs?

New to seL4
1

I read through this very interesting thread: “Performance comparison with non-L4 kernels” which digressed into SMP vs Multi-kernel verification.

I am working on a Genode based project, at the moment genode supports seL4 as a kernel choice, but only integrated it in unikernel version (at least on ARM). I initially thought about looking at SMP integration, but reading through a few papers and the above mentioned thread, I understand that might not be my best move.

At the moment though, I haven’t really looked so much into the Multi-Kernel variant, and I am interested to learn the main differences on those, (and also if they have been run on ARM, A55 or A53 cores).

some of the links I have been injesting as a starting point:

Is there any good starting point to see the limitation of each arch? SMP vs MultiKernel?

Thanks for the help!

2

There currently isn’t official multikernel support in seL4 yet. That is, we have added syscalls to send IPIs to other cores for Arm GICv2 and v3, and on RISC-V it can be done via an SBI call. Adding IPI support to x86 would be more complicated and no one is working on that as far as I know (the people using multikernel on x86 don’t need it for their use case).

The current state is that people have been using single-core builds of seL4 and manually created a multikernel setup. The two approaches used are either building the kernel multiple times with different DTS files to partition RAM, or use custom loaders and hack the seL4 init code to tell it what the partitioning is.

There is a multikernel Mattermost channel, but it’s sadly not very active.

I think upstream support for a more flexible boot interface so people don’t need to hack the init code themselves would help. Now everyone does their own version of that, it would be better to consolidate.

For official support the verification side needs to be finished.

Main practical open issues are partitioning and how to deal with shared hardware, like interrupt controllers. That currently works mostly by chance.

If frameworks like Camkes or Microkit support mulitkernel, then the user changes are minimal. But in your case you use Genode and can’t use such frameworks and need to do the grunt work yourself.

From a practical point of view, I always recommend getting SMP working first, as that is trivial compared to multikernel. If you avoid cross-core IPC calls, then your user space software is ready for multikernel. Notifications can be done cross core via IPI support, you just need to tie the right IPI to the right notification. If you can’t do this 1:1 then things get more complicated and you need to multiplex signals in user space on both cores (once you have that, you can also implement cross-core IPC calls). Once you have SMP working, you can add multikernel support on top of that. It’s mostly additional orthogonal work. If you run into any issues, you can switch between the two configurations to see whether the problem is common or specific to one of them.

But to answer your original question: No, there are currently no docs about this.

Main limitation of SMP is that it will never be verified and that it breaks assumptions made in the code which are not easy to spot and can lead to bugs. Things are a lot more stable now than they used to be, but still. The big kernel lock also slows down syscalls and makes things less deterministic.

Multikernel isn’t verified yet, and not all changes necessary for proper multikernel support have been done yet (IRQ controller), the burden now is mostly all on the toolkit (compile, configuration and boot) side. That said, the current verification still mostly applies, IMHO running a different seL4 kernel on another core isn’t that different than having another bus master: Correctness depends mostly on partitioning. If you get that right, then the safety and security story is still pretty good.

3

Thanks a lot for this info, it looks like SMP will have to be my next stop no matter what then ^^;

Multi-kernel seems to be a handful, I was wondering how cross-core IPC would be handled on multi-kernel (if there were any way to achieve this), but I guess the answer is precisely “no, by design”.

so in essence, multi-kernel acts like multi-partitions.

Thanks!

4

Yes, multikernel is a handful.

On multikernel, a way to do cross-core IPC calls would be to marshal it via special user space proxy processes and use the available IPI support for notification. Simple example implementation:

Say client A on core 0 and a server B on core 1 and A wants to call B.

Client A would need to do a call to a proxy task running on core A.

The proxy would write the arguments + sender info to shared memory and notify another proxy on core B via IPI. The simple implementation now would block on a reply signal from the other core, having a proxy for each remote server. A more complex implementation would have a queue of IPC calls and would only postpone replying to the caller until it receives a reply from the other core.

The other core receives the IPI. If you have enough IPIs, you already know what it is for, as you can tie it 1:1 to a local notification. But usually you don’t have enough unique IPIs available to do this, so you would need to multiplex the IPIs. The way to do this is by writing extra info in shared memory on the sender side and using that on the receiver side. And that’s why doing IPC calls via the same proxy mechanism is relatively straightforward, because the only difference is more data being passed. After figuring out what the IPI was for, you can then forward to call to the local server. Simplest way is doing the IPC call directly, but that will block the task until the server replies.

Now you could stuff everything into one proxy task per core, but from a security and safety point of view that would be a bad design. It’s better to avoid cross-core IPC calls for this reason, but if you do them, at least have one proxy per server on each core. Notifications are pretty stateless, so much less harmful if they get hijacked (and much harder to get wrong as there is no variable amount of data).

As you can see, it’s a very slippery slope from simple stuff to too complex stuff that breaks the whole system security wise if you’re not careful.

For new designs, using a message queue + notifications/IPI would be better for cross-core communication than proxying IPC calls. The only reason to implement cross-core IPC is if you want to maintain the blocking semantics and don’t care about performance (mind that cross-core IPC calls are very slow on SMP too compared to normal IPC calls). However, having cross-core IPC can simplify system design, because it would mean that servers can be single-threaded and not SMP-aware, and for some servers having blocking semantics makes things a lot easier than async message queues.