Extending the GenMC stateless model checker to verify concurrent Rust programs.
My Bachelor thesis at the Department of Computer Science, ETH Zürich, advised by Prof. Dr. Michalis Kokologiannakis.
Stateless model checkers are widely used for verifying concurrent programs, but their application to Rust has thus far been limited. This work extends GenMC, a state-of-the-art stateless model checker for concurrent C/C++ programs under weak memory models, so that it can also verify Rust programs.
Because GenMC operates on the LLVM-IR produced during compilation, the frontend adds support for LLVM-IR constructs emitted by the Rust compiler and provides custom implementations of Rust’s standard-library concurrency APIs so they can be intercepted by the checker. Rust tests were run and cross-checked against the equivalent C programs, and as a case study several concurrent data structures from Crossbeam, a popular open-source Rust crate, were verified.
The full write-up, including the approaches used to bridge the gap between the Rust and C/C++ toolchains, is available in the thesis (Kamberi, 2025).
Stateless model checkers are widely used for verifying concurrent programs, but their application to Rust has thus far been limited. Existing model checkers lack full support for aspects of Rust’s memory model, which prevents accurate verification of concurrent Rust programs. In this thesis, we extend GenMC, a state-of-the-art model checker for concurrent C/C++ programs that supports various weak memory models and is optimal in the number of executions explored, to also verify Rust programs. GenMC verifies the LLVM-IR produced during compilation of a C/C++ program. We extend it to support various constructs in LLVM-IR generated by the Rust compiler and develop approaches for overcoming the challenges we faced in doing so. We provide custom implementations of Rust’s standard library concurrency APIs so they can be used with GenMC. We successfully ran and compared a collection of tests in Rust with the corresponding output for the same test in C. As a case study, we verified various concurrent data-structures of a popular, open-source Rust crate. Our work enables the automatic verification of Rust programs and provides a great foundation for future extension to more concurrency primitives in Rust.
