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

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

互独立且正交. 对于有状态搜索, 相关工作 [42,43,47,69,74] 采用基于状态的确定性模拟执行技术, 通过计算状态哈希并
比对来识别和约减重复状态. 有状态搜索的约减技术通常利用状态的对称性 [43,74] , 将理论上等价的状态归并为一
类, 并通过状态标准化机制确保等价状态的哈希值相同. 当探索到一个状态时, 如果其等价状态已被探索, 则跳过
该状态, 减少需要探索的状态数量 [96] . 例如, 在分布式系统中, 如果多个节点具有对等身份且执行相同代码, 交换
节点的身份 ID 不会影响系统行为, 这时可以将交换身份 ID 的调度产生的状态视为对称的.
有状态搜索还可以与 (静态) 偏序约减 (partial order reduction, POR) 技术结合, 进一步约减执行路径 [52,59,74] . 然
而, 动态偏序约减 (dynamic partial order reduction, DPOR) 技术 [97] (后文将讨论) 与有状态搜索的结合较为复杂, 因
为在 DPOR 的状态探索或回溯过程中, 已遍历的状态被跳过, 从而导致状态探索不完整. 尽管一些新算法 [98,99] 成功
结合了有状态搜索和 DPOR, 并解决了可靠性问题, 但这些算法可能会导致更高的内存消耗和更多的时间开销 [59] ,
IoTCheck [99] 的实验结果也表明了这一点.
对于无状态搜索, 目前仅有个别研究使用基于状态的确定性模拟执行技术 [45] 来支持状态去重, 而状态回溯依
赖于无状态搜索的事件回放. 相比之下, 更常见的无状态搜索方法采用基于事件的确定性模拟执行技术, 不存储状
态信息, 无法区分已访问状态, 容易导致状态空间迅速膨胀.
尽管无状态搜索算法结合了偏序约减技术, 该算法仍然面临探索较大的状态空间挑战. 计算 Persistent 集合通
常需要进行静态分析, 例如分析每个进程可能在哪些通信对象上执行哪些操作. 然而, 要精确计算出一个合适的
Persistent 集合仍然非常困难, 导致状态约减效果不佳 [97] .
为了解决静态分析的不准确性并最大程度减少等价执行路径的探索, Flanagan 等人 [97] 提出了动态偏序约减
(DPOR) 技术. DPOR 通过动态检测下一转移与当前执行路径中的转移的独立性, 在必要时为当前路径添加回溯
点, 只探索那些与当前路径不等价的执行路径. 具体而言, DPOR 基于深度优先搜索, 在探索路径中的每个状态
s 时, 为每个进程的下一转移维护一个回溯集合 (backtracking set). 当遇到一个转移时, 算法会追溯到当前路径中最
后一个与该转移有依赖关系的转移 (记作 S i ), 并利用“happens-before”关系来判断该依赖是否影响进程 p 的未来行
为. 如果有影响, 则将可能导致不同结果的转移添加到 S i 执行前状态的回溯集合中. 当深度优先搜索返回至 S i 执
行前的状态时, 回溯集合中的转移会被探索, 确保所有加入回溯集合的路径都得到探索. DPOR 算法通过数学证明
了, 已探索状态的回溯集合实际上是该状态的一个 Persistent 集合, 从而验证了 DPOR 算法的正确性.
DPOR 算法易于实现且能大幅减少状态空间, 为 DMCK 研究的开展提供了基础, 并成为后续基于无状态搜索
的研究所需实现的标准技术 [11,49,56,67] . 后续研究提出了分布式 DPOR 技术, 通过将不同路径的探索分布到多个节
点上, 大幅提升了 DPOR 的可验证规模 [100] . 此外, DPOR 并不保证探索路径数量的最小化, 为此, 后续研究提出了
最优 DPOR (optimal DPOR) [101] , 使等价的执行路径仅探索一次. 然而, 这些更先进的 DPOR 技术尚未有 DMCK 研
究工作进行集成.
尽管对称约减技术与偏序约减技术是正交的, 但在无状态搜索中无法直接结合. Godefroid [102] 通过将传统对称
约减基于的状态等价性转换为执行路径等价性, 在 VeriSoft 的偏序约减基础上实现了对称约减. Spore [103] 将对称约
减与 DPOR 结合, 进一步减少了无状态搜索的状态空间. 然而, 这种结合方式尚未在 DMCK 场景下适配和应用.
尽管状态去重、对称约减和偏序约减技术大幅减少了状态空间, 分布式系统的状态空间仍然十分庞大, 难以
完全穷尽. 这主要源于系统节点之间的消息通信与节点内部进程或线程间的交互逻辑的复杂组合. DeMeter [40] 提出
了动态接口约减 (dynamic interface reduction, DIR) 技术, 该技术利用分布式系统良好定义的接口, 即组件通过消息
进行通信. 其核心思想是动态发现系统组件之间的接口, 将不同组件分开检查 (局部状态空间探索), 并通过接口行
为组合它们, 以避免昂贵且不必要的全局状态空间探索, 从而在保持可靠性的前提下, 实现指数级的状态空间压
5
缩 (可达 10 倍). DeMeter 结合全局探索与局部探索两种模式. 全局探索阶段首先获取仅包含消息收发的执行路
径, 并将消息投射到相应组件. 局部探索阶段对各组件进行单独检查, 例如通过重放即将达到的消息, 并探索组件
内部的不同执行顺序 (如改变检查点线程与消息接收线程的调度). 如果局部探索过程中某组件发送了全局探索未
发现的新消息, 该消息将被汇报给全局探索, 与已有的消息执行路径组合, 重复执行此过程, 直至全局探索不再产
生新消息执行路径, 且局部探索完成已有消息的探索.