前阵子帮一个做分布式任务调度的团队排查一个线上怪问题他们的选主模块在压测到一定并发时偶尔会出现双主——两个节点同时认为自己是 leader持续时间很短日志里一闪而过重启就消失平时复现不出来。我们三个人翻了两天代码和日志最后一哥们儿拍桌子说要不别猜了用 TLA 把选主逻辑画出来跑一遍。结果不到一下午模型检测器就把那条两条心跳同时过期、各自升主的路径给揪出来了路径短得让人不好意思——总共三步。这件事之后我彻底改变了看法形式化不是学术圈的自娱自乐模型检测也不是那种只能发论文的东西**TLA**这套工具在工程现场是真能省时间的。这篇东西我想聊的就是TLA 模型检测的实操入门。它是什么、能干什么、适合谁我先说清楚TLA 是一门用来描述系统应该怎么运行的规格语言配套的 TLC 模型检测器会把你能想到的所有状态逐个探一遍把违反不变量的执行路径原样端到你面前。它解决的是那种测试测不出来、代码审查看不出来、只有并发时序凑巧才触发的隐蔽缺陷。适合后端、分布式、协议、并发方向的工程师也适合对形式化验证感兴趣、想从工程视角摸一摸门道的同学。你不需要数学系背景会写函数、能理解状态变化就够了。需要提前说一句的是模型检测这个词现在有点被用滥了。搜索的时候你会看到一堆检测模型的结果什么目标检测、版面检测、漏水检测那些是机器学习里的模型跟这里说的模型检测model checking完全是两码事。我指的是用状态空间穷举来验证系统正确性的那一套方法TLA 是这条路线里工程友好度最高的工具之一。1. 先搞懂 TLA 到底在验证什么1.1 并发缺陷为什么这么难抓普通代码的错误大部分是输入错了或者逻辑写错了你写个单元测试喂几个用例就能覆盖。但并发系统的错误不是这个性质。它往往不取决于你是不是写错了某个表达式而取决于多个操作的时序交错。同样一段代码A 先发心跳还是 B 先发心跳结果完全不同网络延迟多一点少一点触发的分支也不一样。这种问题的本质是状态组合爆炸。假设一个系统有两个节点每个节点有几个内部状态加上消息在途的状态组合数就上去了。真实系统里动辄几个变量、几个进程人脑根本枚举不过来。你靠测试去撞撞中的概率极低这也是为什么这类 bug 总是偶发无法复现。TLA 的思路很直接既然人枚举不过来那就让机器把所有可达状态系统地走一遍一条都不放过。这就是模型检测的核心思想——不证明而是穷举加检查。1.2 模型检测和你写测试的根本区别很多人第一次听 TLA 会问这不就是个更复杂的单元测试吗不是。区别在于覆盖方式。测试是采样你挑几条输入路径跑一下看看结果对不对模型检测是穷举它把规格允许的所有行为轨迹全部走完只要存在一条违反不变量的路径它就能找到。换句话说测试能证明错但证明不了对而模型检测在一个有界的抽象世界里能给你在这个模型范围内没有反例的结论。当然这个有界是要害。TLA 的模型是对真实系统的简化你抽象得对不对直接决定了结论的价值。抽象得太粗漏掉关键状态模型通过也没意义抽象得太细状态爆炸机器跑不动。所以建模这件事七分在设计抽象三分在写代码。这一点我在后面会反复讲。1.3 什么样的系统值得上 TLA不是所有项目都值得引入 TLA。我自己的判断标准是三条第一系统里有并发或者分布式的成分多个执行流会互相影响第二一旦出错代价大比如数据不一致、资金错误、不可恢复的状态损坏第三逻辑的状态空间是有限的或者能抽象成有限状态。三条都满足TLA 的投入产出比就很划算。反过来一个纯 CRUD 的后台管理系统或者逻辑简单的数据处理脚本上 TLA 就是杀鸡用牛刀。它不是用来替代测试的而是用来补上测试永远覆盖不到的那块盲区。我一般只在协议、算法、一致性逻辑这类容易出错又难测试的模块上用它建模其余部分照旧写测试。1.4 和 Lean 那条路线的区别在哪现在形式化验证很热另一个常被提到的工具是 Lean。这里得说清楚两者的定位。Lean 是一款交互式定理证明器它走的是构造性证明路线——你得写出一份严格的数学证明让机器逐步校验每一步推理。它表达能力强能验证的东西理论上更广但门槛也高写证明本身是个技术活工程量不小。TLA 走的是模型检测路线你不用写完整证明只要把系统规格和要检查的属性写出来机器自动帮你穷举。代价是它只在一个抽象模型里有结论不能直接保证真实代码正确。两条路没有高下之分看需求想验证算法的数学性质、追求更严格的保证去啃 Lean想快速排查一个并发协议的时序问题、投入要可控TLA 更合适。我个人的经验是工程团队从 TLA 入手更平滑因为它离代码近、反馈快。2. 环境搭建与工具链选择2.1 用 Toolbox 还是 VS CodeTLA 有两种主流使用方式。一种是官方的TLA Toolbox基于 Eclipse 的图形化 IDE开箱即用建模、配置、跑模型、看反例轨迹都在一个界面里新手很友好。另一种是VS Code 插件TLA 扩展轻量适合已经习惯 VS Code 的人配合命令行工具 tla2tools.jar 使用。我建议第一次上手用 Toolbox因为它把配置什么、点了哪个按钮、反例长什么样这些环节都可视化了你能快速建立直观感受。等你熟悉了流程再切到 VS Code 做日常建模会顺手很多。我现在的习惯是探索阶段用 Toolbox 画状态图看反例把稳定的规格放进 VS Code 里跟代码一起管理。2.2 Java 环境与依赖准备TLA 工具链是 Java 写的所以第一步是装 Java 运行环境。JDK 8 以上都行我一般装 11 或 17 的 LTS 版本。装完在命令行敲java -version能打印版本号就说明成了。这一步踩坑的不多唯一要注意的是环境变量别配错尤其是 Windows 上装完要重启终端让 PATH 生效。如果你走命令行路线还需要下载tla2tools.jar这是核心工具包里面有 SANY语法解析器、TLC模型检测器、PlusCal 翻译器等。把它放在一个固定目录跑的时候用java -cp tla2tools.jar tlc2.TLC 你的模块名这种形式调用。我一般会把它路径存成环境变量省得每次写一长串。2.3 我的目录组织习惯建模文件多了以后目录乱是灾难。我的做法是每个被验证的模块单独一个文件夹里面放三样东西XXX.tla规格本体、XXX.cfgTLC 配置文件、README.md记录这次验证的假设和结论。配置文件单独拎出来很重要因为同一个规格你可能想用不同的常量跑多轮配置分离后切换成本很低。注意TLA 模块名必须和文件名严格一致大小写都不能差。我第一次踩的坑就是把文件存成mutex.tla而模块声明写成MutexSANY 死活解析不过排查了十几分钟才发现是大小写问题。2.4 一个最小可跑的结构长什么样在正式写模型前先认识一下 TLA 文件的基本骨架。一个典型的规格文件包含模块声明、扩展EXTENDS、变量声明VARIABLES、初始状态定义Init、下一步动作定义Next、完整规格定义Spec、以及你要检查的不变量或属性。这几块拼起来就是一个完整的状态机描述。理解了这点后面写复杂模型就是往这个骨架里填肉。下面我用一个最简单的计数器模型把流程跑通。3. 手把手跑通第一个 TLA 模型3.1 从一个计数器开始建立直觉先别急着上并发。理解 TLA 最好的方式是看一个笨模型。下面是一个计数器从 0 开始每次加一最多加到 2我们要验证它永远不会超过 2。---------------------------- MODULE Counter ---------------------------- EXTENDS Integers, TLC VARIABLES count Init count 0 Add count 2 /\ count count 1 Next Add Spec Init /\ [][Next]_count /\ WF_count(Next) Inv count 0 /\ count 2 别看它简单这里每个符号都有讲究。VARIABLES count声明了状态变量。Init用等号描述初始状态TLA 里这叫状态谓词。Add是动作里面的count带撇号表示下一时刻的 count没撇的是当前时刻。/\是逻辑与\E是存在量词\in是集合成员。[][Next]_count意思是每一步要么执行 Next要么 count 保持不变这是描述系统的标准写法。WF_count(Next)是弱公平性保证 Next 只要持续可执行就最终会被执行防止模型一直卡在原地不动。Inv就是我们要检查的不变量。3.2 配置文件怎么写Toolbox 里配置是通过界面点的背后其实是一个.cfg文件。手写的话长这样SPECIFICATION Spec INVARIANT InvSPECIFICATION指定用哪个公式来描述系统INVARIANT指定要检查的不变量。就这两行TLC 就知道该干什么了。如果你有常量还要加CONSTANTS段并赋值。配置文件的语法不复杂但大小写和拼写必须和模块里一致否则会报未定义符号。3.3 运行 TLC 并读懂输出跑起来之后TLC 会打印一大堆东西。最关键的几行是找到的状态数distinct states、生成的状态数、以及结论。如果是 Model checking completed. No error has been found.恭喜你模型在这个配置下通过了。如果出了问题它会打印反例轨迹一行一行列出来每个状态步告诉你从 Init 到违反不变量之间系统是怎么一步步走过去的。这份轨迹就是最值钱的东西它精确复现了 bug 发生的最小路径。我第一次跑通看到 No error 那一下还挺有成就感的但很快就意识到——没报错不代表没问题可能是我模型写得不对或者配置漏了约束。所以每次跑通我都会反向做一次验证故意把不变量改错看它能不能报出来。能报出来才说明检测配置是有效的。3.4 把不变量故意写错试试这是我最推荐新手做的一个练习。回到计数器把Inv改成count 1重新跑。TLC 立刻会给你反馈并给出反例从count 0开始执行一次 Add 到count 1还不违反再执行一次到count 2此时count 1被违反了。它精确告诉你哪一步越界了。这个练习的价值在于它让你相信工具是真的在工作而不是在敷衍你。\* 故意写错的不变量用于验证检测器确实能抓到问题 InvBug count 1做完这个反向验证你就对 TLC 的能力有了实感。接下来我们上真正有用的东西——给一个并发场景建模。4. 给真实场景建模从互斥到选主4.1 先明确要验证的属性建模第一步不是写代码是明确我要系统满足什么。以互斥为例核心属性就一条任意时刻最多一个进程在临界区。用 TLA 表达出来就是临界区集合的基数不超过 1。属性定了模型才有目标。这一步最容易被跳过但它决定了你后面的抽象边界——凡是和这条属性无关的状态都可以砍掉这就是控制状态空间的关键。提示建模前先把要验证的性质写成一句大白话再翻译成 TLA。如果这句大白话你自己都说不清楚说明你还没想清楚系统该怎样。4.2 一个带锁的两进程互斥模型下面这个模型模拟两个进程通过一把互斥锁进入临界区。锁只有 free 和 occupied 两种状态进程只有 idle 和 crit 两个阶段。------------------------- MODULE SimpleMutex --------------------------- EXTENDS Integers, FiniteSets, TLC VARIABLES pc, lock, critical Procs {0, 1} Init /\ pc [i \in Procs |- idle] /\ lock free /\ critical {} Enter(i) /\ pc[i] idle /\ lock free /\ pc [pc EXCEPT ![i] crit] /\ lock i /\ critical critical \cup {i} Exit(i) /\ pc[i] crit /\ lock i /\ pc [pc EXCEPT ![i] idle] /\ lock free /\ critical critical \ {i} Next \E i \in Procs: Enter(i) \/ Exit(i) Spec Init /\ [][Next]_pc, lock, critical MutualExclusion Cardinality(critical) 1 这里用了几个新东西[i \in Procs |- idle]是一个函数在 TLA 里叫函数本质是映射表示把每个进程映射到它的状态EXCEPT用来做函数更新类似复制一份然后改一个字段\cup和\是集合并与差Cardinality来自FiniteSets模块算集合大小。Enter(i)里先判断锁是 free 才能进进的时候把锁设成自己这样另一个进程就进不来了。配置里检查MutualExclusion跑起来应该报 No error。4.3 去掉一个约束看它怎么炸教学的关键来了。现在我们把Enter里的lock free这一行去掉也就是让进程不检查锁直接进EnterBug(i) /\ pc[i] idle /\ pc [pc EXCEPT ![i] crit] /\ critical critical \cup {i}重新跑TLC 立刻报错并给出反例进程 0 进入临界区后进程 1 也能进此时critical {0, 1}基数等于 2违反 MutualExclusion。这份反例轨迹只有两三步看一眼就明白 bug 在哪。这就是模型检测的威力——它不是在猜哪里可能出错而是把出错的最短路径直接怼到你脸上。我拿这个改动给团队演示过一次印象很深。有人当场说这不就是少写个 if 吗我 code review 能看出来。问题是真实系统里的少写个 if往往藏在跨模块调用、回调顺序、异常分支里不是一眼能看出来的。模型检测的价值在于它把逻辑剥干净了让你只看时序不受工程噪音干扰。4.4 参数计算状态空间有多少很多人不关心这个但我觉得算一下能帮你判断模型能不能跑完。上面这个两进程模型每个进程 2 个状态idle/crit锁有 3 种取值free/0/1critical 集合最多 4 种可能。粗略组合上限是 2×2×3×4 48 个状态TLC 瞬间跑完。如果把进程数加到 5临界区组合变成 2 的 5 次方状态数就上万了加到 10直接爆炸。这就是为什么真实系统建模要拼命抽象。你会看到我在模型里从来不建模消息内容时间戳重试计数这些细节因为它们对要验证的互斥属性没影响。抽象不是偷懒是让模型检测可行的必要手段。如果你发现状态跑不完八成是抽象力度不够。5. 模型检测的常见坑与排查手册5.1 状态空间爆炸怎么破这是新手第一大会遇到的墙。TLC 跑着跑着不动了内存拉满状态数疯涨。解决办法有四个按优先级排第一砍掉无关变量能抽象的都抽象第二用对称性比如多个进程地位相同可以声明对称集让 TLC 只探一部分第三加常量约束比如让某个计数器不超过 3别让它无限涨第四加状态约束把不该出现但又不违反属性的状态直接排除缩小搜索范围。第二点补充一下。比如两个进程完全对称声明SYMMETRY Perms后TLC 会认为进程 0 和进程 1 互换是等价的不重复探。这个技巧能把状态数砍掉将近一半进程越多效果越明显。代价是要求你确认系统真的对称否则可能漏掉真实反例用之前要想清楚。5.2 建模抽象踩过的坑我踩过最典型的坑是抽象过头。有一次给一个带超时的选主协议建模我把超时机制简化成一个随机的布尔值结果模型怎么跑都通过。提交给同事一看他问超时和心跳过期的先后顺序对结果没影响吗我回去一查正是这个顺序决定了会不会双主。我的抽象把最关键的时序关系抹掉了模型自然查不出问题。这个教训让我养成了一个习惯每次建模完成先做一轮恶意审查——问自己要是我故意想让系统出错我会利用模型里的哪个简化。如果这个问题的答案指向某个被我砍掉的地方那说明砍错了得补回去。5.3 常见报错速查表报错/现象常见原因排查方向SANY 解析失败报未定义符号模块名与文件名不一致、拼写错、缺 EXTENDS逐一比对大小写和模块声明状态数一直涨跑不完状态空间爆炸、变量取值无界加约束、用对称性、砍变量一直报 Invariant violated 但看着没毛病不变量本身写错或抽象漏了前提检查不变量定义确认模型假设Deadlock reached某个状态下没有可执行动作检查 Next 是否覆盖所有情况是否需要 stuttering结果每次都一样但明显不对配置没引用对公式、常量赋值错检查 .cfg 里的 SPECIFICATION 和 CONSTANTS这张表是我自己攒的基本覆盖了八成新手报错。遇到问题先对号入座能省不少时间。5.4 一个容易忽略的细节类型一致性TLA 是弱类型或者说是无类型的变量可以赋任何值。这既是优点也是坑。我有次把一个表示节点 ID 的变量先用整数 0、1后来改成了字符串 n0、n1结果另一处还在做整数比较SANY 不报错TLC 跑到那个分支才崩报了个很隐晦的错。所以我的经验是建模时给每类变量定死类型并保持一致需要类型检查就用ASSUME加上谓词约束能提前挡掉不少低级错误。5.5 从模型结论到代码落地的距离最后说句实在话模型通过了不等于代码就是对的。TLA 验证的是抽象的规格你手写的代码可能实现得和规格不一致。所以落地的时候我一般会把模型里定义的状态动作映射到代码里的实际状态机逐条核对代码是否遵守了模型假设。模型的作用是给你一张正确的行为地图代码照着地图走但走没走对还得靠测试和代码审查兜底。它不是终点是一个更高起点的开始。我个人在实际操作中的体会是TLA 最值钱的时刻不是它说通过的时候而是它说这里有个反例的时候。那份反例轨迹省下的排查时间往往就是引入整套工具链的全部成本。所以别指望它一上来就证明你系统多完美把它当成一个会咬人的、专门找茬的搭档用它去主动找自己的麻烦这才是模型检测在工程里最舒服的用法。下篇我打算聊聊 PlusCal——那玩意儿能让你用类 Pascal 的伪代码写算法再自动翻译成 TLA写起来更接近日常代码适合不想啃纯 TLA 语法的同学。