[Update] seL4/RISC-V SMP support | seL4/RISC-V Tutorials Release

Updates (since 03062017)

 

A new unofficial 24062017 release of seL4, libraries and seL4 Tutorials.

• SMP support, tested on Spike with 2 - 9 cores:
• seL4 is using a big kernel lock.
• Only reschedule IPI (set affinity) is provided.
• Relying on SBI to do other remote operations.
• SBI doesn't provide VADDR-> ASID -> HART operation.
• Using tp register to hold per-core IPC buffer addresses.
• Ported seL4-tutorias to RISC-V. This means:
• People can learn more about both seL4/RISC-V doing the tutorials.
• Lack of RISC-V/Spike user-level timer (or another S-timer) is an issue. seL4 (being a microkernel) is not supposed to provide a timer API, rather, user-level apps should have their own HW timer and device drivers.
• More tests are passing on sel4test now after:
• SMP support.
• Re-adding a supervisor timer (for seL4 scheduling).
• [154/154] Tests pass (8 more tests pass after multicore and timer support).
• All libraries, kernel are rebased to latest seL4's revisions.

seL4 Tutorials 

 

sel4-tutorials [1] is the first recommended entry point for people who want to learn and get hands-on experience on seL4 and its libraries.  This repo [1] contains slides, docs and code tutorials with commented instructions and tasks that take you from writing a seL4 hello world application to doing IPC in a multithreading environment, now on RISC-V.

hello-3 exercise showing 2 threads doing IPC communication

 [1] https://github.com/heshamelmatary/sel4-tutorials/tree/RISCVUnofficialRelease-24062017

seL4test

 

seL4test is a comprehensive unit and functional testing suite for seL4 and can be useful when porting to new platforms or adding new features.

It can be used as a reference how to develop a big project on seL4. A new riscv_smp_defconfig config file for RISC-V is added to test SMP support. Instructions how to run it are provided in this blog post.

For this release that contains SMP, use:

$repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-24062017.xml

Note

 

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

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