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
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
