Verifying real-world concurrent Rust crates (available)

Rust is a popular systems programming language which enforces memory and thread safety through compile-time safety checks [1]. While these constraints effectively prevent data races in safe Rust code, verification of concurrent Rust programs remains an ongoing challenge. Concurrency bugs may occur for a number of reasons, including atomicity violations, “unsafe” Rust code and interactions between Rust and C/C++ foreign function interface (FFI) dependencies.

RustMC [2] is a verification tool for concurrent Rust programs built on top of the GenMC verification framework [3]. GenMC targets the verification of C/C++ programs at the LLVM-IR level [4] by exhaustively exploring all potential interleavings, providing stronger correctness guarantees than conventional testing. RustMC builds on this by adding LLVM transformations and patches to GenMC’s interpreter in order to target the verification of real-world Rust crates.

This project involves applying RustMC to real-world concurrent Rust crates, diagnosing any cases where verification fails, and implementing fixes to extend the tool’s support. Fixes may range from adding support for unsupported language features to improving the tool’s handling of test setup and execution. The project offers valuable experience with Rust, LLVM, concurrency and verification tooling and would suit a student interested in software verification, low-level systems programming and compilers.

The project will be co-supervised by Dr. Dan O’Keeffe (daniel.okeeffe@rhul.ac.uk) and Dr. Julien Lange (julien.lange@rhul.ac.uk). Please feel free to contact us if you have any questions.

[1] The Rust Programming Language (interactive book): https://rust-book.cs.brown.edu/
[2] RustMC: Extending the GenMC stateless model checker to Rust https://arxiv.org/pdf/2502.06293
[3] GenMC: A Model Checker for Weak Memory Models https://plv.mpi-sws.org/genmc/cav21-paper.pdf
[4] LLVM Language Reference Manual https://llvm.org/docs/LangRef.html