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

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


                 了  6  个缺陷  [122] . 此外, Microsoft Research  开发了  P  语言  [115] , 设计上借鉴了  TLA+.
                    ● MongoDB. 在  2016–2019  年间, MongoDB  团队花费数年排查出    5  个严重缺陷, 使用   TLA+后, 仅用数周建模
                 验证便找出这些问题       [126] . 他们的经验表明, 在复杂的分布式协议中, 缺乏形式化模型几乎无法保证正确性. 此后,
                 MongoDB  采用  TLA+验证其改进版     Raft 设计  [24] 并在内部大量使用  TLA+规约.
                    ● DeepSeek. 采用  P  语言验证  AI 基础设施中的高性能分布式文件系统           3FS [26] , 涵盖集群管理、元数据、存储
                 服务和客户端等设计, 特别是针对其改良的              CRPQ  协议及  RDMA  软硬件结合设计进行验证.
                    这些案例表明, 在高层次设计阶段使用模型检验技术能够发现大量设计缺陷, TLA+ 等工具在分布式系统正
                 确性保障中发挥了重要作用, 并已成为业界最佳实践. 然而, 高层次规约在编写时未考虑与代码的互动, 多个工作
                 均指出规约与实现的不一致可能导致缺陷仍然存在于系统实现中                      [22,23,127] .
                    (2) 低层次规约
                    尽管已有不少业界成功实践, 但在多数软件开发过程中, 代码实现前并不常见完整的高层次规约. 此外, 随着
                 需求变化、性能优化或代码缺陷, 代码可能偏离原始设计, 即使高层次规约得到验证, 仍无法确保代码的可靠性.
                 因此, 尽可能贴近代码的低层次规约被提出, 其核心目标是保证规约与代码的一致性, 并提供交互机制以检测二者
                 的语义鸿沟    (第  5.2  节). 在此基础上, 低层次规约通过检查属性是否违反并通过交互机制来确认代码中的缺陷                         (第
                 5.3  节).
                    MongoDB  团队对产品级系统       Realm Sync 中的操作转换函数进行了        TLA+建模, 采用直接翻译代码为         TLA+
                 的方式, 使规约不仅反映设计, 也包含代码细节             [127] . 这一低层次规约发现了一个栈溢出问题, 令开发者震惊, 因为
                 该缺陷此前未被长时间海量的随机测试发现, 且该系统已是成熟的产品级系统. 在翻译代码过程中 MongoDB                                团
                 队也发现了多个代码与规约的分歧并进行了修复, 相关技术将在第                      5.2 节介绍.
                    SandTable [71] 作为互动式  DMCK  的典型代表, 观察到语义感知的       DMCK  仍面临状态爆炸问题, 并提出将状态
                 探索转移到规约层面, 以突破         DMCK  代码执行效率的瓶颈. 该方法采用低层次规约, 建模代码中的核心状态转移,
                 包括全局事件中的消息处理、超时、客户端请求、网络错误和节点故障, 同时抽象掉线程调度、消息序列化等不
                 关注部分. 该方法通过低层次规约验证, 发现了 17 个真实代码缺陷, 另有 6 个代码缺陷在规约与代码交互过程中
                 发现.
                    Remix [73] 也是互动式  DMCK  的代表工作, 发现粗粒度规约可能与代码存在分歧, 导致验证结果不准确, 而细
                 粒度规约则容易引发更严重的状态爆炸问题. 为此, Remix 提出了粗细粒度结合的规约方法, 在保持交互性的同
                 时, 避免丧失发现缺陷的能力. 该方法遵循“由粗到细、逐步细化”的开发原则, 支持增量式迭代开发, 兼具轻量级
                 与实用性. 通过该方法, 研究者在        ZooKeeper 中发现了 6 个深层缺陷. 相比      SandTable, Remix  规约方法在框架性和
                 方法学上更完善, 并覆盖更多不确定性事件, 如线程交互、磁盘操作等, 从而揭示更多难以发现的代码缺陷.
                    低层次规约强调与代码贴近, 因此在发现真实缺陷方面更具实用价值. 从 MongoDB 启发的从代码转译为规
                 约的方式到交互式       DMCK, 相关研究逐步形成规约框架和方法学. 由于其紧密贴合代码, 这些方法都需要提供特
                 定机制, 以支持规约与代码的互动          (第  5.2  节).
                  5.1.3    规约的语言
                    我们根据规约所使用的语言类型, 将规约语言归纳为                  3  类: 形式化规约语言、综合式规约语言和通用编程语
                 言. 这  3  类语言在表达方式上逐步贴近代码, 使规约更符合程序员的使用习惯, 降低模型与代码交互的成本, 并提
                 高了实用性.
                    形式化规约语言: 形式化规约语言主要提供高层抽象视角, 帮助开发者简洁地描述系统的核心特性和行为, 适
                 用于快速验证系统设计的正确性. 尽管这些语言也具备低层次规约的能力, 但由于其与编程语言的设计目标不同,
                 规约与代码间的同步演化和一致性维护是一个挑战.
                    Alloy [128] 是一种轻量级的形式化建模语言, 基于一阶逻辑和关系代数, 使用                SAT/SMT  求解. 它主要用于描述
                 和分析结构化系统       (如数据结构、访问控制等静态性质), 但缺乏显式的并发机制, 不利于分布式系统建模. 尽管
                 Alloy 6 引入了时序逻辑支持, 能够描述随时间演变的系统, 但其对分布式系统的支持仍有限. 早期有研究使用
   305   306   307   308   309   310   311   312   313   314   315