一句话：首个可靠、完备且最优地结合对称归约与偏序归约的无状态模型检测器，并引入实现内部幂等操作对称性。
对称归约（SR）与偏序归约（POR）分别利用对称线程置换和独立指令重排来缩减模型检测的探索空间，但二者的结合在无状态模型检测中仍是开放问题。本文提出 SPORE，首个以可靠、完备且最优方式同时结合 SR 与 POR 的无状态模型检测器。SPORE 不仅能利用客户端程序自身的对称性，还能利用底层实现中的内部对称性，即作者新提出的幂等操作对称概念。实验表明，SPORE 探索的执行数远少于仅采用 SR 或 POR 的工具，显著推进了该方向的最新水平。
Symmetry reduction (SR) and partial order reduction (POR) aim to scale up model checking by exploiting the underlying program structure: SR avoids exploring executions equivalent up to some permutation of symmetric threads, while POR avoids exploring executions equivalent up to reordering of independent instructions. While both SR and POR have been well studied individually, their combination in the context of stateless model checking has remained an open problem. In this paper, we present Spore, the first stateless model checker that combines SR and POR in a sound, complete and optimal manner. Spore can leverage both symmetries in the client program itself, but also internal symmetries in the underlying implementation (i.e., idempotent operations), a novel symmetry notion we introduce in this paper. Our experiments confirm that Spore explores drastically fewer executions than tools that solely employ SR/POR, thereby greatly advancing the state-of-the-art. CCS Concepts: • Theory of computation → Concurrency; Verification by model checking .
@article{KokologiannakisMV24,
title = {SPORE: Combining Symmetry and Partial Order Reduction},
author = {Michalis Kokologiannakis and Iason Marmanis and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656449}
}