Saturday, June 3, 2017

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


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.


[1] started