Introduction
This year I am participating in
GSoC with a new umbrella organization called
lowRISC aiming to produce a completely open-source SoC (System-on-Chip). lowRISC is based on the new open
RISC-V ISA, designed by UC Berkeley. I'll be performing a complete RISC-V port of the new formally-verified microkernel
seL4.
Details
The project basically involves working with seL4 and RISC-V. The next section will introduce some related details about each.
RISC-V
RISC-V
is an open ISA, which is designed to help with computer
architecture education and research. It supports both 32-bit and 64-bit
modes and is powerful enough to run Linux. UC Berkeley team has
implemented this ISA (64-bit RISC-V
Rocket core) and showed off some interesting comparison between it and
ARM Cortex-A5.
 |
| 64-bit RISC-V Rocket Chip and ARM Cortex-A5 comparison [1] |
|
QEMU and Spike are the main simulators that enable running/debugging RISC-V software.
Recently,
a new draft of the RISC-V privileged ISA specification has been
released [2], which describes rich and nice features. Notably, the draft
introduces new four modes that RISC-V can run at (before that, there were only
supervisor and user modes). The four modes are user, supervisor,
hypervisor (however it's not implemented yet) and machine mode. This new
design takes the RISC-V architecture to a new level where
virtualization can be supported and easily researched.
seL4
seL4 is a new open-source L4 microkernel developed by
NICTA and now owned by
General Dynamics C4 Systems.
It gained its popularity being "
The world's first operating-system
kernel with an end-to-end proof of implementation correctness and
security enforcement is now open source." seL4 developers believe that
it's the state-of-art microkernel currently. The following figure shows
the history of microkernels in general and their implementations.
 |
| L4 microkernels history [3] |
L4
simplicity concept has been greatly achieved in seL4 given that it has
about 10K lines on C code, compared to Fiasco.OC which has 36K lines of
C/C++ code.
Currently
seL4 is ported to only two architectures: ARM and IA-32. Only the ARM
port is formally verified, and both support only 32-bit implementation,
however the 64-bit implementation is still a work in progress. The IA-32
port supports booting in multi-kernel mode unlike the ARM port.
seL4
microkernel itself wouldn't be of much interest without user-land
applications and libraries. There are many libraries and projects that
build on seL4 microkernel:
-
verification, the seL4 proofs.
-
seL4test, a test suite for seL4,
including a Library OS layer.
-
CAmkES, a component architecture for
embedded systems based on seL4. See the
CAmkES pages
for more documentation about CAmkES.
-
VMM a componentised virtual machine
monitor for ia32 platforms using Intel VT-X and VT-D
extensions.
-
RefOS, a
reference example of how one might build a multi-server operating
system on top of seL4. It was built as a student project.
seL4 on RISC-V
Porting seL4 to RISC-V needs a knowledge of both seL4 microkernel and RISC-V design/implementation. The project aims to perform a complete port of seL4 microkernel that enables some of the previously mentioned projects to run on it, mainly, the seL4test project that has over 120 tests asserting the seL4 microkernel API, features and behaviour. There have been some implementation trade-offs regarding the project, described below.
32-bit or 64-bit?
Both! As already mentioned, seL4 only supports 32-bit currently, on the other hand, RISC-V has been focusing on 64-bit implementations right from the start with a little support for 32-bit; UC Berkeley team has only 64-bit Rocket chip and there is no 32-bit hardware implementation so far (except for some simple educational repos). Luckily, Spike has recently supported 32-bit mode (with a new --isa flag). It will be easier to port seL4 for 32-bit architecture trying to follow/imitate ARM/IA-32 ports. 64-bit implementation would be more challenging as most of the seL4 data structures and scripts assume 32-bit environment. As there's no 32-bit hardware implementation of RISC-V yet, the port wouldn't have the chance to run on real hardware. Hence, we decided to start with 32-bit porting, make it run on Spike first, and from there we can evolve to 64-bit that can run on Spike, or Rocket Chip--hopefully both!
Rocket Chip vs. Spike and/or QEMU
Again, this is closely related to the previous trade-off of 32/64 bit implementations. So if we ended up with a 64-bit seL4 working on Spike, this can easily run on the 64-bit Rocket Chip. Rocket Chip and Spike are up-to-date with the latest ISA privileged specification, however QEMU isn't. Consequently, we chose to work with Spike as the main simulator. Spike is also more similar to the hardware implementation in that it's simulating the HTIF interface and can communicate with the shared library riscv-fesvr (front-end server) like the Rocket Chip.
Working in which mode?
The latest privileged specification introduces 4 modes that RISC-V software can run in.
Conceptually, seL4 might run in any of the three privileged modes separately, or even two or three of them simultaneously. The next figure shows the possible seL4, guest OSes and applications configurations regarding to which modes they can run at.
 |
| seL4 in which RISC-V mode trade-off |
The number of which modes to run seL4 microkernel in was narrowed down to two by the fact that there is no hypervisor implementation yet. These two modes are: machine (M-mode), and supervisor (S-mode) modes. The M-mode supports physical access control and Base-and-Bounds checking, i.e, no mapping or address translation (SV32, SV39 and SV48), only S-mode does. seL4 microkernel on the other hand expects that it would run in an address-translation-based mode, and would map its kernel image, IPC buffers, bootframe and other areas of memory during bootstrap. So we followed the current seL4 ports for now to work in S-Mode.
Loading the image(s) and mapping pages
The bare seL4 system basically consists of: 1) the kernel image, 2) applications. Current ARM and IA-32 seL4 ports differ in the way they load the kernel image and applications. Since IA-32 port can boot in multi-kernel mode, it loads the images in way similar to grub. So the kernel is the first part that takes control of the physical resources, and it loads/maps the application images itself. The ARM port behaves differently in that it archives the kernel and application images in cpio format. There's a separate elfloader tool that reads the ELF images from the cpio archive, loads it to the available physically-adjacent memory, sets up the VM environment and finally maps the ELF images according to their ELF's section VMAs. Hence, the elfloader is the first to take control of the physical resources, and then it passes control to the kernel (which works in a VM environment right from the start) with some information passed to it about the loading addresses of the kernel image itself and the user image(s). The final image for the seL4/ARM system then contains: 1) elfloader tool, 2) libelf, 3) libcpio, 4) kernel image and 5) user applications. We followed the ARM port as it's more hardware agnostic, and as a start the RISC-V wouldn't need to support multi-kernel mode.
What has been done so far
So far, the basic microkernel port can bootstrap and jump to the user image on Spike in 32-bit mode working only in S-mode.
 |
| seL4 microkernel running on Spike |
To be able to achieve this, I had to work on the following seL4 components.
- libmuslc: libelf depends on libmuslc. I performed a very basic port of musl c library to RISC-V architecture, enough to build it successfully and produce the .a library.
- libelf: This one is portable and architecture-independent. It has to be included part of the elf loading process.
- libcpio: like libelf, libcpio is also architecture-independent and is used to read the cpio archive containing the kernel image and user images.
- elfloader: This tool is developed by seL4 team for the ARM port, I had to port it to RISC-V. It has to work in M-mode and it's acting as riscv-pk, that is, any system calls from seL4 microkernel are redirected to elfloader code, which handles it and returns (apart from its main purpose which is loading the kernel/user images). elfloader currently only supports write and exit system calls (to be able to get some printf output and exit the spike simulator).
- seL4 microkernel: The project is mainly about the seL4 microkernel. The port basically followed ARM port and even a lot of code is copied from it. seL4 microkernel runs in S-mode right from the start as mentioned previously. Some architecture-level capability data structures had to be modified according to the RISC-V ISA, and the low-level RISC-V VM handling code is now implemented to map the kernel image, kernel frames, initial task and user images properly.
- Build system: The build system for seL4 projects is the Linux Kconfig/Kbuild build system. The existing Kconfig/Kbuild files had to be modified to allocate a new entry for RISC-V architecture with a new Spike platform (that runs on Spike simulator). New riscv_defconfig, project-riscv.mk, makefiles and other files were added to enable building a complete seL4/RISC-V system (elfloader, libcpio, libelf, seL4 mircokernel, user image) like in seL4tests project and other seL4 projects.
Next, I'll be working on the seL4 system calls API, timer and IRQ support and 64-bit mode. You can follow my blog to get more updates about the project as well as my github repo(s) [4] [5] [6].
References
[3] Elphinstone, Kevin, and Gernot Heiser. "From L3 to seL4 what have we learnt in 20 years of L4 microkernels?." Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. ACM, 2013.
