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

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

制机制, 无法直接用于 Linux 或其他操作系统, 同时状态爆炸问题也限制了其错误注入的次数.
SandTable [71] 主要面向实现复杂分布式协议的系统, 如 ZooKeeper 和 RedisRaft, 其确定性模拟执行技术支持对
给定事件序列的重放. 其核心技术与 MoDist 类似, 但面向 POSIX API, 采用 LD_PRELOAD 动态链接库截获技术,
主要截获 C 标准库封装的系统调用, 在操作系统内核与被测系统之间插入轻量级截获层. 在分布式环境的操控方
面, SandTable 采用 TPROXY (transparent proxy) 代理技术, 使网络消息在节点无感知的情况下被转发至确定性模
拟执行引擎, 并由该引擎决定消息的送达时机. 此外, SandTable 还通过错误注入模拟了错误事件, 并实现了虚拟时
钟机制, 加速节点感知的时间. 然而, SandTable 主要关注触发协议级逻辑缺陷的全局事件, 并且由于其操控底层操
作系统的方式难以精准识别用户级线程调度, 因此不支持对局部事件进行有效操控; 另一方面, SandTable 的状态
探索能力转移到了模型层, 因此无法“push-button”式直接使用.
Chess [48] 专注于多线程并发程序的不确定性操控 (即局部事件), 其确定性模拟执行技术与 MoDist 类似, 通过
透明截获 WinAPI 来操控线程调度. 然而, Chess 主要针对单机多线程程序的并发错误检测, 不支持分布式系统确
定性模拟执行所需的全局事件截获. 不过, Chess 的实验包含了一个复杂分布式系统 Dryad, 表明其技术在分布式
系统模型检验中的潜力.
从以上工作可以看出, 通用型技术已经具备了应用于工业级分布式系统的能力, 并且具有快速适配新系统的
优势. 然而, Chess 和 MoDist 是专有工具, 未对外开源, 而 SandTable 由于面向特定场景, 无法“push-button”式直接
使用. 同时, 由于底层系统调用截获和新增事件支持的复杂性, 基于该技术的相关研究尚不多见. 尽管如此, 该技术
仍然展示了广阔的应用前景和研究潜力, 尤其在被截获的系统调用数量足够多的情况下, 适配新系统和增加新事
件将变得更加容易.
● 精准型技术 [11,45,56,64,67,73] : 直接插桩被测系统本身, 使事件代码能够精准确定性模拟执行, 具有较强的可扩展
性. 然而, 在适配新系统时, 往往需要对被测系统进行一定程度的手工插桩.
精准型技术通过直接在源代码中插桩, 实现对事件调度的精确、细粒度控制, 确保系统的确定性模拟执行. 相
比通用型方法, 它具有更高的灵活性和精准度, 但通常需要对被测系统进行一定的手工插桩. 典型代表性工作包
括 SAMC [11] 、FlyMC [67] 、dBug [56] 和 Remix [73] .
插桩技术的主要优点包括: 1) 原理直接: 在源代码层面添加特定的截获逻辑, 使代码执行受确定性模拟执行器
控制, 并按需阻塞或调度; 2) 操控精准: 插桩可精确作用于特定代码位置, 而非依赖外部环境间接影响, 从而提供更
细粒度的控制; 3) 广泛适用: 插桩技术适用于多种编程语言, 如 Java [11,67] 、C++ [56,67] 和 Erlang [64] 等. 然而, 插桩技术
也存在一定局限性: 1) 依赖源代码: 需要访问被测系统的源代码, 无法直接操控仅提供可执行文件的系统; 2) 适配
成本: 不同系统需进行特定适配, 增加使用和维护成本; 3) 潜在副作用: 不当的插桩可能影响原始代码逻辑, 导致误报.
SAMC [11] 、FlyMC [67] 和 Remix [73] 利用 Java 成熟的插桩库 AspectJ, 对 ZooKeeper、Cassandra、Hadoop 等工业
级开源分布式系统进行插桩操控. 这些工具的状态恢复机制均通过从初始状态重新执行事件序列的方式来实现.
SAMC 和 FlyMC 主要关注全局事件探索, 特别是在多错误注入场景下的状态空间约减; FlyMC 进一步优化了状态
探索效率. Remix 在支持全局事件的同时, 还进一步支持多线程并发、磁盘 I/O 等局部事件, 并允许不同粒度的事
件控制.
dBug [56] 对 DMCK 技术原理和实现进行了详细描述. 它依赖于手动使用其提供的 C/C++ 库运行时 API 对不确
定性事件进行插桩, 插桩的细节程度决定了控制不确定性事件的范围, 理论上支持全局事件和局部事件的控制. 被
测系统运行于 dBug 客户端, 截获事件后发送至 dBug 服务器端并等待调度. dBug 使用虚拟机运行被测系统, 虽然
虚拟机提供了快照功能, 但快照和恢复操作耗时且消耗空间, 同时虚拟机的内存状态难以用于状态去重, 因此
dBug 仅对初始状态进行保存和恢复, 非初始状态则采用基于事件的回溯技术.
MaceMC [45] 是基于 Mace 框架 [44] 开发的模型检验工具, 专注于发现活性缺陷 (liveness bug). Mace 框架提供了
编程规范和运行时环境, Mace 代码通过使用框架提供的接口, 实现了类似于自动化精准插桩的功能. 然而, 该框架
并不支持直接应用于现有的系统. Mace 框架支持基于状态的确定性模拟执行, MaceMC 利用这一特性, 通过状态的
哈希比对避免遍历重复状态. 然而, MaceMC 并不存储所有状态, 而是采用基于事件的状态回溯方法, 从而减少了实