Description of field of research:
The seL4 microkernel is known not only for its comprehensive formal verification story but also for being the benchmark for microkernel IPC performance. Performance optimisations have so far targeted the critical IPC operation, and to a lesser degree signalling notification objects. While interrupt handling is mapped onto notifications, it has not yet been optimised to the same degree.
This project is to analyse 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.
School
Research Area
Operating systems
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
1) report describing the analysis of the IRQ code path, comparing with notification-object signalling, and optimisations based on comparison to signalling; detailed benchmarks
2) pull request against the seL4 kernel mainline
https://sel4.systems
https://trustworthy.systems
Honours thesis Shane Kadish
