The thesis topics listed here are available to strong undergraduate students. They are mostly associated with research projects and generally quite challenging; many topics have the potential to lead to a publication, and in average we get about one paper a year from the work of one (or more) undergraduate thesis students. Students who are not aiming for excellence are in the wrong place here.
Note that the below list is constantly updated, new topics are added as we identify them as work on various research projects proceeds. Topics marked are recent additions.
We are generally looking for honours candidates, or students with outstanding performance in operating systems. Specifically we guarantee a thesis topic to any student who has obtained a HD grade in UNSW's Operating Systems or Advanced Operating Systems course, no matter what their other grades are!
CakeML is a functional programming language with a certifying compiler, i.e. the compiler output is provably correct. Pancake is a slimmed-down version of CakeML that uses parts of CakeML's compilation framework. This thesis is to explore the usability (or requirements on) of Pancake as a systems language, specifically for writing high-performance device drivers, file systems and network stacks. Requirements on such a language is predictability (specifically no garbage collector), clear, easy-understandable mapping to binary code, and the ability to access hardware registers.
Jointly supervised with Johannes Åman Pohjola
While IPC and Notifications are highly optimised in seL4, the corresponding interrupt-delivery and exception handling operations are less so. Analyse the performance of the present IRQ and exception delivery operations and compare to the corresponding IPC and signalling operations. Develop highly optimised implementations.
Jointly supervised with Kevin Elphinstone
Develop a sampling-based profiling framework for seL4 user-level code, taking inspiration from (and re-using appropriate parts of) Linux gprof. The aim is to have a framework that lets developers easily identify low-hanging fruit for optimisation.
Jointly supervised with Peter Chubb
Investigate the design of high-performance I/O stacks for seL4 (network and persistent storage). Starting with the existing seL4 device driver framework, investigate the suitability of its driver and IP-stack interfaces, identify bottlenecks and suggest and evaluate improvements.
Specifically, perform detailed evaluation of overheads using PMU and tracing and compare to a Linux baseline, as well as pure seL4 system calls. The aim is to demonstrate a system consisting of web server, IP stack and Ethernet driver in separate address space with latencies, throughput and per-packet processing cost within 10% of the Linux baseline. Extra points for beating Linux.
Jointly supervised with Peter Chubb
IPC on single-core seL4 is highly optimised. On multicore, IPC should only be used intra-core, and that case should ideally be no slower than single-core. In particular, concurrent IPCs running on different cores should not interfere. In practice, IPC operates inside the kernel lock, which leads to artificial contention (and thus performance degradation) and slows down even the uncontented case.
This project is to investigate the changes needed to take the IPC fastpath outside the kernel lock, and optimise and evaluate performance. Of particular concern are the exact conditions under which IPC can be performed outside the lock, and what is needed to ensure this is safe, considering that cross-core IPC remains a valid operation (which would have to be locked, of course). The design and implementation must be discussed with verification exterts to ensure that verifying the kernel remains feasible.
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).
Most commercial protected-mode real-time OSes (RTOSes) are “fully preemptible” (in reality they are mostly preemptible, with non-preemptible critical sections). In contrast, seL4 is by design non-preemptible, but uses an incremental consistency design that allows supsending and restarting long-running operations if interrupts are pending. This design leads to reasonable worst-case interrupt latencies.
This thesis is to explore the performance limits of the non-preemptable approach, and compare it to the mostly-preeemptable one. Specifically, it is to investigate what iterrrupt latencies could be achieved in seL4 if there were no verification-provided constraints on the design and implementation, and the API could be simplified as needed. The features that must be kept are capability-based protection and the present scheduling model. Then compare this to a kernel that runs with interrupts enabled as much as possible, and uses interrupt-protected critical sections where possible. This investigation is initially to be performend in a uniprocessor context, extending it to multicore is a bonus.
The thesis will perform a theoretical analysis of what an optimal non-preemptible system system would look like, and long the biggest non-preemptible sections of the mostly-preemptible system would be. This should lead to a on-paper comparison of the performance limits of the two approaches. This will be complemented by an experimental part, where the existing seL4 code base is (possibly drastically) simplified to demonstrate the two approaches, and perform best-case and worst-case latency measurements.
This topic requires a very good understanding of OS implementation trade-offs and the effect of hardware. It also requires strong systems-programming skills. A convincing execution should lead to publishable results.
I will not take on students who have not shown a convincing performance in COMP3231 ``Operating Systems''. I normally expect students to have done COMP9242 ``Advanced Operating Systems'', although I make exceptions in special cases.
Most topics can lead to publications.
Contact the relevant supervisor.
Note for OS/FM related topics: We promise a thesis topic to every interested student who has obtained a HD grade in COMP3231/COMP9201 Operating Systems or COMP9242 Advanced Operating Systems. If necessary we will define additional topics to match demand.
We will not turn down any students doing exceptionally well in OS courses. However, this does not mean that an HD in OS or Advanced OS is a prerequisite for doing a thesis with me. Interested students with lower OS marks are welcome to talk to me if they feel they can convince me that they will be able to perform well in an OS thesis.
Keep in mind that these topics are all research issues and generally at the level of Honours Theses. They are not suitable for marginal students or students with a weak understanding of operating systems. We expect you to know your OS before you start.
Undergraduate thesis topics are also suitable for coursework Master's projects. Same conditions apply: You must have a pretty good track record in OS courses for OS and FM related topics.