Petri Nets-based Methods on Automatically Detecting for Concurrency Bugs in Rust Programs

TL;DR

This paper introduces a Petri net-based approach for efficiently and accurately detecting concurrency bugs in Rust programs, overcoming limitations of static and dynamic analysis methods.

Contribution

It presents a novel Petri net modeling technique for Rust concurrency bugs, integrating syntax-preserving transformation, semantics-preserving state compression, and efficient reachability analysis.

Findings

Reduces false positives by 35.7% compared to LockBud.

Reduces false negatives by 28.3% compared to LockBud.

Achieves 100% faster verification speed than Miri.

Abstract

Rust's memory safety guarantees, notably ownership and lifetime systems, have driven its widespread adoption. Concurrency bugs still occur in Rust programs, and existing detection approaches exhibit significant limitations: static analyzers suffer from context insensitivity and high false positives, while dynamic methods incur prohibitive runtime costs due to exponential path exploration. This paper presents a Petri net-based method for efficient, precise detection of Rust concurrency bugs. The method rests on three pillars: (1) A syntax-preserving program-to-Petri-net transformation tailored for target bug classes; (2) Semantics-preserving state compression via context-aware slicing; (3) Bug detection through efficient Petri net reachability analysis. The core innovation is its rigorous, control-flow-driven modeling of Rust's ownership semantics and synchronization primitives within the Petri net structure, with data operations represented as token movements. Integrated pointer analysis automates alias identification during transformation. Experiments on standard Rust concurrency benchmarks demonstrate that our method outperforms the state-of-the-art methods LockBud and Miri that are both tools of detecting concurrency bugs of Rust programs. Compared to LockBud, our approach reduces false positives by 35.7\% and false negatives by 28.3\% , which is obtained through our precise flow-sensitive pointer analysis. Compared with Miri that is a dynamic analysis tool, although Miri can obtain the same detection results, our method achieves 100% faster verification speed since our method takes a state reduce algorithm.