2022/12/06 by Kaiwen Zhang, Guanjun Liu, Zhang, Kaiwen +1
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Petri Nets in System Modeling #Programming Languages (cs.PL) #Software Engineering (cs.SE) #Software System Performance and Reliability
paper · pdf · doi:10.48550/arxiv.2212.02754
openalex publication_date 2022/12/06 · openalex created_date 2022/12/22 · openalex updated_date 2026/07/28
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.