RustMC: Automated Verification of Real-World Concurrent Rust

RustMC is a stateless model checker that targets push-button verification of unmodified concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This allows verification of Rust code and any foreign function dependencies. In this tool paper we present key implementation challenges, use-cases, and an empirical evaluation of RustMC. The challenges include intercepting threading operations, promoting memory intrinsics, and handling uninitialised accesses, all stemming from Rust’s unique compilation strategy. Case studies adapted from real-world programs show RustMC finds concurrency bugs in unsafe Rust code, FFI calls to C/C++, and atomic operations. We evaluate our tool’s functionality on the Loom model checker test suite and a set of production-level Rust concurrent data structures.