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  is the first recommended entry point for people who want to learn and get hands-on experience on seL4 and its libraries. This repo  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|
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 email@example.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-24062017.xml