# Sel4 unikernel vs multi-kernel vs SMP on genode/sculpt
**URL:** https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319
**Category:** Developer's Corner
**Created:** [May 21, 2026, 5:05pm UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319 "2026-05-21T17:05:58Z")
**Posts on this page:** 9
**Page:** 1
### Author:  [@fdelizy](https://genode.discourse.group/u/fdelizy)
#### Post date: [May 21, 2026, 5:05pm UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/1 "2026-05-21T17:05:58Z")
Hi,
I have been spending some time to investigate why sculpt-os+sel4 was rather slow on ARM IMX8MP, and aside from finding some stability issues that I am still working on, I also found the default config for seL4 is actually mono-core, (non-SMP).
_kinda filling silly for not checking that earlier TBH ^^;_
Reviewing [a few threads](https://sel4.discourse.group/t/performance-comparison-with-non-l4-kernels/1023/5) and papers, I can understand the SMP version isn’t on a path to verification, so choosing unikernel over SMP makes some sense from a security standpoint, yet, the multi-kernel configuration could be an option. It would require a bit more tooling I am sure, but I was wondering, has genode team had a look at the multi-kernel configuration of seL4 for integration?
Right now, mono-thread payloads are quite a bit faster on sel4 compared to hw, but obviously, hw beats sel4 on SMP (since SMP is not activated ^^; )
any thougths?
thanks!
---
### Author:  [@skalk](https://genode.discourse.group/u/skalk)
#### Post date: [May 22, 2026, 9:58am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/2 "2026-05-22T09:58:03Z")
> [@fdelizy](#):
>
> Reviewing [a few threads](https://sel4.discourse.group/t/performance-comparison-with-non-l4-kernels/1023/5) and papers, I can understand the SMP version isn’t on a path to verification, so choosing unikernel over SMP makes some sense from a security standpoint, yet, the multi-kernel configuration could be an option. It would require a bit more tooling I am sure, but I was wondering, has genode team had a look at the multi-kernel configuration of seL4 for integration?
The short answer is: no.
> [@fdelizy](#):
>
> Right now, mono-thread payloads are quite a bit faster on sel4 compared to hw, but obviously, hw beats sel4 on SMP (since SMP is not activated ^^; )
I would be careful with too general assumptions about the runtime performance in between two different underlying kernels in Genode.
When looking at different workloads of our nightly tests, I can see diverse results regarding time needed to succeed in between both mentioned kernels. There are plenty reasons not necessarily directly related to the kernel itself that are responsible therefore. For instance, the initial costs being spent by a client to establish a session are generic, but the actual costs differ on the kernels (what needs to be paid for kernel-resource management). Therefore, it happens that the initial session establishment can be very costly on one kernel, where the client has to try this several times (each time delivering more ram/caps) in a loop. If you have a scenario centered on a lot of dynamic regarding session opening/closing, you get quite different result than maybe I/O heavy loads using shared memory and signaling, and so on. In our regular tests I can see for instance a slightly faster success of the “nic\_router\_stress” test (artificial network test with no real I/O) on sel4, but regarding the “bomb” test (creating and destroying tons of components) it performance collapses in constrast to base-hw. But even here I would be cautious to assume too much from this observation. One would need to first analyze what is actually bottleneck in which situation. Sometimes it might be simply a configuration issue.
---
### Author:  [@fdelizy](https://genode.discourse.group/u/fdelizy)
#### Post date: [May 22, 2026, 10:06am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/3 "2026-05-22T10:06:55Z")
True. That being said, my observations are based on a few benchmarks I created to avoid that bias, I am looking at the best way to share those results in a meaningful fashion (but I digress). You mention you have regular tests, could you point me at what are those? I would be interested to learn from them and maybe add that to my benchmarks as well 🙂
Either way, I need to study a bit more the base-sel4 layer (and base-hw layer for that matter) to see if the multi-kernel integration would be possible or even make sense then. That will be a low priority for this project though, so it might come rather late ^^;
Thanks for the feedback
---
### Author:  [@alex-ab](https://genode.discourse.group/u/alex-ab)
#### Post date: [May 22, 2026, 10:52am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/4 "2026-05-22T10:52:29Z")
> [@skalk](#):
>
> > [@fdelizy](#):
> >
> > Reviewing [a few threads](https://sel4.discourse.group/t/performance-comparison-with-non-l4-kernels/1023/5) and papers, I can understand the SMP version isn’t on a path to verification, so choosing unikernel over SMP makes some sense from a security standpoint, yet, the multi-kernel configuration could be an option. It would require a bit more tooling I am sure, but I was wondering, has genode team had a look at the multi-kernel configuration of seL4 for integration?
>
> The short answer is: no.
What I want to add: for x86 we enabled SMP support, but not for any seL4 ARM platform, simply there was no need to do so.
---
### Author:  [@fdelizy](https://genode.discourse.group/u/fdelizy)
#### Post date: [May 22, 2026, 10:59am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/5 "2026-05-22T10:59:09Z")
> [@alex-ab](#):
>
> What I want to add: for x86 we enabled SMP support, but not for any seL4 ARM platform, simply there was no need to do so.
got it, I might look into that as well, but since the SMP version is not verfiable according to seL4 community, I might just activate and fix or go for the MultiKernel directly (still trying to understand the limitations).
---
### Author:  [@skalk](https://genode.discourse.group/u/skalk)
#### Post date: [May 22, 2026, 11:04am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/6 "2026-05-22T11:04:49Z")
> [@fdelizy](#):
>
> True. That being said, my observations are based on a few benchmarks I created to avoid that bias, I am looking at the best way to share those results in a meaningful fashion (but I digress). You mention you have regular tests, could you point me at what are those? I would be interested to learn from them and maybe add that to my benchmarks as well 🙂
The list of tests we run nightly can be found here:
> **[genode/tool/autopilot.list at main](https://codeberg.org/genodelabs/genode/src/branch/main/tool/autopilot.list)**
>
> genode - Genode OS Framework
The actual results (logs) are not publicly available, but are part of our internal test-suite.
One of the potentially interesting run-scripts is for instance depot\_autopilot.run, which itself contains a bunch of independent ~90 tests that are not dependent on additional peripherals.
---
### Author:  [@fdelizy](https://genode.discourse.group/u/fdelizy)
#### Post date: [June 25, 2026, 4:21pm UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/7 "2026-06-25T16:21:54Z")
a followup question, do you also publish a list of platforms that are subjected to those tests? does this include qemu versions or only actual hardware? or both?
I am interested to see what I should validate my code against to ensure stability too
---
### Author:  [@skalk](https://genode.discourse.group/u/skalk)
#### Post date: [June 29, 2026, 9:59am UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/8 "2026-06-29T09:59:46Z")
In general, no we don’t publish that data, because nobody had the time to sanity the test-data from infrastructural sensitive information yet.
The following table shows which kernels are tested on which hardware/emulator currently:
| Hardware | hw | nova | sel4 | Fiasco.OC |
| --- | --- | --- | --- | --- |
| Raspberry Pi 1 (arm\_v6) | yes | no | no | no |
| i.MX53 QSB | yes | no | no | no |
| i.MX6Q Sabrelite | yes | no | yes | yes |
| i.MX7D Sabre | yes | no | no | yes |
| Qemu PBXA9 | yes | no | no | yes |
| Qemu Zynq | yes | no | no | no |
| Zynq QRSP 31x | yes | no | no | no |
| iMX8MQ EVK | yes | no | yes | no |
| Qemu Raspberry 3 | yes | no | no | yes |
| Qemu RiscV | yes | no | no | no |
| PC (32-bit) | no | yes | no | yes |
| PC (64-bit) | yes | yes | yes | yes |
| Qemu PC (32-bit) | no | yes | no | yes |
| Qemu PC (64-bit) | yes | yes | yes | yes |
I did not listed Linux, Pistachio, OKL4, and old Fiasco as kernels, which are tested on Qemu and PC hardware as well.
---
### Author:  [@fdelizy](https://genode.discourse.group/u/fdelizy)
#### Post date: [June 29, 2026, 2:41pm UTC](https://genode.discourse.group/t/sel4-unikernel-vs-multi-kernel-vs-smp-on-genode-sculpt/319/9 "2026-06-29T14:41:55Z")
Thanks a lot for sharing!