October 2024 - 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

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 18 Apr '25

18 Apr '25

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

5 5

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

iMX8MM seL4 12.1.0 running a VM
by Zippy Manaic 21 Nov '24

21 Nov '24

Hi, I have encountered a problem where the device tree is not correctly being parsed resulting in interrupts not being routed to the VM. A node which exhibits this issue is (there are several more in the iMX8MM device tree that also trigger the problem) ``` snvs@30370000 { compatible = "fsl,sec-v4.0-mon\0syscon\0simple-mfd"; reg = <0x30370000 0x10000>; phandle = <0x1b>; snvs-rtc-lp { compatible = "fsl,sec-v4.0-mon-rtc-lp"; regmap = <0x1b>; offset = <0x34>; interrupts = <0x00 0x13 0x04 0x00 0x14 0x04>; clocks = <0x02 0xe4>; clock-names = "snvs-rtc"; }; }; ``` Interrupts 0x13 and 0x14 should be included in the camkes_dtb_irqs[] variable but they are not. Looking at the node as it is parsed in macros.py via the function parse_dtb_node_interrupts {'compatible': ['fsl,sec-v4.0-mon', 'syscon', 'simple-mfd'], 'reg': [808910848, 65536], 'phandle': [27], 'snvs_rtc_lp': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c28f10>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28f70>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c28fd0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f070>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f0d0>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f130>], 'snvs_rtc_lp_compatible': ['fsl,sec-v4.0-mon-rtc-lp'], 'snvs_rtc_lp_regmap': [27], 'snvs_rtc_lp_offset': [52], 'snvs_rtc_lp_interrupts': [0, 19, 4, 0, 20, 4], 'snvs_rtc_lp_clocks': [2, 228], 'snvs_rtc_lp_clock_names': ['snvs-rtc'], 'snvs_powerkey': [<pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f1f0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f250>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f2b0>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f310>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f370>, <pyfdt.pyfdt.FdtPropertyWords object at 0x7483b4c2f3d0>, <pyfdt.pyfdt.FdtProperty object at 0x7483b4c2f430>, <pyfdt.pyfdt.FdtPropertyStrings object at 0x7483b4c2f490>], 'snvs_powerkey_compatible': ['fsl,sec-v4.0-pwrkey'], 'snvs_powerkey_regmap': [27], 'snvs_powerkey_interrupts': [0, 4, 4], 'snvs_powerkey_clocks': [2, 228], 'snvs_powerkey_clock_names': ['snvs-pwrkey'], 'snvs_powerkey_linux_keycode': [116], 'snvs_powerkey_wakeup_source': [], 'snvs_powerkey_status': ['okay'], 'this_address_cells': [1], 'this_size_cells': [1], 'this_node_path': '/soc@0/bus@30000000/snvs@30370000'} The function is looking for 'interrupts' but the interrupt declaration in the child node has been renamed to 'snvs_rtc_lp_interrupts'. This explains why the interrupts are omitted from the template generated code. A hacky fix, that does appear to work, is to paste the interrupt declarations into the parent node. I'm sure there's a more elegant way to resolve this but my detailed knowledge in this area is lacking. I am going to have a look at seL4 13.0.0 to see if this has already been fixed with a view to a potential backport but thought I'd check here before starting to dig a new hole to fall into. Many thanks, Zippy

2 3

AMD64 - how much virtual address space does the kernel map?
by Ben McCart 30 Oct '24

30 Oct '24

Hellow all, I have been working through the tutorials and doing some experimenting and ran into behavior that very much surprised me. I can seL4_X86_PageTable_Map & seL4_X86_Page_Map to virtual addresses starting at the 96 MB address (0x06000000) with no errors. However, as soon as I try to seL4_X86_PageDirectory_Map that same virtual address I get the error seL4_DeleteFirst. I didn't think the kernel mapped anything for the root address above 64 MB virtual address range for the root address in these tutorials. If it did I would have expected an error for seL4_X86_PageTable_Map & seL4_X86_Page_Map. What is going on? What am I missing? How can I avoid expecting to map a virtual address in a range already mapped by the kernel for the root process on a given architecture? - Ben McCart

2 1

seL4 fails to boot multiple core at CPU 0x1.
by Vishal Gupta 30 Oct '24

30 Oct '24

Dear All, I am a seL4 enthusiast , I am trying to port , build and test seL4 for ARM64 Cortex A53 based hardware. For Single core , I am able to boot via elf-loader then jump to kernel and successfully run Hello World program without any issues. But when I am trying to change it to multiple core SMP enabled on my hardware or even in ARM Qemu setup it is failing to boot. Can anyone please guide me , if seL4 supports multicore than for which version of ARM / board it currently supports , as I could see support for only Sabre-Arm32, which is ARMv7A. Boot log attach for reference. ———————————————————————— ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a4c000…40f57137] No DTB passed in from boot loader. Looking for DTB in CPIO archive…found at 40bacbe8. Loaded DTB from 40bacbe8. paddr=[4024c000…4024dfff] ELF-loading image ‘kernel’ to 40000000 paddr=[40000000…4024bfff] vaddr=[ffffff8040000000…ffffff804024bfff] virt_entry=ffffff8040000000 ELF-loading image ‘sel4test-driver’ to 4024e000 paddr=[4024e000…40654fff] vaddr=[400000…806fff] virt_entry=40e700 Boot cpu id = 0x0, index=0 HVC is not supported for PSCI! Failed to boot cpu 0x1: 18446744073709551615 abort() called. ——————————————————————————— Looking for any guidance, as it will be helpful for me to move forward . Regards, Vishal

2 1

seL4 developer hangout reminder
by Birgit Brecknell 28 Oct '24

28 Oct '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 29 Oct, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. 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

Device memory access issue on sel4 user driver
by misbah khan 25 Oct '24

25 Oct '24

Hello sel4 developers, I am using seL4 for in our arm64 based hardware platform. I need to write a simple driver where i need to read/write some memory mapped registers The device physical address is "0x40520000" When i print the bootinfo using the below code: /*-- filter TaskContent("untyped-start", TaskContentType.ALL, subtask='init') -*/ printf(" CSlot \tPaddr \tSize\tType\n"); for (seL4_CPtr slot = info->untyped.start; slot != info->untyped.end; slot++) { seL4_UntypedDesc *desc = &info->untypedList[slot - info->untyped.start]; printf("%8p\t%16p\t2^%d\t%s\n", (void *) slot, (void *) desc->paddr, desc->sizeBits, desc->isDevice ? "device untyped" : "untyped"); I get the following output: CSlot Paddr Size Type 0x1ac 0 2^30 device untyped 0x1ad 0x40000000 2^28 device untyped 0x1ae 0x50000000 2^23 device untyped 0x1af 0x50810000 2^16 device untyped 0x1b0 0x50820000 2^17 device untyped I am mappint the physical address to virtual and trying to access it as: va = ps_io_map(&ops.io_mapper, (uintptr_t) 0x40520000,0x3000, PS_MEM_NORMAL); ZF_LOGE("Physical address 0x%x mapped to virtual address %p \n",DEV_REG_PADDR,va); for(int j=0;j<DEV_REG_SIZE;j+=sizeof(unsigned int)) { ZF_LOGE("Loc %d --> 0x%x ",j,*(unsigned int*)(va+j)); } I am able to access some registers, but then it gives a fault (after printing 5-6 register values) Similar is the behaviour with any reg between the range 0x40000000 - 0x50000000 Attaching the sample code and output: I am able to access first two address location, after that it gives halt. Regards, Misbah

2 2

sel4 for Imx8Plus
by janarthanan.b＠teclever.com 22 Oct '24

22 Oct '24

Hi sel4 dev team, I'm working on imx8 Plus board for that Building seL4test is done and generated the binary image file of "sel4test-driver-image-arm-imx8mp-evk" with the size of 5mb as per the procedure on sel4 websites. I moved this into sd card and trying to boot into board.but i cant able to boot it. What is the issue on this and how to solve it? if we need to do uboot what's the procedure for that?

3 4