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

IPC Performance of seL4 microkernel on RISC-V Platforms

I managed to get Freedom Unleashed U500 and Boom synthesized on VC707 FPGA Board. This motivated me to port seL4 to run there and do some microbenchmarking using sel4bench project.

Note that the seL4/RISC-V port is still a prototype, yet it can compete with ARM and x86.  The results are based on the following tools/revisions:

1. seL4 9.0.1 Release
2. sel4bench Perfomance Webpage (01/06/2018)
3. SiFive's Freedom Unleashed U500 VC707DevKit (d3c9a39)
4. SiFive's Freedom Unleashed Software Development Kit (547868)
5. Boom (Berkeley Out-of-Order RISC-V Processor): with minor modifications to run on FPGA (19e9e9a) 
6. riscv-tools --with-arch=rv64ima (8ad8d48) 
7. Vivado 2016.4 

IPC Performance on sel4bench (01/06/2018)

	Sabre I.mx6 (Cortex A9 @1GHz)	IA32 SkyLake @3.4GHz	X64 SkyLake @3.4GHz	Jetson TK1 (Cortex A15 @700MHz)	RISC-V Freedom Unleashed U500	RISC-V Boom (Default)
IPC microbenchmark, client->server	917.5	733	1480	955.5	517.9	549.7
IPC microbenchmark, server->client	306	216	776	554	551	553

Results are in cycles.