MongoDB TLA/PlusCal 形式化规格与 TLC 模型检验实战指南【免费下载链接】mongoThe MongoDB Database项目地址: https://gitcode.com/GitHub_Trending/mo/mongo本文以 src/mongo/tla_plus/README.md 为核心骨架结合 MongoDB 仓库src/mongo/tla_plus目录下的真实规格文件并发信号量、复制协议 Reconfig、Raft 共识、分片迁移与事务等展开。读者读完将掌握该目录的规格组织约定、TLC 模型检验器的启动方式与脚本参数含义、.cfg模型配置文件的完整语法以及如何通过“约束 对称性 诱饵不变式”裁剪状态空间来定位死锁、违反选举安全、回滚已提交日志等并发缺陷。一、目录是什么用形式化方法验证 MongoDB 组件正确性src/mongo/tla_plus是 MongoDB 仓库中存放 TLA / PlusCal 形式化规格formal specification的目录其目标是对各类组件进行正确性检验。README 开篇即明确两点目录中的规格部分属于实验性探索部分忠实反映 MongoDB 的实际实现具体以每个规格文件头部的注释为准部分规格面向模型检验model-checking可以直接交给 TLCTLA 的模型检验器运行在有限状态空间内穷举所有可达状态验证不变式invariant与活性liveness性质。当前仓库中实际存在的规格分布在四个组件领域下领域规格说明ConcurrencyOrderedTicketSemaphore建模 MongoDB 有序票据信号量的 acquire/release 协议用于演示 ResizerClient 连续取两张票据时产生的死锁ReplicationMongoReplReconfig复制协议中“重新配置reconfig”过程的规格仅允许单节点变更ReplicationRaftMongoMongoDB 中 Raft 共识算法的形式化规格ReplicationRaftMongoReplTimestampRaft 与复制时间戳结合的规格ReplicationRaftMongoWithRaftReconfig.tla位于目录顶层的扩展规格将 Raft 共识与基于 Raft 的 reconfig 合入同一模型ShardingMoveRange、RangeDeletionsSecondaryNodes、TxnsCollectionIncarnation、TxnsMoveRange分片场景下的范围迁移、次节点范围删除、集合代次incarnation与迁移过程中事务的交叉验证每个规格目录下都附有OWNERS.yml标明该规格的维护责任人。二、规格的组织约定Component/SpecName/三件套README 给出了目录内统一的组织范式。每个面向模型检验的规格都放在形如Component/SpecName/的子目录中包含三个配套文件Component/SpecName/ SpecName.tla specification规格本体 MCSpecName.tla additional operators for model-checking模型检验专用算子 MCSpecName.cfg configuration for model-checking模型检验配置以 Concurrency/OrderedTicketSemaphore 为例实际文件为Concurrency/OrderedTicketSemaphore/ OrderedTicketSemaphore.tla -- 协议规格本体定义状态变量与动作 MCOrderedTicketSemaphore.tla -- 定义 TicketLimit 等状态约束与诱饵算子 MCOrderedTicketSemaphore.cfg -- 声明常量、不变式、性质与约束 OWNERS.yml三者职责分工清晰SpecName.tla规格本体只描述系统本身。定义CONSTANTS、VARIABLES、初始状态Init、下一步动作Next以及不变式如TypeOK、ElectionSafety与活性性质如WaitingLeadsToHolding。它不关心状态空间大小追求的是“实现无关的算法级抽象”。MCSpecName.tla模型检验模块EXTENDS SpecName专为 TLC 添加模型层面的内容——最典型的是状态约束state constraint例如 MCOrderedTicketSemaphore.tla 中的TicketLimit permits taken 10它把可到达状态限定在有限范围内保证 TLC 能终止也可以放置诱饵不变式bait invariant用于定向制造反例。MCSpecName.cfgTLC 配置文本格式的模型配置声明SPECIFICATION、CONSTANTS的具体取值、要检查的INVARIANT/PROPERTY、可选的CONSTRAINT与SYMMETRY。MCSpecName.tla与MCSpecName.cfg的文件名前缀MC是硬性约定模型检验脚本会按“目录名的最后一段 MC 前缀”自动推导要加载的.tla文件详见下文脚本剖析。三、运行模型检验下载 TLC 并执行model-check.sh3.1 环境准备TLC 是 TLA 官方的模型检验器以单个tla2tools.jar形式分发。仓库提供了下载脚本 download-tlc.sh#!/bin/sh echo Downloading tla2tools.jar curl -fLO https://github.com/tlaplus/tlaplus/releases/download/v1.7.0/tla2tools.jar在src/mongo/tla_plus目录下执行该脚本即可获得版本为 v1.7.0 的tla2tools.jar。模型检验脚本 model-check.sh 启动前会检查当前目录是否存在tla2tools.jar缺失时提示“No tla2tools.jar, run download-tlc.sh first”并退出。3.2 运行方式README 给出的调用形式为./model-check.sh Component/SpecName从src/mongo/tla_plus目录执行。例如分别检验 Raft 共识规格与有序票据信号量规格cd src/mongo/tla_plus ./model-check.sh Replication/RaftMongo ./model-check.sh Concurrency/OrderedTicketSemaphore模型脚本在参数校验上做了严格检查必须且只能传 1 个参数SPEC_DIRECTORY否则打印用法并退出该路径必须存在且是目录当前目录必须已有tla2tools.jar按TLA_FILEMC$(echo $1 | sed s/.*\///).tla从参数中截取目录名最后一段、拼上MC前缀推导模型文件例如参数Replication/RaftMongo对应Replication/RaftMongo/MCRaftMongo.tla文件不存在则报错。这也解释了规格文件为什么必须按“SpecName.tlaMCSpecName.tlaMCSpecName.cfg”命名脚本只认识这套命名约定。README 同时提示部分规格的额外说明写在其.tla或.cfg文件注释里运行前应阅读。3.3 脚本内部的 TLC 参数剖析脚本核心的 TLC 调用行值得逐项解读它体现了为大型模型检验场景调优的实践$JAVA_BINARY -XX:UseParallelGC \ -Dtlc2.tool.fp.FPSet.impltlc2.tool.fp.OffHeapDiskFPSet \ -Dutil.ExecutionStatisticsCollector.id10f53a1c957c11ea94a033245b683b65 \ -cp ../../tla2tools.jar tlc2.TLC -lncheck final -workers auto $TLA_FILE-XX:UseParallelGC启用并行垃圾回收器缓解状态探索过程中的堆压力-Dtlc2.tool.fp.FPSet.impltlc2.tool.fp.OffHeapDiskFPSet将状态指纹集合fingerprint set切换为堆外磁盘实现。TLC 靠指纹去重已访问状态当状态数达到千万级时堆内指纹集会撑爆 JVM 堆磁盘指纹集是大型模型检验的标准做法-cp ../../tla2tools.jar脚本会先cd $1进入规格子目录两层深度因此用../../回退到src/mongo/tla_plus定位 jar 包-lncheck final把活性liveness检验推迟到安全检查全部完成之后统一进行。脚本注释说明这是为了“速度”for speed——活性检验涉及公平性fairness与时序逻辑计算开销远大于不变式检查延迟到结尾可避免其对状态搜索的干扰-workers auto自动探测 CPU 核心数并开启多线程状态搜索Java 版本要求脚本头部注释明确“Requires Java 11”。若java不在 PATH 中可通过环境变量JAVA_BINARY指定完整的 Java 可执行文件路径脚本会打印“Using java binary [...]”确认。3.4 Bazel 集成除直接执行 shell 脚本外仓库还提供了 Bazel 封装BUILD.bazel 中定义了一个sh_binary目标load(rules_shell//shell:sh_binary.bzl, sh_binary) package(default_visibility [//visibility:public]) sh_binary( name model_check, srcs [model-check.sh], visibility [//visibility:public], )这意味着在安装了 Bazel 的构建环境中可以通过bazel run //src/mongo/tla_plus:model_check -- SpecDir的形式接入统一的构建工具链具体参数与 shell 用法一致。四、.cfg模型配置的完整语法与实战参数README 没有展开.cfg的写法但仓库内四个规格的配置文件给出了完整、可复制的模板。TLC 的.cfg文件支持SPECIFICATION、CONSTANT(S)、INVARIANT(S)、PROPERTY(IES)、CONSTRAINT(S)、SYMMETRY等指令下面逐一结合真实文件讲解。4.1 Raft 共识规格MCRaftMongo.cfgCONSTANT MaxClientWriteSize 2 CONSTANT MaxTerm 3 CONSTANT MaxLogLen 3 CONSTANT Server {1, 2, 3} INVARIANT NoTwoPrimariesInSameTerm INVARIANT NeverRollbackCommitted INVARIANT NeverRollbackBeforeCommitPoint PROPERTY CommitPointEventuallyPropagates CONSTRAINT StateConstraint SPECIFICATION Spec各条目的作用CONSTANT给规格中的抽象常量赋具体值。Server {1, 2, 3}即 3 节点副本集MaxClientWriteSize 2限制主节点单次动作追加的 oplog 条目数MaxTerm 3限制模拟的选举任期数MaxLogLen 3限制任意节点 oplog 的最大长度。INVARIANT安全性质要求所有可达状态都满足。此处一次性检查三条NoTwoPrimariesInSameTerm同一任期最多一个主节点即选举安全、NeverRollbackCommitted已提交条目不得被回滚、NeverRollbackBeforeCommitPoint不得回滚到提交点之前的条目。PROPERTY时序性质此处CommitPointEventuallyPropagates是活性性质断言提交点最终会传播到所有节点。CONSTRAINT/SPECIFICATION分别绑定模型约束定义在MCRaftMongo.tla中与规格入口Spec。该 cfg 的注释还记录了一条非常真实的历史教训NeverRollbackCommitted与NeverRollbackBeforeCommitPoint是可以被违反的但不构成最终安全危害对应 SERVER-39626该问题至少需要 5 个节点、3 个任期、oplog 长度 ≥ 4超出了当时可承受的模型检验规模——这正体现了“用有限状态空间逼近真实行为”的建模取舍。4.2 Reconfig 规格MCMongoReplReconfig.cfgSPECIFICATION Spec CONSTANTS Leader Leader Follower Follower Down Down CONSTANT Server {n1, n2, n3} CONSTANTS MaxLogLen 2 MaxTerm 3 MaxConfigVersion 3 MaxCommittedEntries 3 SYMMETRY ServerSymmetry CONSTRAINT StateConstraint INVARIANT ElectionSafety PROPERTY NeverRollbackCommitted值得注意的写法枚举常量自赋值Leader Leader、Follower Follower、Down Down是 TLC 中为枚举类型常量的“模型值”赋值等价于声明三个互不相同的模型值SYMMETRY ServerSymmetry声明对称性集合。ServerSymmetry Permutations(Server)定义在 MCMongoReplReconfig.tla 中。TLC 借助节点可互换的对称性把等价状态归并指数级压缩状态空间。但 cfg 注释也明确警告“Symmetry checking may invalidate liveness checking in certain cases”——对称性归并在某些情况下会使活性检验失效或产生误报CONSTRAINT StateConstraintStateConstraint \A s \in Server : currentTerm[s] MaxTerm /\ Len(log[s]) MaxLogLen /\ configVersion[s] MaxConfigVersion /\ Cardinality(immediatelyCommitted) MaxCommittedEntries把任期、日志长度、配置版本、已提交条目数全部封顶保证状态空间有限性质选择安全性质ElectionSafety每个任期至多一个主节点用INVARIANT检查而“永不回滚已提交条目”被写成PROPERTY NeverRollbackCommitted其底层是[][~RollbackCommitted]_vars形式的时序算子说明同一类性质既可以用不变式表达也可以用时序逻辑表达具体选型取决于规格作者的抽象粒度。4.3 有序票据信号量MCOrderedTicketSemaphore.cfgSPECIFICATION Spec CONSTANTS Clients {c1, c2, c3, c4} InitPermits 3 ResizerClientMaxTickets 2 ResizeDelta 3 CONSTRAINTS TicketLimit INVARIANT TypeOK TakenNonNegative TakenMatchesHolding UniqueWaiters AwakeBeforeNonAwake PROPERTY WaitingLeadsToHolding NeverWaitsIndefinitely这一组参数直接对应规格中的四个常量客户端集合Clients、初始许可数InitPermits、Resizer 客户端最多同时持有的票据数ResizerClientMaxTickets、单次即时调整许可数的上下界ResizeDelta。不变式覆盖了从类型正确性TypeOK、票据守恒TakenMatchesHolding到队列结构UniqueWaiters、AwakeBeforeNonAwake的各个层面活性性质WaitingLeadsToHolding断言“不可中断等待的客户端最终一定拿到票据”NeverWaitsIndefinitely断言“等待的客户端最终要么持有票据要么离开队列”。4.4 分片事务规格MCTxnsCollectionIncarnation.cfgSPECIFICATION Spec CONSTANTS Shards {s1, s2} NameSpaces {a, b, c} Keys {k1, k2} Txns {t1, t2} TXN_STMTS 2 DDLS 4 INVARIANTS CommittedTxnImpliesAllStmtsSuccessful CommittedTxnImpliesConsistentKeySet PROPERTIES ResponseForUntrackedNameSpaceIsFromPrimaryShard CONSTRAINTS StateConstraint SYMMETRY Symmetry该配置文件是学习 TLC 建模纪律的绝佳教材其注释浓缩了三条重要经验规格正确性不变式与协议正确性不变式分开管理TypeOK、ShardDataConsistentWithUUID等是“规格自身的健全性检查”默认注释掉、仅在修改规格时开启而CommittedTxnImpliesAllStmtsSuccessful、CommittedTxnImpliesConsistentKeySet这类“协议正确性不变式”必须始终启用诱饵不变式bait invariantBaitStaleDatabaseVersion、BaitStaleShardVersion、BaitSnapshotIncompatible、BaitHappyPath、BaitTrace等是被故意写成“错误”的命题。每次只启用一个TLC 便会给出对应故障场景的反例轨迹用于验证规格“确实能抓出某种 bug”相当于模型的冒烟测试CONSTRAINT与活性PROPERTY互斥注释明确说明——eventually与~leads-to类活性性质在存在CONSTRAINTS时可能检测不到违规同时启用会拖慢模型检验且不会带来额外收益。同样检查活性性质时不应使用对称性集合symmetry sets否则 TLC 可能漏报错误或报告不存在的错误。因此该文件把唯一的活性性质ResponseForUntrackedNameSpaceIsFromPrimaryShard单独保留并在需要完整活性检查时按注释建议关闭CONSTRAINTS与SYMMETRY。4.5 小结.cfg指令速查表指令作用仓库示例SPECIFICATION指定规格入口一般为Spec全部四个 cfgCONSTANT(S)给规格常量赋模型值Server {1, 2, 3}、MaxTerm 3INVARIANT(S)检查所有可达状态都满足的安全性质ElectionSafety、TypeOKPROPERTY(IES)检查时序/活性性质CommitPointEventuallyPropagates、WaitingLeadsToHoldingCONSTRAINT(S)状态约束裁剪状态空间以保证终止TicketLimit、StateConstraintSYMMETRY对称性归并压缩状态空间与活性检查互斥ServerSymmetry、Symmetry五、规格本体剖析从源码级细节看建模思路5.1 有序票据信号量捕获“连续取两张票”的死锁OrderedTicketSemaphore.tla 的模块注释点明了建模动机Models the OrderedTicketSemaphore acquire/release protocol to demonstrate a deadlock if a ResizerClient takes two tickets consecutively.即该规格的使命是演示一个具体缺陷当 Resizer 客户端负责动态调整许可数的特殊线程连续获取两张票据时协议会死锁。规格建模了四个核心状态变量VARIABLES permits, \* 可用许可数整数 taken, \* 已取走许可数整数 waitQueue, \* 等待队列记录 [thread, awake, interruptible] heldTickets \* 每个客户端持有的票据数关键动作分为五类TryAcquire快速路径无需排队直接取票、Acquire慢速路径入队等待、WakeAndConsume被唤醒后消费许可并出队、DoRelease释放许可并唤醒队首、ImmediateResizeResizer 客户端一次性增减许可、Interrupt中断一个可中断的等待者。其中有几处值得品味的建模细节快速路径的判定条件经历了演进。当前实现为CanSkipQueue permits Len(waitQueue)而注释保留了一行被废弃的旧定义permits 0 /\ waitQueue 并标注其引发SERVER-122680死锁/活性失败——规格文件直接记录了真实线上缺陷的修复合订历史唤醒的级联语义。WakeFirstN唤醒队列中前 N 个未醒等待者Interrupt特别处理“已被唤醒但尚未出队”的线程——此时中断它必须继续唤醒下一个等待者WaitFirstN(RemoveAt(...), 1)否则会丢失唤醒信号导致活锁这是信号量实现中经典的“lost wakeup”问题Resizer 客户端的行为特权。CanAcquire允许 ResizerClient 在heldTickets[t] ResizerClientMaxTickets时连续持有多个票据而普通客户端一旦持有就必须先释放heldTickets[t] 0ImmediateResize还要求permits taken n ResizerClientMaxTickets保证调整后至少有足够的票据留给 ResizerClient。配套不变式AwakeBeforeNonAwake队列中已醒者必然排在未醒者之前与TakenMatchesHoldingtaken必须等于全体客户端持有票据之和共同构成了对该协议正确性的完整刻画。5.2 Reconfig 规格单节点变更下的配置安全MongoReplReconfig.tla 建模 MongoDB 复制协议中的 reconfig 流程并明确限定“仅允许单节点变更”This spec only allows single node changes。规格的核心是围绕**配置config**展开的三个变量config一个服务器集合、configVersion配置版本号、configTerm写入该配置时主节点的任期。Reconfig(i)动作仅允许 Leader 执行且前置条件非常严格Reconfig(i) /\ state[i] Leader /\ ConfigIsSafe(i) \* 当前配置必须安全 /\ \E newConfig \in SUBSET Server : /\ \/ \E n \in newConfig : newConfig \ {n} config[i] \* 加 1 个节点 \/ \E n \in config[i] : config[i] \ {n} newConfig \* 删 1 个节点 /\ i \in newConfig /\ AliveNodes(newConfig) \in Quorums(newConfig) \* 新配置至少有一个法定人数存活其中ConfigIsSafe(i)由两层判定构成TermQuorumCheck该节点以主身份联系过新配置的法定人数ConfigQuorumCheck法定人数内的节点配置版本与配置任期一致以及OpCommittedInConfig先前配置中已提交的条目必须在新配置中也已提交。BecomeLeader在升主时抬高configTerm与ConfigQuorumCheck协同确保“旧配置无法在 ConfigIsSafe 成立后赢得选举”。该规格还提供了丰富的不变式/性质供检查ElectionSafety每个任期至多一个 Leader、ConfigVersionIncreasesWithTerm、NeverRollbackCommitted、AtMostOneActiveConfig同时最多只有一个活跃配置以及活性性质ConfigEventuallyPropagates、ElectableNodeEventuallyExists。5.3 RaftMongo提交点机制与回滚边界RaftMongo.tla 是 MongoDB 中 Raft 共识算法的规格。与经典 Raft 规格相比它突出了 MongoDB 的两个特色抽象committedEntries已提交条目集合与commitPoint提交点分离committedEntries记录所有被确认提交的index, term条目每个服务器维护自己的commitPoint一个[term |- ..., index |- ...]记录CommitPointLessThan(i, j)按“先比任期、再比索引”的字典序比较提交点的新旧日志一致性检查与回滚判定CanSyncFrom(i, j)要求“i 的日志末项任期等于 j 日志中同索引处的任期”这正是 Raft 日志匹配性质的形式化CanRollbackOplog(i, j)判定节点 i 的日志是否落后于 j 而需要截断回滚。该规格文件头部直接给出了运行指引与 README 互为印证To run the model-checker, first edit the constants in MCRaftMongo.cfg if desired, then:cd src/mongo/tla_plus./model-check.sh RaftMongo注意这里省略了Component/前缀而 README 的写法是./model-check.sh Component/SpecName——两者等价因为脚本只取参数路径的最后一段来拼MC前缀。同目录下的 RaftMongoReplTimestamp 是 Raft 与复制时间戳replication timestamp机制的结合规格关注日志提交与时间戳推进之间的一致性目录顶层的 RaftMongoWithRaftReconfig.tla 则把 Raft 共识与“基于 Raft 的 reconfig”统一进一个模型用于验证二者的交互。5.4 分片相关规格迁移、删除与事务的交叉验证Sharding 领域下的四个规格覆盖了分片运维中最容易出并发错误的场景MoveRange分片间数据块chunk范围迁移的协议规格RangeDeletionsSecondaryNodes范围迁移后次节点上执行范围删除range deletion的规格——这是 MongoDB 分片迁移清理流程中与本地并发读写交互最微妙的环节TxnsCollectionIncarnation事务与集合代次collection incarnation交互的规格验证“已提交事务必然所有语句成功”“已提交事务必然保持一致的键集合”等协议不变式TxnsMoveRange事务与范围迁移并发时的行为规格。这些规格共享前面 4.4 节所述的一整套建模纪律规格不变式 / 协议不变式 / 诱饵不变式分层、约束与活性互斥是研究“分布式协议 并发事务”交叉场景下形式化方法的现成案例。六、状态空间裁剪三板斧约束、对称性与诱饵综合各规格的实践可以把 MongoDB 使用 TLC 的工程经验归纳为三条可复用的方法用状态约束CONSTRAINT封顶所有无界维度。每个规格的MCSpecName.tla都定义了自己的StateConstraintRaftMongo 封顶任期与日志长度MaxTerm、MaxLogLen、Reconfig 额外封顶配置版本与已提交条目数MaxConfigVersion、MaxCommittedEntries、OrderedTicketSemaphore 封顶permits taken 10。无界是模型检验的天敌建模时必须为每个会无限增长的变量找到上限。用对称性SYMMETRY压缩同构状态。节点集合、分片集合、客户端集合天然可交换Permutations(Server)让 TLC 只探索每种排列的一个代表。但务必记住 cfg 文件中的两处警告对称性可能使活性检验失效Reconfig cfg检查/~性质时应禁用约束与对称性TxnsCollectionIncarnation cfg。用诱饵不变式bait invariant验证规格本身的检错能力。故意引入一个错误命题确认 TLC 能给出反例轨迹从而证明“这个模型真的能抓出那类 bug”。这与测试中的“变异测试”思想同源是形式化规格质量保障的重要一环。七、总结从 README 到可复现的模型检验工作流回到 README.md 的定位它是一个高度凝练的“目录使用说明”规格的组织范式Component/SpecName三件套、运行方式./model-check.sh Component/SpecName、以及“详细说明请读各规格注释”的指引。而本文在此基础上结合仓库内真实规格与配置把完整工作流展开为五步阅读目标规格的SpecName.tla头部注释确认其建模范围与实验/实现属性按需调整MCSpecName.cfg中的常量节点数、任期数、日志长度等注意与MCSpecName.tla中StateConstraint的匹配执行cd src/mongo/tla_plus ./download-tlc.sh获取 v1.7.0 的tla2tools.jar需要 Java 11可用JAVA_BINARY指定路径执行./model-check.sh Component/SpecName启动 TLC必要时可用bazel run //src/mongo/tla_plus:model_check -- SpecDir走 Bazel 路径解读 TLC 输出的反例轨迹counterexample trace定位违反的INVARIANT/PROPERTY必要时启用对应诱饵不变式复现目标缺陷。这套工作流的价值在于它把“MongoDB 复制/分片/并发组件为何正确”从代码评审的定性讨论变成了可穷举、可复现、可回归的形式化验证。对任何希望深入研究分布式共识与并发协议正确性的开发者而言src/mongo/tla_plus目录都是一份可以直接运行、边读边验的活教材。【免费下载链接】mongoThe MongoDB Database项目地址: https://gitcode.com/GitHub_Trending/mo/mongo创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考