I've built a simple hello for RISC-V. It runs in Spike as expected. In QEMU it doesn't run. It stops at loading the kernel in elfloader/src/common.c at the lines below: 199 printf("ELF-loading 199\n"); 200 /* Copy the data. */ 201 unpack_elf_to_paddr(elf, dest_paddr); I'd really like to use QEMU/GDB to debug my kernel. Can anyone shed some light on what's happening here? The failed output from QEMU looks like this: user@user-KVM:/mnt/data/femur/build$ qemu-system-riscv64 --machine spike --nographic --bios images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 The output from spike is the same but complete: ser@user-KVM:/mnt/data/femur/build$ /mnt/data/rocket-tools/bin/spike images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 ELF-loading image 'hello' paddr=[c0027000..c013afff] vaddr=[10000..123fff] virt_entry=10216 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 Jumping to kernel-image entry point... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc0bffd8a00 "rootserver" halting...Power off
Hi Jeremy, Running seL4 in QEMU, you should use the following command, $> qemu-system-riscv64 -machine spike -cpu rv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/hello-image-riscv-spike Making sure you use QEMU > v4.2.0 - Siwei ________________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Porter, Jeremy <porter.188@buckeyemail.osu.edu> Sent: Friday, 13 November 2020 4:25 AM To: devel@sel4.systems Subject: [seL4] QEMU vs Spike on RISC-V Debugging I've built a simple hello for RISC-V. It runs in Spike as expected. In QEMU it doesn't run. It stops at loading the kernel in elfloader/src/common.c at the lines below: 199 printf("ELF-loading 199\n"); 200 /* Copy the data. */ 201 unpack_elf_to_paddr(elf, dest_paddr); I'd really like to use QEMU/GDB to debug my kernel. Can anyone shed some light on what's happening here? The failed output from QEMU looks like this: user@user-KVM:/mnt/data/femur/build$ qemu-system-riscv64 --machine spike --nographic --bios images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 The output from spike is the same but complete: ser@user-KVM:/mnt/data/femur/build$ /mnt/data/rocket-tools/bin/spike images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 ELF-loading image 'hello' paddr=[c0027000..c013afff] vaddr=[10000..123fff] virt_entry=10216 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 Jumping to kernel-image entry point... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc0bffd8a00 "rootserver" halting...Power off _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
OK, this worked perfectly. Thank you! Is there a reason we need so much memory? I've got the command you sent working with -m size=1025M, but I can't go lower. I've looked at machine.c code for the platform (spike) but that seems to adjust to the size provided by hardware. ________________________________ From: Zhuang, Siwei (Data61, Kensington NSW) <Siwei.Zhuang@data61.csiro.au> Sent: Thursday, November 12, 2020 7:54 PM To: Porter, Jeremy <porter.188@buckeyemail.osu.edu>; devel@sel4.systems <devel@sel4.systems> Subject: Re: QEMU vs Spike on RISC-V Debugging Hi Jeremy, Running seL4 in QEMU, you should use the following command, $> qemu-system-riscv64 -machine spike -cpu rv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/hello-image-riscv-spike Making sure you use QEMU > v4.2.0 - Siwei ________________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Porter, Jeremy <porter.188@buckeyemail.osu.edu> Sent: Friday, 13 November 2020 4:25 AM To: devel@sel4.systems Subject: [seL4] QEMU vs Spike on RISC-V Debugging I've built a simple hello for RISC-V. It runs in Spike as expected. In QEMU it doesn't run. It stops at loading the kernel in elfloader/src/common.c at the lines below: 199 printf("ELF-loading 199\n"); 200 /* Copy the data. */ 201 unpack_elf_to_paddr(elf, dest_paddr); I'd really like to use QEMU/GDB to debug my kernel. Can anyone shed some light on what's happening here? The failed output from QEMU looks like this: user@user-KVM:/mnt/data/femur/build$ qemu-system-riscv64 --machine spike --nographic --bios images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 The output from spike is the same but complete: ser@user-KVM:/mnt/data/femur/build$ /mnt/data/rocket-tools/bin/spike images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 ELF-loading image 'hello' paddr=[c0027000..c013afff] vaddr=[10000..123fff] virt_entry=10216 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 Jumping to kernel-image entry point... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc0bffd8a00 "rootserver" halting...Power off _______________________________________________ Devel mailing list Devel@sel4.systems https://urldefense.com/v3/__https://sel4.systems/lists/listinfo/devel__;!!KG...
seL4 doesn't detect memory at runtime. The physical memory is specified in the DTS file, in this case, kernel/tools/dts/spike.dts seL4 build system extracts the memory info from this file, generates platform headers, kernel/gen_headers/plat/machine/devices_gen.h If you'd like to use smaller memory, simply modify the memory section in the DTS file. ________________________________________ From: Devel <devel-bounces@sel4.systems> on behalf of Porter, Jeremy <porter.188@buckeyemail.osu.edu> Sent: Saturday, 14 November 2020 6:57 AM To: devel@sel4.systems Subject: Re: [seL4] QEMU vs Spike on RISC-V Debugging OK, this worked perfectly. Thank you! Is there a reason we need so much memory? I've got the command you sent working with -m size=1025M, but I can't go lower. I've looked at machine.c code for the platform (spike) but that seems to adjust to the size provided by hardware.
This looks like it will work, but I'm on seL4 10.0 right now. I've not been able to get a cmake configuration that works with seL4 12.0 for RISC-V yet. I think this is the biggest hurdle now, how to get seL4 built for RISC-V with a very simple hello world project.
participants (3)
-
Porter, Jeremy -
porter.188＠osu.edu -
Zhuang, Siwei (Data61, Kensington NSW)