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.

Details:

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.

Links

$repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git -m sel4test-18072018.xml


$repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git -m sel4bench-18072018.xml