Friday, June 1, 2018

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.