sel4test/RISC-V unofficial release - priv-1.10 - spec-2.3

Major updates since 2015

• - It's now based on seL4's master (rather than experimental) branch, which means it makes use of architecture-independent verified code.
• - Instead of earlier 32-bit support, it's now based on 64-bit RISC-V.
• - Compatible with latest RISC-V priv-1.10 and user-2.2/3 specs.
• - sel4test and libraries are ported and passing 146/146 tests.
• - Tested on Spike and Rocket Chip on FPGA soft-float (also previous version worked with QEMU 1.9.1).
• - Implements seL4's fastpath support.
• - 3 page mappings are supported (Sv39: 4KiB, 2MiB and 1GiB).
• - Relies on SBI from unmodified riscv-pk/bbl to emulate M-mode (same as riscv-linux).

Work in progress

• - Upstreaming seL4/RISC-V port.
• - Multicore support.
• - Research-wise, I've been working on adding CHERI support to RISC-V (Spike) as an extension, and aiming to experiment seL4 on it.

TODO list

• - Upstream the kernel (and libraries).
• - Add debug and benchmark support.
• - Release sel4bench.
• - Port sel4-tutorial to RISC-V (Start Guide for new comers/learners).
• - External interrupt handling and work with PLIC.

Quick How to

1. Install riscv64 tools (priv-1.10)
2. Get sel4test/RISC-V (using repo, for more info see [1])
3. $repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-03062017.xml
   $repo sync 
4. $make riscv_defconfig && $make 
5. build riscv-pk/bbl with path to images/sel4test-driver-image-riscv-spike (from 4)
6.  run spike with bbl image generated from 5.

sel4test/RISC-V running on Spike

Note

This work is of my personal/independent effort (during spare-time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstreamed.

References

[1]  https://wiki.sel4.systems/Getting started