June 2025 - Devel - lists.sel4.systems

question about the seL4/camkes-vm-examples
by PX 20 Nov '25

20 Nov '25

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

5 7

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

06 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

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

19 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 22 Jun '25

22 Jun '25

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

Fwd: Re: I am interested in porting LionOS to X64 architecture
by Jingyao Zhou 10 Jun '25

10 Jun '25

Resend because I forgot to CC the mailing list. Begin forwarded message: From: Jingyao Zhou <jingyao.zhou(a)unsw.edu.au> Date: 5 June 2025 at 11:47:49 GMT+8 To: Peter Relich <prelich(a)intellisenseinc.com> Subject: Re: [seL4] Re: I am interested in porting LionOS to X64 architecture Hi Peter, I am glad to see that you are interested in contributing to x86 support for LionsOS! Several x86-related works/plans are going on in the Trustworthy Systems Team. For the seL4 kernel, there are pending pull requests for remappable MSI and IOAPIC supports that need to be updated and tested; we would like to add posted interrupts and MSI-x, but there are no concrete plans yet. For the x86 Microkit, we adopted Neutrality-CH's works and have been updating it (e.g. adding virtulization support). There are two major issues: * We need to figure out a nicer way to generate the machine description for x86 machines * We also need to add IOMMU supports We hope to upstream the work soon. For seL4 Device Driver Framework: we have working examples running on Supermicro servers as well as QEMU. We hope to upstream them soon as well. For adding x86 support for libvmm: the work is on hold due to the prerequisites, plus a kernel issue with multi-IOAPIC support. We will resume it as soon as possible. We apologize for the lack of information; we will keep our progress on x86 supports updated on GitHub in the future. Regards, Jade. ________________________________ From: Peter Relich via Devel <devel(a)sel4.systems> Sent: Wednesday, June 4, 2025 3:49 AM To: devel(a)sel4.systems <devel(a)sel4.systems> Subject: [seL4] Re: I am interested in porting LionOS to X64 architecture Thanks everyone. I got authorized to continue my effort, and I was looking into what is currently available. I don't have to worry about red/black channels for now, so confidentiality is not yet a priority. My main priority is to create a steel thread so that if the main operating system crashes, a giant robotic vehicle can be teleoperated or shutdown without hurting anyone. I saw that Neutrality-CH (Switzerland) had forked the Microkit library for x86 (https://github.com/Neutrality-ch/microkit) but they had only made two commits, the last one was in December 17. I tried to contact them a few weeks ago, but I didn't hear back so I'm not sure the status/funding of their project. Anyway, currently the VMM capabilities are not developed for their fork which would make deployment of an OS tedious. At first glance, it looks like I need to put some work into building a VMM into their fork by studying and then calling the seL4 vcpu, interrupt, x86_src routines into their Microkit fork? I guess my question now as I parse through everything. Is the Neutrality-CH fork the best, most recent x86 fork of the microkit? Or is there another library/fork I should consider for development? I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request, but since I'm working on a specific Intel architecture (8th gen, uses Intel VT-x and VT-d for virtualization), I can avoid over generalizing my solution and focus on this specific application. Is there any value in extracting/porting the work performed in CAmkES x86 virtualization for the microkit x86 fork? Thanks again for all the help! -Peter ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments. _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.

1 0

Re: I am interested in porting LionOS to X64 architecture
by Peter Relich 10 Jun '25

10 Jun '25

Thanks everyone. I got authorized to continue my effort, and I was looking into what is currently available. I don't have to worry about red/black channels for now, so confidentiality is not yet a priority. My main priority is to create a steel thread so that if the main operating system crashes, a giant robotic vehicle can be teleoperated or shutdown without hurting anyone. I saw that Neutrality-CH (Switzerland) had forked the Microkit library for x86 (https://github.com/Neutrality-ch/microkit) but they had only made two commits, the last one was in December 17. I tried to contact them a few weeks ago, but I didn't hear back so I'm not sure the status/funding of their project. Anyway, currently the VMM capabilities are not developed for their fork which would make deployment of an OS tedious. At first glance, it looks like I need to put some work into building a VMM into their fork by studying and then calling the seL4 vcpu, interrupt, x86_src routines into their Microkit fork? I guess my question now as I parse through everything. Is the Neutrality-CH fork the best, most recent x86 fork of the microkit? Or is there another library/fork I should consider for development? I saw that their approach for pre-generating an ELF file for the bootloader was the main obstacle for their pull request, but since I'm working on a specific Intel architecture (8th gen, uses Intel VT-x and VT-d for virtualization), I can avoid over generalizing my solution and focus on this specific application. Is there any value in extracting/porting the work performed in CAmkES x86 virtualization for the microkit x86 fork? Thanks again for all the help! -Peter ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

2 2

Booting software on Odroid-C4
by Julia Royer 06 Jun '25

06 Jun '25

Hello, I would like to boot my Microkit software on an Odroid-C4, but I’m a bit confused about the process. Is there any tutorial available, or perhaps an existing U-Boot image that I could use? Thank you for your help. Best regards, Julia Royer

5 8

seL4 developer hangout reminder
by Birgit Brecknell 05 Jun '25

05 Jun '25

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