RustMC：将 GenMC 无状态模型检查器扩展到 Rust
RustMC: Extending the GenMC stateless model checker to Rust
AI总结：
本文提出 RustMC，通过扩展 GenMC 以支持 LLVM IR 上的并发 Rust 程序验证，解决了线程操作拦截、内存内建函数和未初始化访问等挑战，并在真实案例中有效发现不安全 Rust、FFI 调用及原子操作误用导致的并发缺陷。
摘要：
RustMC 是一个无状态模型检查器，能够对并发 Rust 程序进行验证。由于 Rust 和 C/C++ 都编译为 LLVM IR，RustMC 构建在 GenMC 之上，而 GenMC 为 LLVM IR 提供了一个验证框架。这使得 Rust 代码以及任何 C/C++ 依赖项都能被自动验证。本文是一篇工具论文，介绍了我们在扩展 GenMC 过程中所解决的关键挑战。这些挑战源于 Rust 独特的编译策略，包括拦截线程操作、处理内存内建函数以及未初始化访问。通过改编自真实世界程序的案例研究，我们展示了 RustMC 在发现并发缺陷方面的有效性，这些缺陷来源于不安全的 Rust 代码、对 C/C++ 的 FFI 调用以及原子操作的不正确使用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
