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.
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 UnleashedThis 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 UARTsThat 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
Benchmarking support in seL4Need 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 portA 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