Parsimonious Optimal Dynamic Partial Order Reduction
arxiv(2024)
摘要
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 (POP) DPOR, 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 a related optimal DPOR
algorithm for a different representation of concurrent executions as graphs
shows that POP has comparable worst-case performance for smaller benchmarks and
outperforms the other one for larger programs.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要