RustMC: Extending the GenMC stateless model checker to Rust

TL;DR

RustMC is a novel tool that extends the GenMC model checker to verify concurrent Rust programs by addressing Rust-specific compilation challenges, enabling detection of concurrency bugs in real-world applications.

Contribution

This paper introduces RustMC, the first stateless model checker tailored for Rust, overcoming unique compilation and concurrency challenges to verify Rust and C/C++ code dependencies.

Findings

Successfully verified real-world Rust programs for concurrency bugs.

Detected unsafe Rust code and incorrect atomic operations.

Demonstrated effectiveness in handling FFI calls to C/C++.

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.