Wednesday, July 18, 2018

New sel4test and sel4bench releases supporting SiFive's Unleashed Platform

In Brief: New features:

  • A new option to run seL4 in machine mode.
  • Ported seL4 to QEMU's SiFiveU and virt platforms.
  • DTB parsing in seL4 to read and use UARTs when available.
  • Ported seL4 to run on VC707 FPGA Freedom Unleashed platform.
  • Initial Benchmarking support in seL4.
  • Initial sel4bench port that can measure IPC and trap timing.


seL4 in Machine mode

  • Enables future virtualization efforts (e.g. running Linux in S-Mode)
  • User level is not affected by this change
  • Kernel works in physical memory (doesn't use MMU or TLBs)
  • No "global" kernel mappings in this mode
  • User can use the entire virtual address space
  • This allows the seL4 to use and/or export devices (like UART) without the need to trap to riscv-pk

seL4 on SiFive/Freedom Unleashed

This platform is the same as spike with minor modifications to the memory layout in order to use 1 GiB DRAM mapped into 2-level page tables (instead of 1). It runs on:
  • QEMU's sifiveu and virt platforms.
  • Freedom Unleashed VC707 Dev Kit.
  • Boom (modified to work with Freedom SDK).

DTB Parsing of UARTs

That was quite easy to do, by just copying riscv-pk code to the initial seL4's DTB code. It follow riscv-pk behaviour of trying to find UART devices before using HTIF. It currently supports riscv-pk's UART drivers (copied):
  • SiFive's UART
  • UART16550
In machine mode, it works just fine because there's no address translation. In supervisor mode, I had to map the whole UART (1GiB-padded) address in a 1 GiB page. This is just for simplicity, future improvements would be mapping it in a 4 KiB page and/or to use HTIF for kernel and UART for user-level.

Benchmarking support in seL4

Need to add timestamp function in the kernel to read cycles. Furthermore, I added Benchmarking system calls in libsel4 to allow user levels calls. This enables both generic and utilisation benchmarking in seL4.

sel4bench port

A very basic initial port to be able to measure IPC and Hardware traps. Results for this work are shown in my previous blog post.


$repo init -u -m sel4test-18072018.xml

$repo init -u -m sel4bench-18072018.xml