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?