(12- or 24-unit Honours or Masters project, jointly supervised with Alwen Tiu)
Read-copy-update (RCU) is a synchronisation mechanism used pervasively throughout the Linux kernel and a recurring source of subtle race-condition bugs, with several recent kernel zero-days stemming from incorrect RCU usage. This project aims to build a formal model (potentially based on process algebra) of the guarantees the RCU API makes to its callers, and uses it to detect misuse in the code that consumes that API by model checking.
Background
RCU lets readers run concurrently with updates without locking: an updater publishes a new version of a data structure and defers reclamation of the old version until a grace period has elapsed, by which point every reader that could still observe the old version has left its read-side critical section. Its correctness rests on temporal and memory-ordering constraints that are easy to get wrong — dereferencing a pointer outside a critical section, freeing before the grace period completes, or relying on an ordering the memory model does not provide.
Formal verification of RCU has received sustained attention for over a decade, but almost entirely aimed at the implementation: Liang, McKenney, Kroening, and Melham verified Tree RCU with CBMC; Kokologiannakis and Sagonas applied stateless model checking to the same code under weak memory; and separation-logic proofs, from Tassarotti, Dreyer, and Vafeiadis to the 2025 relaxed-memory proof of a general-purpose RCU library by Jung and colleagues, establish that the RCU machinery is correct. Client code is verified only where a manual, per-structure proof has been carried out. How to check, with some automation, whether the ordinary kernel code that calls the RCU API uses it correctly is largely open — yet that is where the race conditions surfacing as kernel vulnerabilities live. Static analysers flag candidate misuses heuristically, but without a semantic model of the RCU contract they miss subtle interleavings and emit false positives.
Scope
The project will build an operational model of the RCU usage contract — read-side critical sections, grace periods, publication, and deferred reclamation — capturing what a reader may and may not observe, expressed in a process algebra or directly in a model checker’s input language. Canonical correct and buggy usage patterns (missing critical section, premature reclamation, reader/updater races) will be encoded and checked against safety properties such as “no reader accesses a reclaimed object”, using SPIN or CBMC for the sequentially consistent baseline and GenMC with the Linux-Kernel Memory Model for the weak-memory behaviour that makes these bugs hard to see. The 12-unit version delivers the contract model and a checked catalogue of misuse patterns. The 24-unit version distils this into a method that checks an abstracted fragment of RCU-using kernel code against the contract, evaluated on known RCU-related kernel bugs, and uses the model as a semantic filter over existing static-analysis warnings to cut false positives.
References
- P.E. McKenney et al., What is RCU, Fundamentally? and the RCU documentation, Linux kernel — https://docs.kernel.org/RCU/whatisRCU.html.
- L. Liang, P.E. McKenney, D. Kroening, T. Melham, Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel, DATE 2018 (arXiv:1610.03052).
- M. Kokologiannakis, K. Sagonas, Stateless Model Checking of the Linux Kernel’s Read–Copy Update (RCU), International Journal on Software Tools for Technology Transfer 21, 2019, pp. 287–306.
- J. Tassarotti, D. Dreyer, V. Vafeiadis, Verifying Read-Copy-Update in a Logic for Weak Memory, PLDI 2015, pp. 110–120.
- J. Jung, S. Park, J. Lee, J. Yeon, J. Kang, Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic, PACMPL 9 (PLDI), 2025.
- M. Kokologiannakis, V. Vafeiadis, GenMC: A Model Checker for Weak Memory Models, CAV 2021, LNCS 12759, Springer.
- J. Alglave, L. Maranget, P.E. McKenney, A. Parri, A. Stern, Frightening Small Children and Disciplining Programmers: The Linux-Kernel Memory Model, Communications of the ACM 61(11), 2018.
- G.J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.