August 2025 - Devel - lists.sel4.systems

seL4 vs QNX and Linux benchmarks
by Andrew Warkentin 07 Oct '25

07 Oct '25

Somebody in the Zoom call the other day (IIRC it was Gernot) said that seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is somehow faster in a simple benchmarking experiment in which a client repeatedly sends messages to a bit-bucket server, using the TSC to determine timing. I'm running both QNX and seL4 under identical VirtualBox configurations with a single core. I'm using a QNX 6.3.1 x86-32 image i have in my collection (x86-64 support was only added in 7.0; this is the most recent image I have with dev tools installed). The seL4 version I'm using is from February 2022 and is built for x86-64 with MCS enabled (the priority of the threads is 255, and both the timeslice and budget are the initial thread default of 5 ms). My benchmark times a loop of 10000 RPCs; for QNX it's just using the regular read() function on /dev/null or a custom server that also acts like /dev/null but forces a copy of the message into a server-provided buffer, and for seL4 I'm directly calling Send()/Recv()/Reply(). I've also tested Linux's /dev/null, and QNX's implementation actually seems somewhat faster than it (for the system /dev/null; the custom server's best case seems only slightly worse than under Linux). Under QNX and Linux I'm running a C implementation of the benchmark and under seL4 I tried both C and Rust implementations (which have very similar performance). The messages on QNX and Linux are 100 bytes, and on seL4 they are 2 words, which should be hitting the fast path. Here are the best and worst cases I got: seL4: 0.114-0.136s QNX, custom null server: 0.006-0.063s QNX, system null server: 0.002-0.022s Linux: 0.004-0.005s Has anyone else benchmarked seL4 IPC against that of QNX and gotten better (or comparable) results for seL4, unlike what I got? Is synchronous IPC just less optimized under seL4 than QNX?

6 13

About MSI-X interrupts on x86
by Alberto Lange 06 Sep '25

06 Sep '25

Hi all, here Albert I’m working on a SuperMicro E300-9D server and trying to passthrough an Intel X557-AT2 NIC to a Linux 6.1 guest. The .camkes configuration seems to be right, here are the configs for the device (the device is correctly detected on the VM): vm2.vm_ioports = []; vm2.pci_devices = [ { "name":"outer_eth", "bus":0xb5, "dev":0x0, "fun":1, "irq":"outer_eth", "memory":[ {"paddr":0xf9000000, "size":0x01000000, "page_bits":12}, // BAR0 {"paddr":0xfb000000, "size":0x00008000, "page_bits":12}, // BAR3 ] } ]; vm2.vm_irqs = [ {"name":"outer_eth", "ioapic":0, "source":0xb, "level_trig":0, "active_low":1, "dest":12} ]; I’m seeing the following errors during boot and when bringing the interface up: [ 2.040786] i40e 0000:00:01.0: MAC address: 3c:ec:ef:d2:88:85 [ 2.090786] i40e 0000:00:01.0: MSI-X vector reservation failed: -38 [ 2.109960] i40e 0000:00:01.0: MSI-X not available, trying MSI [ 2.115660] i40e 0000:00:01.0: MSI init failed - -38 [ 2.121656] i40e 0000:00:01.0: MSI-X and MSI not available, falling back to Legacy IRQ [ 2.220802] i40e 0000:00:01.0 eth1: NIC Link is Up, 1000 Mbps Full Duplex, Flow Control: None [ 2.290774] i40e 0000:00:01.0: Features: PF-id[1] VSIs: 66 QP: 1 VxLAN Geneve PTP VEPA ... # ifconfig eth1 up [ 451.042525] i40e 0000:00:01.0 eth1: NETDEV WATCHDOG: CPU: 0: transmit queue 0 timed out 5770 ms [ 451.052764] i40e 0000:00:01.0 eth1: tx_timeout: VSI_seid: 391, Q 0, NTC: 0x0, HWB: 0x1, NTU: 0x1, TAIL: 0x1, INT: 0x0 [ 451.065876] i40e 0000:00:01.0 eth1: tx_timeout recovery level 2, txqueue 0 [ 456.082601] i40e 0000:00:01.0 eth1: NETDEV WATCHDOG: CPU: 0: transmit queue 0 timed out 10810 ms My thought is that this NIC does not work reliably with legacy IRQ mode. My question is: Is there any implementation of MSI-X interrupts for x86 in the seL4 VMM, or plans to support it? If such support exists, I would like to contribute, as I plan to share my project once it’s finished. Thanks in advance for any guidance or suggestions. Albert

3 4

Error on managing the same IRQ in 2 VM (x86) #84
by Alberto Lange 20 Aug '25

20 Aug '25

Hi! I'm working on top of the zmq_samples example, trying to set up 2 Ethernet devices on 2 of the 3 VM's. The passthrough for both VM's has been done, and both detect the NICs. For more information, this is the setup for the irqs in the camkes file: vm0.vm_irqs = [ {"name":"inner_eth", "ioapic":0, "source":0xb, "level_trig":1, "active_low":1, "dest":10} ]; vm2.vm_irqs = [ {"name":"outer_eth", "ioapic":0, "source":0xb, "level_trig":1, "active_low":1, "dest":12} ]; My problem is related to having the same IRQ11 in both e1000e devices. I can't control this; that is what QEMU provides. When I set up the first NIC in any VM, say VM0, doing ifconfig eth1 up, it works correctly, but when I try to bring up the other one, VM2, the whole system freezes for a moment. Then VM0 complains about this: [ 48.557120] irq 10: nobody cared (try booting with the "irqpoll" option) [ 48.557120] CPU: 0 PID: 0 Comm: swapper/0 Tainted: G W 4.9.337+ #19 [ 48.557120] df811f94 d08f1778 df807d00 00000000 df811fa8 d08f08e0 df807d00 00000000 [ 48.557120] d0459f68 df811fc4 d04596ec 0000000b 00000000 df807d00 00000000 d0459f68 [ 48.557120] df811fd8 d0457a55 00000000 df807d00 df807d64 df811fe8 d0457a7e df807d00 [ 48.557120] Call Trace: [ 48.557120] [ 48.557120] [] dump_stack+0x4f/0x63 [ 48.557120] [] __report_bad_irq+0x33/0x98 [ 48.557120] [] ? unmask_irq+0x22/0x22 [ 48.557120] [] note_interrupt+0x185/0x1c3 [ 48.557120] [] ? unmask_irq+0x22/0x22 [ 48.557120] [] handle_irq_event_percpu+0x31/0x38 [ 48.557120] [] handle_irq_event+0x22/0x3b [ 48.557120] [] handle_level_irq+0x52/0x80 [ 48.557120] [] handle_irq+0x91/0xb6 [ 48.557120] [ 48.557120] [ 48.557120] [] do_IRQ+0x33/0x99 [ 48.557120] [] common_interrupt+0x2c/0x34 [ 48.557120] [] ? __do_softirq+0x55/0x1a1 [ 48.557120] [] ? _local_bh_enable+0x6c/0x6c [ 48.557120] [] call_on_stack+0x40/0x46 [ 48.557120] [ 48.557120] [] ? irq_exit+0x56/0x91 [ 48.557120] [] ? do_IRQ+0x7f/0x99 [ 48.557120] [] ? common_interrupt+0x2c/0x34 [ 48.557120] [] ? default_idle+0x16/0x18 [ 48.557120] [] ? arch_cpu_idle+0xd/0xf [ 48.557120] [] ? default_idle_call+0x14/0x16 [ 48.557120] [] ? cpu_startup_entry+0xbb/0x158 [ 48.557120] [] ? rest_init+0x5d/0x5f [ 48.557120] [] ? start_kernel+0x339/0x343 [ 48.557120] [] ? i386_start_kernel+0x3e/0x40 [ 48.557120] handlers: [ 48.557120] [] e1000_intr [ 48.557120] Disabling IRQ #10 Any interruption goes to VM2; they all go to VM0 but are not intended to go to that one, so they are ignored. Any thoughts on this would be appreciated!

2 2

seL4 developer hangout reminder
by Birgit Brecknell 18 Aug '25

18 Aug '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 20 Aug, 8:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Experimental prototype of CHERI-enabled seL4 is released
by Hesham Almatary 13 Aug '25

13 Aug '25

Hello, The CHERI Alliance has released a prototype of CHERI-seL4, an experimental version of the seL4 microkernel with CHERI support. This release includes CHERI-Microkit, a lightweight userspace framework, and a set of exercises and tutorials designed to help developers explore CHERI’s potential in a real microkernel environment. The release is aimed at developers who want to build and experiment with memory-safe C/C++ software on seL4. It supports the draft CHERI-RISC-V architecture and runs on QEMU, Codasip’s X730 processor, CHERI-Toooba, and CHERI-CVA6 on FPGA. For those who are unfamiliar with CHERI, CHERI support in seL4 enables memory-safe C/C++ user-level projects and applications without having to (re)write code in languages like Rust. This complement's seL4's strong isolation between different components, enforced by the MMU and seL4's software capabilities. We welcome any feedback. Learn more: https://cheri-alliance.org/cheri-sel4-and-cheri-microkit-released/ Regards, Hesham

4 14

seL4 developer hangout reminder
by Birgit Brecknell 04 Aug '25

04 Aug '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 5 Aug, 22:00 UTC For your local date and time please see https://sel4.systems/stay-informed.html#calendar Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0