Dynamic Partial Order Reductions for Spinloops

Abstract

Stateless model checking (SMC) coupled with dynamic partial order reduction (DPOR) is an effective way for automatically verifying safety properties of loop-free concurrent programs. SMC, however, does not work well for programs with loops because it cannot distinguish loop iterations that make progress from ones that revisit the same state. This results in redundant exploration that dominates the verification time. We present SAVER (Spinloop-Aware Verifier), a memorymodel- agnostic SMC/DPOR extension that detects zero-net-effect spinloops and avoids redundant explorations that lead to the same local state. As confirmed by our experiments, SAVER achieves an exponential reduction in verification time and outperforms stateof- the-art tools in a variety of real-world benchmarks.