seL4 / camkes-vm-linux

Other
4 stars 13 forks source link

Can I run Linux/seL4 on top of risc-v? #7

Closed mpolitzer closed 3 years ago

mpolitzer commented 3 years ago

After going through the camkes-vm-linux tutorial on sel4-tutorials, I noticed that risc-v was not an option. Is it or will it be supported? Also, this seems to require vt-x support on x86, will it require hypervisor support as well on risc-v?

gernotheiser commented 3 years ago

virtualisation extensions for RISC-V are still in draft form, and I'm not sure there is any hardware out that implements them. @yyshen is tracking support for the draft virtualisaiton extensions in a branch

yyshen commented 3 years ago

@mpolitzer Here is the manifest [https://github.com/SEL4PROJ/sel4-riscv-vmm-manifest] for the experimental riscv hypervisor extension support.

mpolitzer commented 3 years ago

thanks, I'll have a look at it.

jetshaw00 commented 2 years ago

@yyshen when i tested the repo [https://github.com/SEL4PROJ/sel4-riscv-vmm-manifest], It looks like the VM is not up. Did I do something wrong? my qemu version is : qemu-system-riscv64 --version QEMU emulator version 5.2.0 (Debian 1:5.2+dfsg-11+deb11u1) Copyright (c) 2003-2020 Fabrice Bellard and the QEMU Project developers

Init local IRQ
Bootstrapping kernel
Initializing PLIC...
available phys memory regions: 1
  [80200000..17ff00000]
reserved virt address space regions: 3
  [ffffffc084000000..ffffffc084026000]
  [ffffffc084026000..ffffffc08402656d]
  [ffffffc084027000..ffffffc085782000]
Booting all finished, dropped to user space
Caught cap fault in send phase at address 0
while trying to handle:
vm fault on code at address 0x1a4c8 with status 0x14
in thread 0xffffffc17f815200 "rootserver" at address 0x1a4ca
With stack:
0x0: INVALID
0x8: INVALID
0x10: INVALID
0x18: INVALID
0x20: INVALID
0x28: INVALID
0x30: INVALID
0x38: INVALID
0x40: INVALID
0x48: INVALID
0x50: INVALID
0x58: INVALID
0x60: INVALID
0x68: INVALID
0x70: INVALID
0x78: INVALID
Ivan-Velickovic commented 2 years ago

Hi @jetshaw00 I believe I know what is wrong, but first could you please open a separate issue here: https://github.com/SEL4PROJ/sel4_riscv_vmm/, if you could also include the commands you ran to get to this output that would be helpful.