RISCV support in Microkit

[podhrmic]

Hi, following up on #15 I am looking into adding support for RISCV, specifically for the Polarfire Icicle kit. Besides the obvious changes in build_sdk.py and makefiles (mostly replace the hardcoded arm toolchain with something configurable), what else do you expect to be the major pain points?

The loader seems to provide a good number of utilities (enable/disable mmu and such), but it is not clear how much are these used. Not sure how this changes for RISCV (the existing platforms don't support virtualization for example).

Some of this could be provided by OpenSbi, and in fact that is what the riscv version of the seL4 tests suite uses.

The same goes for the monitor - besides some of the debug prints it looks fairly generic, unless I am missing something?

[Ivan-Velickovic]

I’ve added support for RISC-V on my fork of seL4CP, I should be able to open a PR for it within a couple of weeks (there’s one remaining issue with it right now that would prevent you from just using my changes in the meantime however, I’ll try fix this ASAP)

[podhrmic]

@Ivan-Velickovic oh nice! Would you be able to share even the unpolished version of your fork? Maybe I can help push it over the finish line if you would like.

[podhrmic]

@Ivan-Velickovic have you been able to make any progress on the RISCV port? I am very curious, because we would like to run sel4cp on Polarfire Icicle Kit (multicore RISCV board), which I think might be interesting for others as well.

[podhrmic]

@Ivan-Velickovic any news about the RISCV support?

[Ivan-Velickovic]

Here is the link to my development branch: https://github.com/Ivan-Velickovic/sel4cp/tree/dev. It should work for the Polarfire on single-core but I don't have a Polarfire so I can't test it myself unfortunately. Note that currently loading with the seL4CP image as an OpenSBI FW_PAYLOAD will not work, I'm working on a fix now though. I'm in the middle of adding 32-bit RISC-V support as well. Multi-core will come later.

I should give a warning though, as this is a development branch, things are not yet stable and as high-quality as they should be.

[podhrmic]

Thanks for the update! Do you have instructions for running it on Polarfire? I see you have an example for Spike, but not for Polarfire. I have a board so can give it a try.

[podhrmic]

@Ivan-Velickovic could you please point me to the Polarfire example?

[Ivan-Velickovic]

@Ivan-Velickovic could you please point me to the Polarfire example?

There is no Polarfire example because I don't have one to test on (sorry perhaps I should have been clearer in that the state of the RISC-V support should be enough that if you did a platform port to the Polarfire that it should work).

[Ivan-Velickovic]

@Ivan-Velickovic could you please point me to the Polarfire example?

Some details that may be of use in case you do try to do a port:

Add the Polarfire configuration to the list of board support in build_sdk.py. That should be everything actually since the loader just uses OpenSBI for UART output. I believe from a previous post on the seL4 Discourse forum that the boot process of the Polarfire has OpenSBI first then U-Boot then seL4/user-space? If so then you should be able to follow the same example as the Star64 here https://github.com/Ivan-Velickovic/sel4cp/blob/dev/example/star64/hello/Makefile. There will be a raw image produced so in U-Boot you want to use go ${loadaddr} where loadaddr is the address the image is loaded in U-Boot and matches the loader_link_address specified in build_sdk.py.

Hope this helps.

[podhrmic]

@nspin @Ivan-Velickovic what would it take to run the rust crates on RISCV? I see that you already have RISCV target file which is great, but looks like Ivan's changes need to be merged to upstream sel4cp first?

[nspin]

@nspin @Ivan-Velickovic what would it take to run the rust crates on RISCV? I see that you already have RISCV target file which is great, but looks like Ivan's changes need to be merged to upstream sel4cp first?

On the Rust side, it shouldn't take much! The sel4 crate already supports riscv64, though that support hasn't been thoroughly tested yet. riscv64 support in the sel4-sys crate, however, has been thoroughly tested. riscv64 support would still have to be added to the sel4-runtime-common crate. Just an entry assembly fragment, really.

[podhrmic]

I would be happy to give it a try, but you can to point me to the reference assembly file?

[nspin]

This is the fragment I had in mind:

https://github.com/coliasgroup/rust-seL4/blob/d9777945ff261a40dbe35d8902377c073ad76e18/crates/sel4-runtime-common/src/start.rs#L37

This module would also need some attention:

https://github.com/coliasgroup/rust-seL4/blob/d9777945ff261a40dbe35d8902377c073ad76e18/crates/sel4-reserve-tls-on-stack/src/lib.rs

Fleshing out riscv64 is high on my to-do list, but I'm not sure exactly when I'll get around to it. Feel free to start working on it, and let me know if I can help!

[podhrmic]

@Ivan-Velickovic I see that you have a number of RISCV boards supported in your fork - but not any associated PR. Is there anything that needs to be resolved before you can merge those examples into upstream?

[Ivan-Velickovic]

@Ivan-Velickovic I see that you have a number of RISCV boards supported in your fork - but not any associated PR. Is there anything that needs to be resolved before you can merge those examples into upstream?

Yes, the RISC-V support needs to be merged first but these changes are fairly invasive so I'm not going to make a PR for it until CapDL support is merged.

[Ivan-Velickovic]

A lot of the feature changes described in the roadmap will not be upstreamed until CapDL support is. I want to get that out of the way first since it affects almost everything else.

[podhrmic]

@Ivan-Velickovic I am running into an error trying to build your version of SDK with RISCV support:

• microkit branch: https://github.com/Ivan-Velickovic/microkit -> dev
• seL4 branch: https://github.com/Ivan-Velickovic/seL4 -> microkit-dev
• RISCV toolchain: riscv64-unknown-elf-toolchain-10.2.0 as described in the README

The error I get after running $ ./pyenv/bin/python build_sdk.py --sel4=./seL4/:

make: Entering directory '/home/mpodhradsky/Workspace/CPS/SEL4/microkit/loader'
riscv64-unknown-elf-gcc -c -std=gnu11 -g3 -nostdlib -ffreestanding -DBOARD_qemu_riscv_virt -DNUM_CPUS=1 -DARCH_riscv64 -Wall -Werror -mcmodel=medany -march=rv64imac -mabi=lp64 src/riscv/loader.c -o /home/mpodhradsky/Workspace/CPS/SEL4/microkit/build/qemu_riscv_virt/release/loader/loader.o
src/riscv/loader.c:7:10: fatal error: strings.h: No such file or directory
    7 | #include <strings.h>
      |          ^~~~~~~~~~~
compilation terminated.
make: *** [Makefile:101: /home/mpodhradsky/Workspace/CPS/SEL4/microkit/build/qemu_riscv_virt/release/loader/loader.o] Error 1
make: Leaving directory '/home/mpodhradsky/Workspace/CPS/SEL4/microkit/loader'
Traceback (most recent call last):
  File "/home/mpodhradsky/Workspace/CPS/SEL4/microkit/build_sdk.py", line 872, in <module>
    main()
  File "/home/mpodhradsky/Workspace/CPS/SEL4/microkit/build_sdk.py", line 841, in main
    build_elf_component("loader", root_dir, build_dir, board, config, loader_defines)
  File "/home/mpodhradsky/Workspace/CPS/SEL4/microkit/build_sdk.py", line 658, in build_elf_component
    raise Exception(
Exception: Error building: loader for board: qemu_riscv_virt config: release

Manually adding the proper include directory to the loader makefile fixed this problem:

$ git diff
diff --git a/loader/Makefile b/loader/Makefile
index e70ab88..5bdc3f2 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -51,7 +51,7 @@ ifeq ($(ARCH),aarch64)
 else ifeq ($(ARCH),riscv64)
        MARCH := rv64imac
        MABI := lp64
-       C_FLAGS_ARCH := -mcmodel=medany -march=$(MARCH) -mabi=$(MABI)
+       C_FLAGS_ARCH := -mcmodel=medany -march=$(MARCH) -mabi=$(MABI) -I/opt/riscv64-unknown-elf-toolchain-10.2.0-2020.12.8-x86_64-linux-ubuntu14/riscv64-unknown-elf/include
        ASM_CPP_FLAGS_ARCH := -march=$(MARCH) -mabi=$(MABI) -DFIRST_HART_ID=$(FIRST_HART_ID)
        ASM_FLAGS_ARCH := -march=$(MARCH) -mabi=$(MABI)
 else ifeq ($(ARCH),riscv32)

Not sure if there is a better way to fix the include path?

[Ivan-Velickovic]

Can you run which riscv64-unknown-elf-gcc and report the path?

[podhrmic]

Good point! Looks like I had the path messed up (a system riscv package colliding with the sifive riscv package). I believe this can be closed now, thanks for the pointer!