Page 303 - 《软件学报》2026年第5期
P. 303

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


                 探索效率.
                    在探索一条执行路径时, 首先需要初始化集群环境, 这一过程涉及诸多耗时操作, 如清理磁盘和启动节点进
                 程. 例如, FlyMC 的集群初始化平均耗时 18 s. 无状态搜索的状态回溯会导致重复执行事件序列, 而初始化集群是
                 所有执行路径的首个事件, 因此消耗大量时间. 为优化此过程, FlyMC 和 dBug 采用初始状态快照, 大幅减少了重
                 复初始化的开销, FlyMC 将平均初始化时间从 18 s 降至 2 s         [104] .
                    代码执行过程中存在多种影响速度的因素, 如超时等待、磁盘写入和虚拟机运行时开销. 其中, 与超时相关的
                 逻辑通常可通过虚拟时钟加速           [49,67,71] , 避免真实等待. MoDist 采用虚拟时钟, 实现了  22–159  倍的加速. 然而, 其他
                 影响执行速度的因素通常难以进一步优化.
                    模型检验器本身也可能引入额外开销, 如插桩和调度开销. 插桩开销因确定性模拟执行技术的不同而有所变
                 化, 例如  MoDist 的插桩开销占代码执行时间的 18%–57%, 通常难以进一步优化. 调度开销则与实现方式相关. 例
                 如, FlyMC 在执行 54 个事件时耗时 18 s, 其中约 14 s 用于调度器在事件执行前的等待, 以防止并发问题. FlyMC
                 观察到并发问题较为罕见, 因此采用历史记录追踪缓存状态-事件转移, 缓存命中时无需等待, 将事件执行时间缩
                 短至 4 s [104] . 调度开销还受状态探索算法影响. MP-Basset 实现了有状态和无状态两种搜索算法, 有状态搜索在大
                 规模状态空间下优于无状态搜索; 而在较小状态空间下, 无状态搜索更具优势                       [59] .
                    现有工作均在一定程度上优化了状态探索速度, 但由于代码执行时间已成为主要开销, 进一步优化已接近瓶
                 颈. 我们总结了对代码直接进行模型检验的典型工具在单条执行路径上的平均执行时间: 底层操作系统劫持的
                 MoDist 约为  2 s; 基于代码插桩的   dBug  需  8–38 s, SAMC  接近  40 s, FlyMC  在  SAMC  基础上优化至  6 s.
                  3.3   属性验证

                    模型检验通过检查安全性          (safety) 和活性  (liveness) 属性来判定系统是否满足预期要求, 若属性不满足, 则表
                 明系统存在缺陷. 安全性检查确保系统在整个状态空间内始终满足特定条件, 即“坏事不会发生”. 活性检查则要求
                 系统最终达到预期状态, 即“好事最终会发生”. 目前, 所有传统 DMCK 均支持安全性检查, 而仅有少数支持活性检
                 查  (如  MaceMC  和  MoDist) [45,49] .
                  3.3.1    安全性验证
                    通用安全性约束: DMCK 直接运行被测系统代码, 因此需满足一些基本的通用安全性约束, 例如无内存泄漏、
                 无堆栈数据损坏、无节点异常崩溃等. DMCK 可检测节点在无错误注入的情况下是否崩溃, 若发生崩溃, 则表明
                 系统存在缺陷     [49,71] . 此外, 由于代码真实动态运行, 其他与内存相关的安全性问题通常可借助外部运行时检测工
                 具, 例如  Valgrind [105] .
                    领域特定安全性: 分布式系统的安全性通常依赖于具体应用场景, 违反这些属性可能导致严重后果. 例如, 共
                 识算法   (Raft、Paxos 等) 实现的分布式数据库需确保数据一致性、不可丢失、仅有一个有效主节点、提交编号单
                 调递增等. 这些领域安全性检查通常由开发者手动编码. 部分安全性可通过单个节点的本地数据检查, 例如提交编
                 号的单调递增性, 可直接在代码中插入断言              (assertion) 实现. 工业级系统通常在开发阶段已广泛使用断言. 而涉及
                 全局一致性的安全性        (如集群仅有一个有效主节点) 则需获取分布式系统的全局快照. 全局状态快照的获取依赖
                 于确定性模拟执行技术, 该技术可确保所有节点状态一致. 在基于事件的确定性模拟执行技术中, 系统需提供额外
                 的状态观测能力. 例如, MoDist 采用      D3S [89] 的  state exposer 技术, 通过透明劫持节点进程的特定函数或系统调用来
                 收集状态信息, 并由全局检查器验证系统行为是否符合安全性要求.
                  3.3.2    活性验证
                    活性属性要求系统最终达到某个期望状态, 而不仅是检查某些状态是否满足条件. 理论上, 活性验证需覆盖所
                 有可能   (包括无穷) 的执行路径或状态. 传统模型检验通常采用强连通分量                   (strongly connected component, SCC) 分
                 析, 并基于公平性假设       (fairness assumption) 排除“不现实”的执行路径, 其核心思想是: 如果系统进入一个            SCC  无
                 限循环且不满足活性属性, 则认为活性属性被违反.
                    然而, 在 DMCK 中, SCC 技术难以适用: 1) 有状态搜索在面对大规模分布式系统状态空间时, 难以高效使用
   298   299   300   301   302   303   304   305   306   307   308