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
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)
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
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)