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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Trading Space for Simplicity in Stateless Model Checking

  • Parosh Aziz Abdulla,
  • Mohamed Faouzi Atig,
  • Sarbojit Das,
  • Bengt Jonsson,
  • Konstantinos Sagonas

摘要

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.