 |
| SOS running on seL4 on RISC-V |
Abstract
Following the first status update of my project (Porting seL4 to RISC-V), this post reveals more updates, most notably, the port is now mature enough to run SOS (Simple Operating System) which is recommended by the seL4 getting started guide [1] [2] to learn about seL4 programming. Given that SOS is used part of an advanced operating system course offered by UNSW and currently only runs on Sabre Lite ARM-based board, seL4 on RISC-V can be considered the second supported platform for SOS, and the first all-open-source seL4 system, providing that seL4 (and its components), RISC-V ISA, Spike simulator (and hopefully soon Rocket-Chip/lowRISC on FPGA) are all open-source.
Details
Running SOS on seL4/RISC-V platform proves that the port is continually making a steady progress, and asserting that most of seL4/RISC-V API and internals are known to work fine. As mentioned before, a seL4 microkernel port itself wouldn't be interesting without some use cases. So, rather than unit testing each seL4 function itself, I preferred to port an existing (and interesting) use-case like SOS, that's entirely dependent on the seL4 API, and heavily utilizes many of its features. This gives me a better understanding of how a real-world seL4-based application would need/act, and how the seL4 microkernel implementation should react, debugging from the very highest level of a seL4 system (applications running on SOS which in turn runs on seL4) down to the very lowest-level of RISC-V hardware implementation. So what's SOS, and what was needed to run it on the seL4/RISC-V port?
What's SOS
"simple operating system (SOS) is a server running on top of the seL4 microkernel. The SOS server is expected to provide a specified system call interface to its clients (Specified in
libs/libsos/include/sos.h)." [2] The SOS framework is described in the following figure. |
| SOS framework |
The components shown in the picture above are:
- Harware: The hardware described in our case is the RISC-V platform. Currently only the Spike simulator is supported.
- seL4 microkernel: this is the seL4 RISC-V port of the kernel (and the third port after IA-32 and ARM). It provides the functionalities needed to run our SOS project in the sort of memory management, scheduling, IPC, etc.
- SOS: a stub operating system running on top of seL4 microkernel. It's intended to be developed and enhanced by students and/or people who are interested to learn about seL4. SOS initializes a synchronous endpoint capability for its clients/applications to use for communication. Interrupts are delivered using an asynchronous endpoint (seL4 has two types of endpoint capability: synchronous and asynchronous).
- tty_test: it serves as a simple application running on top of SOS that simply prints out a hello word message.
What's needed to support running SOS
Other than the seL4 microkernel internals, almost all of the current seL4 user-level libraries had to be supported to build SOS and its applications, the following picture is captured from the high-level Kconfig file of the project.
 |
| Project Kconfig file |
To be able to build/run SOS, the following components are involved:
- seL4 microkernel, it now supports memory management capabilities, context switch, traps from user applications, and a lot (than what has been discussed here) more architecture-dependent functions were implemented.
- libseL4: This is the user-level library for applications to deal with seL4 microkernel via system calls. It defines the format of the system calls, kernel objects definitions, user-level context and it exposes them all to the user.
- libmuslc: The C library that seL4 and its libraries depend on. It has been ported to RISC-V part of this project, and now it's working pretty fine as expected.
- libsel4muslcsys: A minimal muslc implementation for the root task to bootstrap, it provides stdio related system call handlers and it's part of the bootstrap procedure of the root task, defining the system call table and entry point for muslc-based applications.
- libplatsupport: Some platform related functions (BSP) for seL4 supported platforms. For example serial driver initialization and console driver functions for a given board are provided there. libsel4platsupport depends on it. I had to add Spike platform with very basic implementation just to get over build dependencies.
- libsel4platsupport: For RISC-V it has to be ported to provide the bootstraping and the exe entry point __sel4_start for the root task. It gets the boot frame address from the seL4 microkernel, constructs the stack vector as muslc expects, and then jumps to the normal muslc _start entry, enabling it to populate the libc environment's data-structures with its details, initializes TLS, files and stdio handlers, etc. Finally the muslc task bootstrap procedure jumps to the user's main() function, or the root task, which in our use case is SOS.
- libcpio: used by SOS to parse the cpio archive, searching for user binaries.
- libelf: This one is used by SOS to parse the ELF binaries extracted from the cpio archive. Hence SOS can read the ELF's section headers, and do the loading/mapping consequently.
- libsel4cpace: a library provided to abstract away the details of seL4 CSpace management, this library had to also be ported for RISC-V. It's used by SOS to construct tasks' CSpace.
- mapping: SOS comes with mapping.c file that's needed in conjunction with elf.c to load/map the user ELF binaries. It's ported to RISC-V and it invokes the newly provided RISC-V system calls like seL4_RISCV_Page_Map and seL4_RISCV_PageTable_Map
 |
| seL4/SOS bootstrap procedure |
What's next
Next I'll be working on 64-bit support, IRQ handling, seL4test project, and see how we can take the port to the FPGA-level. The project repos are listed below [4] [5].References
[1] Getting Started with seL4
[2] Advanced Operating Systems Course | Project: A Simple Operating System
[3] SOS framework
[4] [Github] seL4 RISC-V por
[5] [Github] seL4 project containing SOS
