Page 293 - 《软件学报》2026年第5期
P. 293
2172 软件学报 2026 年第 37 卷第 5 期
● 错误事件: 包括节点宕机、重启、网络分区、消息丢失、重复或乱序等. 错误事件是分布式系统的固有特
性, 影响节点间的网络状态, 并可能进一步改变整个系统的执行路径, 尤其是在边缘情况下.
● 客户端请求/工作负载: 客户端可以在任意时刻发送请求至服务器, 影响系统状态.
在上述全局事件中, 超时机制在多个事件的判定与触发中发挥关键作用. 分布式系统常通过超时检测网络异
常或节点故障 (如网络分区、节点宕机), 进而触发重试、错误处理等操作, 例如定期发送保活消息并在超时未收
到响应时认定节点失联. 此外, 由于系统时钟漂移 (clock drift) [41] 和定时器调度的不确定性, 超时事件的触发时刻本
身具有不确定性, 进一步加剧了代码级状态空间的复杂性.
局部事件指影响节点内部执行环境的不确定性, 通常涉及线程调度与资源访问, 并取决于系统的代码实现方
式. 主要包括以下几类.
● 线程调度: 在多线程并发执行时, 线程可能在任意执行点被抢占或交替运行, 不同的调度顺序可能改变共享
数据结构的访问顺序, 从而影响系统行为. 例如, 持久化线程与消息处理线程的调度顺序不同, 可能导致节点状态
的差异.
● 资源访问: 某些资源访问相关的系统调用可能受环境因素影响, 尤其是磁盘 I/O 操作, 其执行结果可能成功
或失败, 从而引入不确定性.
● 随机数: 系统中若通过随机数控制执行逻辑 (如随机化超时), 将引入不确定性. 随机数的生成依赖操作系统
提供的种子, 因此受环境影响.
此外, 未定义行为和弱内存模型等节点内部环境的不确定性通常不属于 DMCK 的关注范围, 研究中常通过简
化假设加以规避, 例如默认不存在未定义行为, 并采用强一致性内存模型.
为了实现这些事件的确定性模拟执行, 系统需要能够从一个状态精确地转移到另一个状态, 并具备回溯能力,
以便探索不同的执行路径. 根据状态保存和恢复的方式, 现有技术主要分为两类: 基于状态的方法通过存储和恢复
内存信息来回溯系统状态, 而基于事件的方法则依赖于事件序列的重新执行来恢复先前状态.
不同的研究工作由于研究目标不同, 在技术选型、技术特性、全局事件与局部事件的支持能力、实现方式以
及被测系统上各有差异. 表 1 对比了实现确定性模拟执行技术的典型工具, 其中, “技术特性”主要考察以下 3 个方
面: 易扩展性 (extensibility), 即是否能在不修改 DMCK 工具自身的情况下, 轻松引入新的事件类型; 可适用性
(adoptability), 即是否能广泛适用于不同类型的分布式系统; 透明性 (transparency), 即 DMCK 工具是否能在无需大
幅修改被测系统的前提下, 直接验证新的目标系统.
表 1 确定性模拟执行技术典型工具的支持能力、实现技术及应用范围
发表会议及 技术实现 技术 全局事件支持 局部事件支持
工具 事件操控方式 被测系统
年份 分类 特性 能力 能力
[42]
OSDI 2002 , 易扩展、 部分支持 (仅 手动适配被测系统到 Linux等系统实现的AODV、
CMC [43] 基于状态 支持所有类型
NSDI 2004 可适用 资源访问) CMC运行时环境 TCP协议
Mace/ PLDI 2007 [44] , 基于状态/ 透明、 支持所有类型 部分支持 (仅 自动编译到Mace语言 Mace语言编写的程序:
MaceMC NSDI 2007 [45] 事件混合 易扩展 线程调度) 运行时环境 Chord、RandTree等
Erlang语言 (子集) 实现的
自动翻译到McErlang
McErlang [46] ICFP 2007 [47] 基于状态 易扩展 支持所有类型 未支持 分布式协议: Chord、Leader
运行时接口
Election
部分支持 (仅 支持所有类型 透 明 截 获 操 作 系 统 主要面向多线程程序:
透明、
[48]
Chess OSDI 2008 基于事件 支持消息事 (主要面向线 (Windows) 调度相关 PLINQ、CDS, 也可检查
可适用
件) 程调度) API 分布式系统: Dryad
透明截获应用程序与
透明、 Berkeley DB、MPS、
[49]
MoDist NSDI 2009 基于事件 支持所有类型 支持所有类型 操作系统 (Windows)
可适用 PacificA
的交互, 错误注入
自 动 编 译 到 Crystal- Mace语言编写的程序:
透明、 部分支持 (仅
[50]
CrystalBall NSDI 2009 基于状态 支持所有类型 Ball 运行时环境 (基 RandTree、BulletPrime、
易扩展 线程调度)
于Mace) Paxos和Chord

