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

2184 软件学报 2026 年第 37 卷第 5 期

框架从下至上, 底层为传统 DMCK 所研究的通用状态探索与约减机制, 包括搜索算法、动态偏序约减、对称
性约减, 以及面向不同局部组件的状态划分策略等, 构成上层利用语义策略进行状态探索的基础支撑. 中间层关注
分布式系统中的共性语义特征, 如消息传递与节点崩溃事件之间的独立性与对称性, 也包括面向容错等垂直领域
的通用语义结构. 此阶段开始系统性分析分布式容错逻辑, 并通过白盒方式收集系统内部语义信息, 结合人工建模
加以利用. 最上层则代表后续研究对系统关键模块的深入建模, 通过形式化模型和正确性规约等手段表达更细粒
度的系统特定语义, 进一步推动 DMCK 向新阶段演进.
本节重点关注中间层的语义规则设计. 此类规则可通过手工建模或结合人工标注的静态分析生成, 并反馈给
底层机制加以利用: 与独立性相关的规则由动态偏序约减机制驱动, 对称性规则由对称约减机制驱动, 垂直领域相
关规则则结合专门的领域化约减策略, 聚焦关键行为或故障模式.
4.2 系统语义感知优化技术
本节从独立性、对称性和垂直领域约减这 3 个方面展开讨论. 独立性与对称性约减主要利用分布式系统中消
息与崩溃的语义信息去除等价状态或路径, 而垂直领域约减针对特定分布式系统的领域特性聚焦特定状态空间,
如图 6 所示, 灰色框表示被约减的状态或路径.

S0

e1 e2

…
e2 e1
… … …
S1 S2 S3 S4 S5 …
(a) 事件独立性约减 (b) 状态对称性约减 (c) 垂直领域约减
图 6 独立性、对称性和垂直领域约减示意图

4.2.1 独立性约减
动态偏序约减依赖事件的独立性, 以避免对独立事件进行无意义的重排序. 对系统事件独立性的信息越充分,
可约减的等价执行路径就越多. 传统 DMCK 未利用系统语义信息, 通常仅判断不同节点间的消息独立性. 例如, 在
同一状态下, 若多个消息发送至不同节点, 因各节点对不同消息的处理互不影响, 系统执行结果不会因接收顺序变
化而发生改变, 因此这类消息被视为彼此独立.
为更全面地识别分布式系统中的独立事件, 尤其是多条消息发送至同一节点的独立性, 以及崩溃事件与消息
事件的独立性, SAMC [11] 提出了两种基于系统语义的独立性约减策略. 首先, 本地消息独立性 (local-message
independence, LMI) 关注同一节点接收的多条消息是否独立. SAMC 根据消息对本地 (节点) 状态的影响方式, 并
结合分布式系统中常见的设计模式, 总结出 4 类消息处理语义, 并将其封装为条件语句: 1) 消息被丢弃 (predicate
discard, pd), 即消息不会影响本地状态, 直接丢弃, 例如许多分布式协议 (如 Raft, Paxos) 会丢弃旧版本号或过时的
投票信息; 2) 变量自增 (predicate increment, pi), 即消息接收处理对某个变量进行自增操作, 例如选举投票计数的
更新; 3) 变量赋值为常量 (predicate constant, pc), 即消息到达后直接赋值为固定值, 例如节点接收到领导者消息后
角色变为跟随者; 4) 本地状态修改 (predicate modify, pm), 即消息会导致本地状态发生变化, 例如接收到客户端请
求后更新日志内容. 基于这些语义, SAMC 设定了以下规则来判定消息是否独立: 1) 若任意一条消息满足 pd, 则两
条消息独立; 2) 若两条消息均满足 pi 或 pc, 则它们独立; 3) 若其中一条消息为 pm, 且无 pd 消息, 则两条消息不独
立. 用户只需对语义进行简单建模即可利用这些规则, 例如 m.vote < localState.myVote 这一条件可用于判断 pd, 表
示当消息 m 的投票值小于本地投票值 localState.myVote 时直接丢弃该消息.
其次, 崩溃-消息独立性 (crash-message independence, CMI) 关注崩溃事件与消息的独立性. 传统 DMCK 并未
建模节点崩溃事件的语义, 因此需与所有事件重排序, 加剧状态爆炸, 导致许多 DMCK 仅能注入极少量崩溃事件