企业官网建设流程全解析

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），可以直接交给 TLC（TLA+ 的模型检验器）运行，在有限状态空间内穷举所有可达状态，验证不变式（invariant）与活性（liveness）性质。

当前仓库中实际存在的规格分布在四个组件领域下：

每个规格目录下都附有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.cfg（TLC 配置）：文本格式的模型配置，声明SPECIFICATION、CONSTANTS的具体取值、要检查的INVARIANT/PROPERTY、可选的CONSTRAINT与SYMMETRY。

MCSpecName.tla与MCSpecName.cfg的文件名前缀MC是硬性约定：模型检验脚本会按“目录名的最后一段 + MC 前缀”自动推导要加载的.tla文件，详见下文脚本剖析。

三、运行模型检验：下载 TLC 并执行model-check.sh

3.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. 必须且只能传 1 个参数（SPEC_DIRECTORY），否则打印用法并退出；
2. 该路径必须存在且是目录；
3. 当前目录必须已有tla2tools.jar；
4. 按TLA_FILE="MC$(echo $1 | sed 's/.*\///').tla"从参数中截取目录名最后一段、拼上MC前缀，推导模型文件（例如参数Replication/RaftMongo对应Replication/RaftMongo/MCRaftMongo.tla），文件不存在则报错。

这也解释了规格文件为什么必须按“SpecName.tla+MCSpecName.tla+MCSpecName.cfg”命名：脚本只认识这套命名约定。README 同时提示，部分规格的额外说明写在其.tla或.cfg文件注释里，运行前应阅读。

3.3 脚本内部的 TLC 参数剖析

脚本核心的 TLC 调用行值得逐项解读，它体现了为大型模型检验场景调优的实践：

"$JAVA_BINARY" -XX:+UseParallelGC \ -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet \ -Dutil.ExecutionStatisticsCollector.id=10f53a1c957c11ea94a033245b683b65 \ -cp ../../tla2tools.jar tlc2.TLC -lncheck final -workers auto "$TLA_FILE"

• -XX:+UseParallelGC：启用并行垃圾回收器，缓解状态探索过程中的堆压力；
• -Dtlc2.tool.fp.FPSet.impl=tlc2.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.cfg

CONSTANT 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.cfg

SPECIFICATION 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 StateConstraint：StateConstraint == \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.cfg

SPECIFICATION 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.cfg

SPECIFICATION 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 建模纪律的绝佳教材，其注释浓缩了三条重要经验：

1. 规格正确性不变式与协议正确性不变式分开管理：TypeOK、ShardDataConsistentWithUUID等是“规格自身的健全性检查”，默认注释掉、仅在修改规格时开启；而CommittedTxnImpliesAllStmtsSuccessful、CommittedTxnImpliesConsistentKeySet这类“协议正确性不变式”必须始终启用；
2. 诱饵不变式（bait invariant）：BaitStaleDatabaseVersion、BaitStaleShardVersion、BaitSnapshotIncompatible、BaitHappyPath、BaitTrace等是被故意写成“错误”的命题。每次只启用一个，TLC 便会给出对应故障场景的反例轨迹，用于验证规格“确实能抓出某种 bug”，相当于模型的冒烟测试；
3. CONSTRAINT与活性PROPERTY互斥：注释明确说明——<>（eventually）与~>（leads-to）类活性性质在存在CONSTRAINTS时可能检测不到违规；同时启用会拖慢模型检验且不会带来额外收益。同样，检查活性性质时不应使用对称性集合（symmetry sets），否则 TLC 可能漏报错误或报告不存在的错误。因此该文件把唯一的活性性质ResponseForUntrackedNameSpaceIsFromPrimaryShard单独保留，并在需要完整活性检查时按注释建议关闭CONSTRAINTS与SYMMETRY。

4.5 小结：.cfg指令速查表

五、规格本体剖析：从源码级细节看建模思路

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（释放许可并唤醒队首）、ImmediateResize（Resizer 客户端一次性增减许可）、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] = 0）；ImmediateResize还要求permits + taken + n >= ResizerClientMaxTickets，保证调整后至少有足够的票据留给 ResizerClient。

配套不变式AwakeBeforeNonAwake（队列中已醒者必然排在未醒者之前）与TakenMatchesHolding（taken必须等于全体客户端持有票据之和）共同构成了对该协议正确性的完整刻画。

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 的工程经验归纳为三条可复用的方法：

1. 用状态约束（CONSTRAINT）封顶所有无界维度。每个规格的MCSpecName.tla都定义了自己的StateConstraint：RaftMongo 封顶任期与日志长度（MaxTerm、MaxLogLen）、Reconfig 额外封顶配置版本与已提交条目数（MaxConfigVersion、MaxCommittedEntries）、OrderedTicketSemaphore 封顶permits + taken < 10。无界是模型检验的天敌，建模时必须为每个会无限增长的变量找到上限。
2. 用对称性（SYMMETRY）压缩同构状态。节点集合、分片集合、客户端集合天然可交换，Permutations(Server)让 TLC 只探索每种排列的一个代表。但务必记住 cfg 文件中的两处警告：对称性可能使活性检验失效（Reconfig cfg），检查<>/~>性质时应禁用约束与对称性（TxnsCollectionIncarnation cfg）。
3. 用诱饵不变式（bait invariant）验证规格本身的检错能力。故意引入一个错误命题，确认 TLC 能给出反例轨迹，从而证明“这个模型真的能抓出那类 bug”。这与测试中的“变异测试”思想同源，是形式化规格质量保障的重要一环。

七、总结：从 README 到可复现的模型检验工作流

回到 README.md 的定位，它是一个高度凝练的“目录使用说明”：规格的组织范式（Component/SpecName三件套）、运行方式（./model-check.sh Component/SpecName）、以及“详细说明请读各规格注释”的指引。而本文在此基础上，结合仓库内真实规格与配置，把完整工作流展开为五步：

1. 阅读目标规格的SpecName.tla头部注释，确认其建模范围与实验/实现属性；
2. 按需调整MCSpecName.cfg中的常量（节点数、任期数、日志长度等），注意与MCSpecName.tla中StateConstraint的匹配；
3. 执行cd src/mongo/tla_plus && ./download-tlc.sh获取 v1.7.0 的tla2tools.jar（需要 Java 11，可用JAVA_BINARY指定路径）；
4. 执行./model-check.sh Component/SpecName启动 TLC（必要时可用bazel run //src/mongo/tla_plus:model_check -- <SpecDir>走 Bazel 路径）；
5. 解读 TLC 输出的反例轨迹（counterexample trace），定位违反的INVARIANT/PROPERTY，必要时启用对应诱饵不变式复现目标缺陷。

这套工作流的价值在于：它把“MongoDB 复制/分片/并发组件为何正确”从代码评审的定性讨论，变成了可穷举、可复现、可回归的形式化验证。对任何希望深入研究分布式共识与并发协议正确性的开发者而言，src/mongo/tla_plus目录都是一份可以直接运行、边读边验的活教材。

【免费下载链接】mongoThe MongoDB Database项目地址: https://gitcode.com/GitHub_Trending/mo/mongo