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.