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

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

现复杂度和内存消耗, 但回溯过程会增加一定的 CPU 开销. 为提高回溯效率, MaceMC 可选择性地存储部分状态.
Concuerror [64] 是一个针对 Erlang 并发程序的模型检验工具. 它利用了 Erlang 语言的 actor 模型及其统一的进
程通信机制, 使得 Concuerror 的自动插桩工具能够直接对 Erlang 源代码进行语法变换, 从而对不确定事件自动插
入插桩代码. 然而, 尽管 Erlang 的 actor 模型和消息传递特性常用于构建分布式系统, Concuerror 主要用于检测并
发错误, 关注多线程执行的验证, 不支持涉及节点故障、网络异常等全局错误事件的检验.
从以上工作可以看出, 精准型插桩技术因其原理直接、操控精准以及广泛适用等优点, 得到了广泛的研究. 然
而, 其主要劣势在于被测系统需要一定程度的手工插桩. 尽管如此, 在工业界, 由于大多数企业自主开发系统并拥
有全面的系统知识, 插桩的成本相对可控 [11] .
3.1.4 确定性模拟执行作为关键技术的相关研究
近年来, 确定性模拟执行技术在分布式系统测试和重放调试研究中得到了广泛应用 [78−83] . 在工业界和开源社
区, 受到 FoundationDB [84] 启发的确定性模拟执行测试技术得到了广泛应用 [85−88] . 这些技术在分布式系统的测试与
调试中发挥了重要作用. 尽管这些研究通常不涉及状态空间的系统性探索, 因此不属于严格意义上的 DMCK, 确
定性模拟执行技术作为 DMCK 的关键使能技术, 经过适当扩展和演变, 可以转化为 DMCK. 例如, MoDist [49] 继承
了其前身 D3S [89] 的分布式系统调试能力, 而 MaceMC 及其调试器 MDB 也依赖 MaceMC 的模拟器来实现确定性
模拟执行 [45] . 鉴于此, 这些工作具有重要的研究价值. 接下来, 我们将分别从分布式系统确定性重放调试作为关键
技术的研究工作和 FoundationDB 启发的工业界应用两个角度展开讨论.
Liblog [83] 是一个分布式系统事件记录和确定性重放库, 基于 LD_PRELOAD 技术截获 C 标准库的系统调用封
装函数. Liblog 采用中心化的 logger 进程记录事件日志, 不同节点截获的信息 (如网络接收、节点超时等) 会被发
送到 logger. 重放时, Liblog 通过恢复最近的内存快照, 并按照事件日志的顺序执行, 以确保执行过程的可复现性.
Friday [79] 在 Liblog 的基础上, 提供了分布式断点和全局状态分析机制. 它能够协调多个 GDB 实例, 在指定节点上
设置断点, 并检查全局属性, 从而增强分布式系统的调试能力. WiDS [78] 基于 Macedon 框架, 在单个进程中模拟分
布式系统. 其核心方法是通过随机执行来发现缺陷, 并提供了缺陷确定性重放的调试功能, 使开发者能够精准复现
[80]
并分析问题. Morpheus 是一个针对 Erlang 分布式系统的并发测试工具, 通过程序重写技术拦截通信原语, 采用
偏序采样 (partial order sampling, POS) 方法进行随机测试, 同时提供确定性执行能力. 当发现错误时, Morpheus 能
够记录并重放精确的执行轨迹, 确保错误的可复现性. 该工具在 RabbitMQ 等系统中发现了 11 个先前未知的协议
错误, 展现了其有效性. DEMi (distributed execution minimizer) [81] 通过确定性调度优化分布式系统的缺陷执行路径,
减少 fuzzing 发现的缺陷中不必要的执行步骤, 从而提升可分析性和缺陷重现能力. 该工具通过插桩 Akka 框架的
消息和时钟, 实现受控的确定性执行. Mocket [82] 利用形式化模型的状态空间生成测试用例, 并通过 Java ASM 插桩
技术对分布式系统进行确定性执行, 以精确控制测试用例的执行过程. 测试过程中, Mocket 通过对比执行状态与
模型状态是否一致来检测系统缺陷.
FoundationDB [84] 是工业界最早在分布式数据库测试中引入确定性模拟执行 (deterministic simulation) 的系统.
由于当时 C++ 语法尚未提供对 actor 模型和协程 (如 async/await) 的语言级支持, FoundationDB 开发了 Flow 语言,
在 C++ 之上引入 actor 模型, 并通过对网络、磁盘、时间、随机数的模拟使得测试环境完全可控. 然而, 这也导致
其确定性模拟引擎与 FoundationDB 紧密耦合, 难以复用于其他项目. FoundationDB 以极高的可靠性著称, 其支撑
着苹果 iCloud 业务的数十亿级数据库. FoundationDB 的联合创始人 Will Wilson 随后创办了 Antithesis 公司 [85] , 专
注于利用确定性模拟执行技术进行分布式系统测试. Antithesis 构建了一个确定性模拟的虚拟机环境, 使得分布式
系统中 (或计算机系统中) 的几乎所有不确定性因素均可控 [90] . 该公司获得了多轮风险投资 (当前共融资 7 700 万
美元), 反映了确定性模拟执行技术在工业界的广泛关注和应用潜力. 在 FoundationDB 的启发下, 多款工业级产品
[87]
构建了各自的确定性模拟执行框架. 例如, RisingWave 开发者开发了 MadSim 框架, sled 数据库构建了其专属的
确定性模拟执行框架 [86] , tokio 项目也集成了类似的测试方法 [88] .
3.2 状态空间探索技术
本节将介绍状态空间探索技术的原理及其优化方法. 状态空间探索从初始状态出发, 系统性穷举可调度事件