RustMC: Extending the GenMC stateless model checker to Rust

TL;DR

RustMC tackles the challenge of exhaustively verifying concurrent Rust programs, including interactions with C/C++ via FFI. It extends GenMC by compiling Rust to LLVM IR with a customised toolchain and by introducing LLVM passes to handle Rust-specific memory intrinsics and uninitialized accesses. The approach enables exhaustive exploration of thread interleavings to detect data races and atomicity violations in both safe Rust and mixed-language code, demonstrated on real-world-style bugs. The work delivers an open-source framework that leverages GenMC’s verification engine and lays groundwork for broader Rust verification, with future plans to integrate MIXER for more complex memory-access patterns.

Abstract

RustMC is a stateless model checker that enables verification of 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 enables the automatic verification of Rust code and any C/C++ dependencies. This tool paper presents the key challenges we addressed to extend GenMC. These challenges arise from Rust's unique compilation strategy and include intercepting threading operations, handling memory intrinsics and uninitialized accesses. Through case studies adapted from real-world programs, we demonstrate RustMC's effectiveness at finding concurrency bugs stemming from unsafe Rust code, FFI calls to C/C++, and incorrect use of atomic operations.

Figures (7)

• Figure 1: A data raced caused by an external, non-thread-safe, C function.
• Figure 2: Architecture of RustMC.
• Figure 3: Uninitialised read in Rust (top) and corresponding LLVM IR (bottom).
• Figure 4: An atomicity violation in safe code, adapted from the Rand crate rand_fix_commit.
• Figure 5: Data-race in safe Rust code.