- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 15 Sep '25

15 Sep '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 17 Sep, 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

Kernel use of MPIDR_EL1 register on ARM
by Julia Vassiliki 10 Sep '25

10 Sep '25

For ARM platforms, the hardware provides access to the MPIDR ("Multiprocessor Identification Register") [1], which, amongst other things, provides access to 2 (or 3, for AArch64) affinity levels: Aff0, Aff1, Aff2, and possibly Aff3. However, seL4 instead seems to gather the CPU index from a loader-set `tpidr_el1`. /* tpidr_el1 has the logic ID of the core, starting from 0 */ mrs x6, tpidr_el1 /* Set the sp for each core assuming linear indices */ ldr x5, =BIT(CONFIG_KERNEL_STACK_BITS) mul x5, x5, x6 This is then overwritten later. with the kernel stack address. Is there any reasoning for why it was done this way? The elfloader [3] then has read the MPIDR and converted it to TPIDR_EL1 for the kernel, and it uses a generated table to map the MPIDR IDs to "logical core IDs" [4]. Here is the boot log for the TX2, which does use non-contiguous Aff0 IDs. Boot cpu id = 0x100, index=2 Core 257 is up with logic id 1 Core 258 is up with logic id 2 Core 259 is up with logic id 3 Enabling MMU and paging Of note here is 2 things: 1. That the ARM PSCI specification [5], for "target_cpu" when calling PSCI_ON or OFF methods (such as done in the elfloader) expects a MPIDR-like ID (I say "like" because it is with the "U" and "MT" bits masked out). In its current state, the seL4_BootInfo provided ID is instead the logical ID, which means that there's no way to see the value of MPIDR from userspace. 2. The GICv3 uses MPIDR affinity values when sending IPIs, and so the kernel does actually maintain a "mpidr_map" which wouldn't be necessary if everything talked in terms of MPIDRs. (It would still be required for other reasons on SMP as opposed to multikernel, though). BOOT_CODE void cpu_initLocalIRQController(void) { word_t mpidr = 0; SYSTEM_READ_WORD(MPIDR, mpidr); mpidr_map[CURRENT_CPU_INDEX()] = mpidr; active_irq[CURRENT_CPU_INDEX()] = IRQ_NONE; gicr_init(); cpu_iface_init(); } In the spirit of being a minimal hardware abstraction, I feel that it makes more sense for the kernel's APIs to be in terms of MPIDRs [6], but that it would probably be a breaking change. Internally, aside from this, it makes *more* sense for the kernel to think in terms of MPIDRs for the core values, rather than a "logical core ID". Some context for how this is represented in the device trees: In the device tree documentation 'Documentation/devicetree/bindings/arm/cpus.yaml' [2] the `<reg>` field of the cpus node tells the values of each of the CPU nodes; mapping the affinities (possibly non-contiguous) to a contiguous CPU index could be done with a build-time lookup table. For example, here is the first part of the OdroidC4 device tree, which tells us that node 0 is Aff0=0, Aff1=0. cpus { #address-cells = <0x02>; #size-cells = <0x00>; cpu@0 { device_type = "cpu"; reg = <0x00 0x00>; }; /* etc */ } [1]: https://arm.jonpalmisc.com/latest_sysreg/AArch64-mpidr_el1 [2] https://www.kernel.org/doc/Documentation/devicetree/bindings/arm/cpus.yaml [3]: https://github.com/seL4/seL4_tools/blob/26f94df7e97a04f8ee49c1e94a0aa120365… [4]: https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/… [5]: https://documentation-service.arm.com/static/6703a8b8d7e4b739d817e10d [6]: So, the SMP affinity APIs, and BootInfo->nodeID field. Julia This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.

3 3

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

On LionsOS and Switches
by wocexeg869＠forexru.com 22 Jul '25

22 Jul '25

Many enterprise grade switches from Cisco to Juniper switches are running on Linux. That also is the case with prosumer hardware such as Ubiquiti, Mikrotik (CRS line), Aruba, etc... Wouldn't this be a good use case for LionsOS? The security of the layer 2 is an important part of the security of the overall network and it should be easier to implement compared to the firewall that is currently being worked on. Thank you for your attention to this matter!

3 2

seL4 developer hangout reminder
by Birgit Brecknell 21 Jul '25

21 Jul '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 23 July, 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

seL4 developer hangout reminder
by Birgit Brecknell 07 Jul '25

07 Jul '25

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 8 July, 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