Page 300 - 《软件学报》2026年第5期

唐瑞泽 等: 分布式系统模型检验技术研究进展 2179

率极低, 基本不可行.
为解决上述问题, VeriSoft 提出了高效的无状态搜索算法 (efficient stateless search) [77] , 引入偏序约减 (partial-
order reduction) [92] 等技术来减少对等价执行路径的重复探索. 尽管该算法仍在形式上不保存状态, 其搜索决策实际
上利用了历史信息来约减状态空间. 由于 VeriSoft 是最早面向真实程序进行系统性状态空间探索的工具, 首次系
统化提出了无状态搜索的概念, 其定义和实现方式影响深远. 本文后续提及的“无状态搜索”均指这种结合偏序约
减的高效实现方式, 而非原始意义上的完全无历史信息的搜索算法.
VeriSoft 核心思想是, 若多个动作无依赖关系 (如不同节点上的独立操作), 则不同执行顺序最终到达的状态等
价. 例如, 若网络缓存中有发送至节点 A 和 B 的消息, 则 A 先接收或 B 先接收不会影响二者都接收消息后的最终
状态. 偏序约减通过选择性搜索 (selective search) 减少冗余探索, 即在每个状态仅搜索部分使能动作, 而非所有可
能的动作.
VeriSoft 算法 (图 4) 基于深度优先搜索, 并结合 sleep-set [93] 和 persistent-set [92] 剪枝优化. Stack 结构存储从初始
状态到当前状态的转移动作 (第 9 行和第 12 行), 用于支持撤销 (Undo) 操作 (第 13 行), 即通过重放 Stack 中的转
移动作重构先前状态. 每个状态 s 关联 Persistent 集合和 Sleep 集合: Persistent 集合 (由 Persistent_Set 函数返回)
包含被使能的部分动作, 未包含的动作与其独立, 因此仅探索 Persistent 集合可避免重复探索等价路径 (Mazurkie-
wicz trace) [94] . Sleep 集合记录已探索的独立事件组合, 作为深度优先搜索的参数 (第 11 行), 在下一次探索时排除
(第 6 行), 进一步减少等价路径的重复搜索.

1 Initialize: Stack is empty;
2 Search() {
3 DFS( );
4 }
5 DFS(set: Sleep) {
6 T = Persistent_Set () \ Sleep;
7 while T ≠ do {
8 take t out of T;
9 push( t) onto Stack;
10 Execute( t);
11 DFS({t′ ∈ Sleep | t′ and t are independent});
12 pop t from Stack;
13 Undo(t);
14 Sleep = Sleep ∪ {t};
15 }
16 }

图 4 无状态搜索算法 (引自 VeriSoft [77] )

无状态搜索算法的优势在于避免存储状态带来的问题. 相比广度优先或随机搜索, 深度优先搜索减少了无状
态搜索中高开销的回溯次数, 并结合 Stack 结构, 仅存储必要的路径信息以在回溯时重构状态, 从而降低事件存储
成本. 其缺点是无法检测状态空间中的环, 遇到环时可能导致无限递归, 可通过限制搜索深度来规避. 此外, 由于不
支持环检测, 该算法无法直接验证标准的活性 (liveness) 属性, 但可通过检查有限事件序列来近似检测特定活性属
性, 例如, 若系统未终止于某个期望状态, 则可判定为死锁.
3.2.2 状态空间约减方法
状态空间探索面临状态爆炸问题, 导致在有限时间内无法穷尽所有状态, 从而影响 DMCK 的有效性. 因此, 所
有相关研究均提出了相应的应对方案. 传统 DMCK 研究主要集中在适用于分布式系统的通用状态空间约减技术
上. 由于状态空间约减的核心在于: 约减后的探索路径是否仍能覆盖所有可能导致属性违反 (即系统缺陷) 的执行
路径, 这一能力通常被称为约减算法的 soundness [95] , 是模型检验中确保验证有效性的基础. 为便于后文讨论, 本文
将满足 soundness 要求的方法称为“可靠型约减方法”, 而不满足 soundness 要求的方法称为“不可靠型约减方法”.
可靠型 (sound) 约减方法: 可靠型约减方法包括状态去重、对称约减、偏序约减和动态接口约减, 这些方法相