question about the seL4/camkes-vm-examples
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...
"PX" == PX <seawolf.peng@gmail.com> writes:
PX> Hi,All I am trying to build the seL4 VMM example for the PX> qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build PX> the vmm image successfully, but I cannot run the image. Here are PX> what I did: 1. I use the PX> "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" PX> command. I'm seeing the same issue. It looks like a NULL pointer reference. FWIW the CI runs on real hardware are succeeding. It's _meant_ to work ... will chase on Monday. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
"Peter" == Peter Chubb via Devel <devel@sel4.systems> writes:
"PX" == PX <seawolf.peng@gmail.com> writes: PX> Hi,All I am trying to build the seL4 VMM example for the PX> qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build PX> the vmm image successfully, but I cannot run the image. Here are PX> what I did: 1. I use the "../init-build.sh PX> -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command.
Peter> I'm seeing the same issue. It looks like a NULL pointer Peter> reference. FWIW the CI runs on real hardware are succeeding. Peter> It's _meant_ to work ... will chase on Monday. Turns out there was a bug in the continuous integration system that was meant to catch this kind of thing: https://github.com/seL4/ci-actions/issues/339 We'll get that fixed then work on the cause for the breakage. Thankyou for reporting the issue! -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.
Hello everyone, I'm still encountering the same issue when trying to run the system according to the manual. I'm not sure if this problem has been resolved yet. How should I proceed to run it correctly? I used the following command: ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt It reports an error: CMake Error at apps/Arm/vm_minimal/CMakeLists.txt:94 (message): Only AARCH64 is supported If I comment out the relevant code: --- a/apps/Arm/vm_minimal/CMakeLists.txt +++ b/apps/Arm/vm_minimal/CMakeLists.txt @@ -90,9 +90,9 @@ elseif("${KernelARMPlatform}" STREQUAL "qemu-arm-virt") # QEMU supports ARMv7/aarch32 and ARMv8/aarch32, but currently there are # Linux images for aarch64 only. However, it is unclear if that is the only # blocker to get this example run in QEMU on aarch32. - if(NOT KernelSel4ArchAarch64) - message(FATAL_ERROR "Only AARCH64 is supported") - endif() + # if(NOT KernelSel4ArchAarch64) + # message(FATAL_ERROR "Only AARCH64 is supported") + # endif() The compilation proceeds normally, but the following error still occurs during runtime: ./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 r4p0 paddr=[6141d000..626dd047] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6145eb20. Loaded DTB from 6145eb20. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'rootserver' to 60044000 paddr=[60044000..613fcfff] vaddr=[10000..13c8fff] virt_entry=18e10 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..e0043e84) [e0044000..e13fd000) [ff000000..ff200000) Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: 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) clean_up@fdtgen.c:374 Non-existing node /platform@c000000 specified to be kept 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... QEMU: Terminated
Hi jiazhouyang Have you tried passing `-DAARCH64=TRUE`, so it looks like: ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt -DAARCH64=TRUE I can also reproduce this behaviour. It looks like the documentation is incorrect. Julia ________________________________________ From: jiazhouyang--- via Devel <devel@sel4.systems> Sent: Thursday, 20 November 2025 13:22 To: devel@sel4.systems Subject: [seL4] Re: question about the seL4/camkes-vm-examples Hello everyone, I'm still encountering the same issue when trying to run the system according to the manual. I'm not sure if this problem has been resolved yet. How should I proceed to run it correctly? I used the following command: ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt It reports an error: CMake Error at apps/Arm/vm_minimal/CMakeLists.txt:94 (message): Only AARCH64 is supported If I comment out the relevant code: --- a/apps/Arm/vm_minimal/CMakeLists.txt +++ b/apps/Arm/vm_minimal/CMakeLists.txt @@ -90,9 +90,9 @@ elseif("${KernelARMPlatform}" STREQUAL "qemu-arm-virt") # QEMU supports ARMv7/aarch32 and ARMv8/aarch32, but currently there are # Linux images for aarch64 only. However, it is unclear if that is the only # blocker to get this example run in QEMU on aarch32. - if(NOT KernelSel4ArchAarch64) - message(FATAL_ERROR "Only AARCH64 is supported") - endif() + # if(NOT KernelSel4ArchAarch64) + # message(FATAL_ERROR "Only AARCH64 is supported") + # endif() The compilation proceeds normally, but the following error still occurs during runtime: ./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 r4p0 paddr=[6141d000..626dd047] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6145eb20. Loaded DTB from 6145eb20. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'rootserver' to 60044000 paddr=[60044000..613fcfff] vaddr=[10000..13c8fff] virt_entry=18e10 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..e0043e84) [e0044000..e13fd000) [ff000000..ff200000) Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/204 T0xffc13400 "rootserver" @106e0]: 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) clean_up@fdtgen.c:374 Non-existing node /platform@c000000 specified to be kept 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... QEMU: Terminated _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems 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.
participants (5)
-
jiazhouyang＠nudt.edu.cn -
Julia Vassiliki -
Peter Chubb -
PX -
yanshuili.lys＠gmail.com