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

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

并依赖不可靠约减策略加速缺陷发现. SAMC 识别到崩溃事件可能产生两类影响: 1) 全局影响 (predicate global
impact, pg), 即若节点 X 的崩溃会导致节点 N 向其他节点发送消息, 则 X 的崩溃对 N 产生全局影响; 2) 局部影响
(predicate local impact, pl), 即若节点 X 的崩溃不会导致节点 N 进一步发送消息, 则 X 的崩溃仅对 N 产生局部影
响. 基于此, SAMC 定义崩溃事件与消息的独立性: 若崩溃事件会产生全局影响 (pg), 则需与所有消息重排序, 存在
依赖关系; 若仅产生局部影响 (pl), 则与其他消息独立, 无需重排序. CMI 特别适用于基于 quorum 机制的容错分布
式系统. 用户可通过 #follower >= majority 建模 pl, 反转条件则可用于建模 pg.
FlyMC [67] 将这些独立性策略进一步推广为更广义的事件独立性, 包括同一节点上更新不同变量的消息之间的
独立性, 以及与崩溃事件相关的独立性. 在分布式协议中, 多个协议或模块可能同时运行, 导致同一节点可能接收
并处理属于不同协议的消息. 例如, ZooKeeper 的 Zab 协议 [6,10] 同时包含原子广播协议和选主协议, 相关消息仅修
改各自协议中的变量, 因此彼此独立. 为支持此类优化, FlyMC 设计了一套机制, 允许开发者标注不相互影响的消
息, 并利用静态分析自动转换为系统语义信息模型.
具体而言, FlyMC 通过静态分析维护 readSet 和 updateSet, 用于判断消息是否独立. 若两条消息处理的 readSet
和 updateSet 变量无交集, 则它们独立. 一个特殊规则是, 若两条消息的 updateSet 变量完全相同, 且所有变量的变
更方式均为 +1 或−1, 则它们仍然独立. 这种模式在分布式协议中常见, 例如 ack++ 统计确认数. 对于崩溃事件,
FlyMC 将其对其他节点的影响抽象为 updateSet 变量的变更. 例如, 在集群中, 若一个跟随者节点崩溃, 领导者维护
的 liveNodes 变量减少 1 (liveNodes– –), 则该跟随者崩溃事件的 updateSet 包含领导者 liveNodes 变量.
在 SAMC 和 FlyMC 之前, 一些研究已开始利用系统语义信息进行状态约减 [59,75] , 然而, 这些工作针对的是编
程语言实现的分布式协议, 而非 ZooKeeper 等工业级分布式系统. 例如, MP-Basset [59] 主要针对基于消息通信的容
错分布式协议 (如 Paxos) 进行模型检验优化. 这类协议的典型特征是接收多条消息、修改状态并向网络发送消息,
而一次状态更新通常需要多个消息共同触发. 例如, 在 Paxos 共识协议中, 提案者需等待大多数 (quorum) 接受者
的响应才能进行状态转移.
基于这一观察, MP-Basset 提出了 quorum transition 概念, 在单次状态转移中同时处理多个消息, 从而跳过中
间状态, 避免传统方法因逐条处理消息而导致的状态爆炸. 为支持此机制, MP-Basset 在消息传递模型中引入
quorum transition, 并设计了 MP 语言用于建模此类语义. MP 语言提供 @message 注解标记消息处理的状态转移函
数, 并使用 @guard 注解定义执行前需满足的条件 (如收到足够数量的消息). 此外, MP-Basset 采用 transition refinement
(转移精化) 技术调整状态转移粒度, quorum transition 是 transition refinement 的特例, 使偏序约减技术能够利用精
化后的独立事件, 从而优化状态空间. 实验表明, MP-Basset 最大减少了 92% 的内存开销和 85% 的时间消耗. 本质
上, 该方法利用的独立性是 SAMC 和 FlyMC 所描述的同一节点内消息独立性的特例.
MP-Basset 的后续研究进一步提出了 LPOR (local partial-order reduction) 框架 [75] , 基于静态偏序约减优化领域
相关等价状态空间. LPOR 允许开发者将系统语义编码为 Can-Enable 关系和 Dependency 关系, 以捕捉消息传递系
统中的事件依赖性. 实验表明, LPOR 在验证复杂协议时可实现高达 94% 的状态空间约减. 然而, 该方法主要聚焦
于理论研究, 在真实分布式系统环境中的模型检验应用仍然存在挑战.
4.2.2 对称性约减
对称性约减技术在传统的有状态搜索中被广泛应用 [96,106] . 分布式系统具有大量对称性, 例如节点角色的对称
性. 然而, 在 SAMC [11] 之前, 较少有 DMCK 利用对称性约减. 这主要是因为 DMCK 早期研究更侧重于提高工具的
有效性, 而能够验证真实分布式系统的 DMCK 采用无状态设计. 传统对称性约减通常依赖于有状态搜索中的状态
标准化, 以消除重复状态, 而在无状态搜索中直接应用较为困难.
SAMC 定义了崩溃恢复对称性 (crash recovery symmetry, CRS) 和重启同步对称性 (reboot synchronization
symmetry, RSS), 两者原理相似, 这里以崩溃恢复对称性为例. DMCK 在原理上需要遍历所有可能的消息组合, 而
崩溃事件是由 DMCK 主动注入的, 因此可以减少不必要的注入. 例如, 在一个包含 4 个节点的分布式系统中, n1–n3
均为跟随者 (follower), n4 为领导者 (leader). 如果 n1–n3 中任意一个节点崩溃, 系统的恢复行为相同, 则仅需注入
一次崩溃事件.