Taste of Research (ToR) Project Proposals
Applications
Applications for summer research in Trustworthy Systems for the topics below can be made through
Projects
Systems
Optimise the seL4 exception and IRQ fastpaths
Supervisor: Gernot Heiser
Abstract: The seL4 microkernel is known on the one hand for its correctness and security proofs, on the other hand for its unbeaten performance. Performance optimisations have so far targeted the critical IPC operation, and to a lesser degree signalling notification objects. While interrupt and exception handling are mapped onto notifications and IPC, respectively, they have not been optimised to the same degree.
This project is to start with analysing interrupt (IRQ) delivery performance and compare it to optimised notification signalling. Using the performance monitoring unit (PMU) and tracing in a simulator (QEMU), the student will analyse overheads and write or improve an IRQ fast path. If time permits, they will perform similar work on the exception-handling fast path.
Expected outcomes:
- report describing the analysis of the IRQ code path, comparing with notification-object signalling, and optimisations based on comparison to signalling; detailed benchmarks;
- pull request against the seL4 kernel mainline.
Evaluate and improve the seL4 device driver framework
Supervisor: Gernot Heiser
Abstract: seL4 is a strict microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. This means that I/O operations require extra context switches compared to a monolithic system such as Linux, where all those components are inside the kernel.
seL4 has a device driver framework (DDF), which specifies driver interfaces and protocols, but the DDF is so far not fully optimised. This project is to perform a detailed analysis of the DDF performance for a typical network-I/O configuration, consisting of a web server, a TCP/IP stack and an Ethernet driver, all in separate address spaces, comparing this with a corresponding Linux configuration. This analysis will identify performance bottlenecks, and their root cause as either design or implementation shortcomings. These will then be fixed, with the aim of resultant performance no more than 10% worse than Linux.
Expected outcomes:
- report describing the analysis, improvements and performance comparison to Linux;
- pull request against the DDF mainline.
The FPU as a first-class kernel object
Supervisor: Gernot Heiser
Abstract: seL4 presently treats the floating-point unit (FPU) as part of the thread context, saved in the thread control block (TCB) on preemption. As FPU state is large and most user threads do not use floating-point operation, the kernel uses lazy switching for the FPU, meaning on a context switch FPU access is disabled, resulting in an exception when a thread attempts to use it; the kernel will then save and restore the FPU state.
The drawback of this scheme is that TCBs are large (2KiB), most of which is wasted for threads not accessing the FPU. The lazy switch also introduces a covert timing channel. Both problems can be avoided my making the FPU a first-class kernel object, accessible only via presentation of an FPU capability. TCBs reduce in size (0.5-1 KiB) and timing channels can be prevented by FPU access being explicit.
Expected outcomes:
- Design of a new FPU object type for seL4, including analysis of design trade-offs and security specs
- Implementation in the seL4 kernel for AArch64 or RV64
- Performance evaluation of IPC between threads with and without FPU access and comparison to the mainline kernel
- Pull request against mainline
Optimise seL4 cold-cache / worst-case performance
Abstract: seL4 IPC operations are highly optimised for hot-cache (best case) but far less so for bad/worst-case. This project is to first determine present cold-cache performance by extending the sel4bench suite for cold caches. It is then to analyse and understand what limits present performance and is to improve it, by ensuring cache-friendly datastructure layout and other optimisations. The emphasis will be on the IPC, interrupt and exception ast paths, optionally looking at other parts of the code as well (especially slow paths).
Novelty:seL4 kernel with much improved cold-cache performance, prevention of cold-cache performance regressions.