Saturday, June 24, 2017

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

1 comment:

  1. Hi

    I am trying to replicate your work on seL4 by building "seL4 tests" for "Spike" platform on Ubuntu 18.04.3 LTS, a 64-bit system.

    First of all, I was able to build RISC-V tools with "build.sh" after manually installing "riscv-gnu-toolchain" from GitHub as well as additional python modules (future, ply, protobuf). I then kicked of "../init-build.sh -DPLATFORM=spike -DRISCV64=TRUE -DSIMULATION=1" from local build directory.

    After that, however, "ninja" command complained about "undefined reference to `__nedf2'". I understand there is no FPU support in "Spike" platform so a need for "soft-float" module. Where should I specify "-lsoft-fp"?

    Any suggestions?

    Thanks,


    Jacob (jacobyu2018@gmail.com)

    ReplyDelete