Trading Space for Simplicity in Stateless Model Checking
摘要
Stateless model checking is a fully automatic verification technique for concurrent programs. which 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 exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Recently, the authors of this paper presented Parsimonious-OPtimal (POP) DPOR, an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. This space consumption bound was realized due to a carefully crafted encoding of so-called sleep sets, a mechanism for preventing redundant exploration. This encoding brings some conceptual complexity to POP, which achieves good worst-case performance at the possible expense of worse average-case performance. In this paper, we present a simpler technique for managing sleep sets, which has exponential worst-case space consumption but better average-case performance. We experimentally compare these two sleep set management schemes on a range of benchmarks. The experimental results confirm that a simpler sleep set is a better choice when designing DPOR algorithms as they are faster and have similar memory consumption for average programs.