一句话：提出 Psym，用细粒度规范配置表示在符号探索中同时避免状态、交错及状态更新计算的冗余，提升分布式系统验证可扩展性。
分布式系统验证因消息与故障的大量交错而面临状态空间爆炸。已有方法通常通过状态哈希、偏序归约等避免冗余状态和冗余交错，但转移更新状态时的冗余计算仍未被消除。本文提出一种高效符号探索方法，采用新颖、细粒度且规范的分布式系统配置（状态）表示，在探索过程中动态识别并避免这些冗余；该探索器还提供与状态空间抽象、偏序归约及其他交错归约兼容的接口。作者实现工具 Psym，实验表明其性能优于先进探索工具，可验证多种常见分布式协议，并扩展到多个真实工业案例。
Verification of distributed systems using systematic exploration is daunting because of the many possible interleavings of messages and failures. When faced with this scalability challenge, existing approaches have traditionally mitigated state space explosion by avoiding exploration of redundant states (e.g., via state hashing) and redundant interleavings of transitions (e.g., via partial-order reductions). In this paper, we present an efficient symbolic exploration method that not only avoids redundancies in states and interleavings, but additionally avoids redundant computations that are performed during updates to states on transitions. Our symbolic explorer leverages a novel, fine-grained, canonical representation of distributed system configurations (states) to identify opportunities for avoiding such redundancies on-the-fly. The explorer also includes an interface that is compatible with abstractions for state-space reduction and with partial-order and other reductions for avoiding redundant interleavings. We implement our approach in the tool Psym and empirically demonstrate that it outperforms a state-of-the-art exploration tool, can successfully verify many common distributed protocols, and can scale to multiple real-world industrial case studies across
@article{paperbot1935,
title = {Psym: Efficient Symbolic Exploration of Distributed Systems},
author = {Lauren Pick and Ankush Desai and Aarti Gupta},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591247}
}