Parsimonious Optimal Dynamic Partial Order Reduction

TL;DR

This paper introduces POP, a space-efficient optimal DPOR algorithm for stateless model checking of concurrent programs, reducing memory usage while maintaining exploration completeness.

Contribution

POP combines novel techniques to achieve polynomial space complexity in optimal DPOR, improving scalability and efficiency over existing methods.

Findings

POP significantly reduces memory consumption compared to prior algorithms.

POP scales better on programs with long executions.

Implementation in Nidhugg demonstrates practical efficiency improvements.

Abstract

Stateless model checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to TruSt, a related optimal DPOR algorithm that represents executions as graphs, shows that POP's implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt's on programs with long executions.