TLA+模型检测实战：用TLC揪出双进程互斥协议时序缺陷

1. 从一次测试全绿、线上却撞车说起几年前我接手过一个双进程的临界区逻辑单测跑了三百多次全过压测一上量就偶发两个执行体同时进临界区。当时排查了整整两天最后发现是两个判断之间存在一个极短的时间窗口。问题在于这类时序窗口几乎不可能靠跑测试跑出来——你跑一万次没事第一万零一次出事而且是概率性出事。后来我把这段逻辑用 TLA 抽出来把进程状态压缩成四个取值TLCTLA 自带的模型检测器在几十毫秒内就给出了一个五步的反例轨迹清清楚楚地告诉我第 2 步和第 3 步之间必须插入一个原子操作。这就是模型检测和形式化验证在工程里的真实定位它不证明你的代码写得对它证明你的设计在一个被穷尽枚举的状态空间里没有违反你声明的不变式。TLA 是 Leslie Lamport 设计的一套规约语言核心表达力来自时序逻辑配套的工具链Toolbox / TLC负责把规约当成一个有限状态机去暴力搜索。这篇是实践一目标很明确让一个没用过形式化方法的普通开发者在自己机器上跑通第一个 TLA 模型并且亲手制造一个看起来完全正确的互斥协议然后让 TLC 把它打脸再一步步修好。读完你应该能独立写出百行以内的规约会读反例轨迹知道UNCHANGED、公平性、状态空间裁剪这些词在实操里到底意味着什么。顺便先把一个高频误解掐掉如果你在搜索引擎里输入模型检测大概率会先撞上一堆 AI 领域的目标检测模型、版面检测模型、河道水位检测模型、车牌检测识别模型、漏水检测训练模型之类的结果。这些词里的检测模型指的是神经网络权重文件和 TLA 的模型检测Model Checking完全是两码事。前者是拿数据训出来的函数逼近器后者是把系统抽象成状态迁移图之后做的穷尽搜索。搜索的时候记得带上TLA、TLC、形式化这几个限定词否则很容易被带偏。顺带一句如果你看到Lean 形式化验证那是另一条技术路线——定理证明Theorem Proving它靠人写证明脚本、机器检查证明能处理无限状态但需要大量人工TLA 走的是模型检测路线全自动但只覆盖有限或有界状态空间。这两者的取舍我会在第 1.3 节说清楚。2. 先把工具链跑通别卡在第一步2.1 Toolbox 和 VS Code 插件选哪条路刚上手的时候我建议用官方TLA Toolbox理由很实际它是 Eclipse 套壳界面笨重但它把编辑规约—配置模型—运行 TLC—查看反例轨迹这条链路做成了图形化的一整套。反例轨迹在 Toolbox 里是可视化的状态列表点开每一步能直接看到哪个变量变了、是被哪个动作改的这对新手理解反例到底在讲什么帮助极大。等你把语法和调试套路摸熟了再换成 VS Code 的 TLA 插件微软出的那个用起来轻快很多但轨迹展示就没那么友好了。运气不太好的是 Java 环境的坑新版工具链要求 JDK 11 或更高早期版本用 JDK 8 就能跑。如果你装完 Toolbox 打开就报找不到 Java或者启动直接闪退十有八九是 JDK 版本不对或者JAVA_HOME没配。我的做法是单独装一个 JDK 17 或 21把JAVA_HOME指向它不要让系统里那一堆乱七八糟的运行时互相干扰。如果你更习惯命令行tla2tools.jar是核心所有东西都在里面java -cp tla2tools.jar tlc2.TLC -config Peterson.cfg -workers 4 Peterson.tla-workers 4意思是开四个线程并行搜索状态空间多核机器上直接拉满。调试的时候还可以用-simulate num10000做随机模拟先快速看看规约能不能跑起来比完整枚举快得多。2.2 模块名必须等于文件名这个规定第一次一定会坑你TLA 的模块声明长这样---- MODULE Peterson ---- EXTENDS Integers, TLC ... 模块名Peterson必须和文件名Peterson.tla完全一致大小写敏感。不一致的话TLC 报的错非常晦涩不会直接告诉你文件名和模块名对不上。我第一次踩这个坑的时候对着报错研究了半小时最后才发现是自己随手把文件存成了peterson.tla。同理.cfg配置文件的基础名也要和模块名一致Peterson.cfg否则 Toolbox 可能关联不到。这些约定看起来是小事但它们属于那种不知道就一定会浪费你半小时的类型。2.3.cfg里真正要填的只有四类字段模型配置文件看着像天书其实常用的就四类SPECIFICATION Spec CONSTANTS Procs {0, 1} INVARIANT MutualExclusion PROPERTY LivenessSPECIFICATION指定要检查哪个时序公式。一般填Spec也就是Init /\ [][Next]_vars /\ 公平性这一坨的封装。CONSTANTS把规约里声明的常量具体化。这是模型规模的总开关Procs {0, 1}就是双进程模型换成{0, 1, 2}就是三进程。INVARIANT不变式TLC 会在每一个可达状态上检查它。这里写MutualExclusion就等价于任何时刻都不可能两个进程同时在临界区。PROPERTY时序性质活性只在实践二里细讲。有一个非常关键的区别要记住INVARIANT检查的是每个状态PROPERTY检查的是整条行为序列。互斥、取值范围、类型约束这类任何时刻都成立的东西写INVARIANT最终一定会进入临界区这种迟早性质写PROPERTY。写错了位置TLC 要么报类型错误要么给你一个你完全看不懂的结果。3. TLA 的核心抽象把状态机写成数学谓词3.1 变量和 Init初始状态往往不止一个TLA 里的VARIABLES声明的是状态变量也就是构成系统状态的那几个量。接着写Init它是一个谓词描述所有合法的初始状态。注意是所有——如果Init里有非确定性选择比如turn \in Procs那初始状态就是多个TLC 会把它们全都展开成搜索的起点。VARIABLES pc, flag, turn vars pc, flag, turn Init /\ pc [i \in Procs |- L0] /\ flag [i \in Procs |- FALSE] /\ turn \in Procs这里的[i \in Procs |- L0]是一个函数在 TLA 里函数本质是集合到值的映射把每个进程映射到初始状态L0。TLA 里没有数组这个概念凡是用下标访问的东西——数组、字典、HashMap——统一用函数表达后面你会看到pc[i]和pc [pc EXCEPT ![i] L1]这种写法。EXCEPT是函数更新算子[pc EXCEPT ![i] L1]的意思是除了下标i处的值改成L1其他位置保持原样。这跟函数式编程里的不可变更新是一个思路。3.2 Next 动作与 primed 变量的读法Next描述从当前状态到下一个状态的迁移关系。这里最容易绕晕的就是带撇号的变量。读法很简单记住一条规矩不带撇号的是当前状态的值带撇号的是下一个状态的值。一个动作就是一个关于当前状态 下一个状态的谓词TLC 的工作就是找出所有满足这个谓词的下一个状态。SetFlag(i) /\ pc[i] L1 /\ flag [flag EXCEPT ![i] TRUE] /\ pc [pc EXCEPT ![i] L2]这三行合起来的意思是如果当前进程i处在L1那么存在一个后继状态其中flag在i位置变成TRUEpc在i位置变成L2其余不变。因为turn在这个动作里被赋值了或者被UNCHANGED约束了所以它是确定的。提示如果某个动作既没给变量加也没写UNCHANGED那这个变量就成了下一个状态可以是任意值。TLC 遇到这种情况要么在求值时抛异常要么直接把状态空间炸掉。这是新手最常犯的错误之一。3.3UNCHANGED的三种写法和一个高频翻车点UNCHANGED常见的三种写法UNCHANGED turn \* 单个变量 UNCHANGED flag, turn \* 变量元组 UNCHANGED vars \* 因为之前定义了 vars pc, flag, turn第三种最省事前提是你提前定义好了vars这个元组这样Next和Spec都能直接复用。翻车点在于UNCHANGED pc, flag和UNCHANGED vars的语义不一样。前者只说这两个不变turn就没被约束语义上允许turn任意变。我在一个锁模型里因为漏了一个变量导致 TLC 报的状态数是理论值的上千倍而且反例轨迹长得完全没法看——因为里面混进了大量莫名改变的状态。所以我的习惯是每个动作写完先把vars里所有变量过一遍确认每一个要么有要么在UNCHANGED列表里。3.4 Spec 与公平性安全和活性分别靠谁保证把上面几块拼起来就是完整的规约Next \E i \in Procs : SetFlag(i) \/ Enter(i) \/ Exit(i) \/ Done(i) Spec Init /\ [][Next]_vars[][Next]_vars是时序逻辑写法读作要么发生Next迁移要么所有变量保持不变stutter。这个下划线写法把保持不动也纳入允许的行为非常重要——因为真实的系统里进程也会有空转的时候。如果你还想断言进程不会永远被饿死就得加公平性FairSpec Init /\ [][Next]_vars /\ \A i \in Procs : WF_vars(Enter(i))WF_vars(A)的意思是弱公平如果一个动作A在某时刻之后一直可执行那它最终一定会被执行。反过来SF_vars(A)强公平要求它在无穷多次可执行的情况下必须被执行。这两个概念在实际建模里的差别很微妙但加错了会导致活性检查出现假阴性——你以为协议没问题其实只是公平性假设太强了。注意公平性只影响活性liveness不影响安全性safety。这一篇我们只查安全不变式公平性可以先不加等实践二检查最终一定能进临界区时再回来细抠。4. 第一个真活儿写一个看起来完全正确的双进程互斥4.1 状态变量设计与迁移图我们要建模的是最朴素的自旋锁只有两个变量pc每个进程的状态机位置和flag每个进程是否想进临界区。每个进程的路径是L0检查对方的flag是否为FALSEL1把自己的flag置为TRUEL2临界区L3已完成空转这套设计的思路是我先看看对方想不想进想的话我就不抢了。听起来毫无问题这也是为什么它在很多人的直觉里是对的。4.2 完整代码---- MODULE FlagOnly ---- EXTENDS Integers, TLC CONSTANT Procs VARIABLES pc, flag vars pc, flag Other(i) CHOOSE j \in Procs : j / i Init /\ pc [i \in Procs |- L0] /\ flag [i \in Procs |- FALSE] Check(i) /\ pc[i] L0 /\ ~flag[Other(i)] /\ pc [pc EXCEPT ![i] L1] /\ UNCHANGED flag SetFlag(i) /\ pc[i] L1 /\ flag [flag EXCEPT ![i] TRUE] /\ pc [pc EXCEPT ![i] L2] Exit(i) /\ pc[i] L2 /\ flag [flag EXCEPT ![i] FALSE] /\ pc [pc EXCEPT ![i] L3] Done(i) /\ pc[i] L3 /\ UNCHANGED vars Next \E i \in Procs : Check(i) \/ SetFlag(i) \/ Exit(i) \/ Done(i) Spec Init /\ [][Next]_vars MutualExclusion \A i, j \in Procs : (i / j) ~(pc[i] L2 /\ pc[j] L2) Other(i)用CHOOSE挑出另一个进程。CHOOSE是 TLA 里的选择算子从满足条件的集合里挑一个——在Procs {0, 1}的条件下它是确定的。所以这个模块严格来说只对双进程成立三进程以上得换算法。配置文件SPECIFICATION Spec CONSTANTS Procs {0, 1} INVARIANT MutualExclusion4.3 不变式怎么写才算写对了MutualExclusion的定义值得反复看一眼\A i, j \in Procs : (i / j) ~(pc[i] L2 /\ pc[j] L2)这里有两个坑。第一个是必须排除i j的情况。如果不写i / j那么当i j时只要pc[i] L2整个式子就被破坏——哪怕只有一个进程在临界区。这是纯逻辑错误跟协议本身没关系。第二个坑是不变式不能过强。比如你写\A i \in Procs : pc[i] / L2意思是永远没人能进临界区这个不变式倒是不太可能被破坏除非 TLC 找不到路径但它表达的完全不是你想要的属性。不变式写得太强TLC 会给你一个看起来莫名其妙的反例——其实是你的不变式错了不是模型错了。经验每次看到Invariant is violated先花十秒钟问自己一句——到底是模型错了还是我这条不变式写错了这两个方向的排查路径完全不同。4.4 跑 TLC读反例轨迹点下运行TLC 会在几十毫秒内返回Error: Invariant MutualExclusion is violated. The behavior up to this point is: State 1: Initial predicate /\ pc (0 : L0 1 : L0) /\ flag (0 : FALSE 1 : FALSE) State 2: Check(0) line 21 of module FlagOnly /\ pc (0 : L1 1 : L0) /\ flag (0 : FALSE 1 : FALSE) State 3: Check(1) line 21 of module FlagOnly /\ pc (0 : L1 1 : L1) /\ flag (0 : FALSE 1 : FALSE) State 4: SetFlag(0) line 27 of module FlagOnly /\ pc (0 : L2 1 : L1) /\ flag (0 : TRUE 1 : FALSE) State 5: SetFlag(1) line 27 of module FlagOnly /\ pc (0 : L2 1 : L2) /\ flag (0 : TRUE 1 : TRUE)这就是那个我人工查了两天的 bug被压成五行。读法是从上往下看每一步被哪个动作驱动State 2 是进程 0 执行了CheckState 3 是进程 1 执行了Check。关键在于这两次Check都发生在任何一次SetFlag之前——两个进程都检查了对方还没想进然后各自去置自己的标志位。等它们都置完之后谁都拦不住谁了双双进入临界区。真实的硬件上这个窗口可能只有几十纳秒压测跑一万次也未必撞上。但 TLC 的逻辑是我不管你概率多低只要存在一条可达路径我就给你找出来。5. 反例读完之后三个版本的迭代与取舍5.1 为什么只靠一个标志位注定失败很多人第一反应是那我加个锁把 Check 和 SetFlag 合起来不就行了。可以但你得先明白为什么合起来就能解决。从对称性角度看得更清楚Check和SetFlag拆成两步之后两个进程可以同时在检查完毕、尚未置位这个中间状态两者看到的世界是完全对称的——都认为对方不想进。而互斥本质上是要求两个对称的进程做出不一致的决定一个进、一个等这必须有某个打破对称的东西。在FlagOnly里这个东西不存在所以失败是结构性的不是运气问题。这个结论其实可以推广只用对称的、只读的、每个进程私有的信息是解不了双进程互斥的。必须引入共享的可写状态。5.2 版本二加一个turn变量Peterson 算法Peterson 的做法是在把自己标志位置起来的同时把turn变量写成对方的编号也就是主动把优先权交出去。然后在等待时检查对方想进并且turn指向对方两个条件同时满足才等。---- MODULE Peterson ---- EXTENDS Integers, TLC CONSTANT Procs VARIABLES pc, flag, turn vars pc, flag, turn Other(i) CHOOSE j \in Procs : j / i Init /\ pc [i \in Procs |- L0] /\ flag [i \in Procs |- FALSE] /\ turn \in Procs L0(i) /\ pc[i] L0 /\ flag [flag EXCEPT ![i] TRUE] /\ turn Other(i) /\ pc [pc EXCEPT ![i] L1] L1(i) /\ pc[i] L1 /\ ~(flag[Other(i)] /\ turn Other(i)) /\ pc [pc EXCEPT ![i] L2] /\ UNCHANGED flag, turn L2(i) /\ pc[i] L2 /\ flag [flag EXCEPT ![i] FALSE] /\ pc [pc EXCEPT ![i] L3] /\ UNCHANGED turn L3(i) /\ pc[i] L3 /\ UNCHANGED vars Next \E i \in Procs : L0(i) \/ L1(i) \/ L2(i) \/ L3(i) Spec Init /\ [][Next]_vars MutualExclusion \A i, j \in Procs : (i / j) ~(pc[i] L2 /\ pc[j] L2) 为什么加一个turn就成立了因为turn是同一时刻只能取一个值的共享变量而且两个进程都会去写它。谁最后写谁就把优先权让给了对方。上面那个致命的交错序列现在长这样进程 0 写turn 1进程 1 写turn 0turn最终是 0于是进程 0 判断turn Other(0) 1不成立直接进临界区进程 1 判断turn Other(1) 0成立继续等。对称性被turn这个最后一个写入者打破了。5.3 版本三原子锁以及原子性假设藏在哪第三个版本更贴近工程实现——用一个共享的lock变量谁抢到谁进---- MODULE AtomicLock ---- EXTENDS Integers, TLC CONSTANT Procs VARIABLES pc, lock vars pc, lock Init /\ pc [i \in Procs |- L0] /\ lock free Acquire(i) /\ pc[i] L0 /\ lock free /\ lock i /\ pc [pc EXCEPT ![i] L1] Release(i) /\ pc[i] L1 /\ lock free /\ pc [pc EXCEPT ![i] L2] Next \E i \in Procs : Acquire(i) \/ Release(i) Spec Init /\ [][Next]_vars MutualExclusion \A i, j \in Procs : (i / j) ~(pc[i] L1 /\ pc[j] L1) 跑一下安全不变式能过。但这个能过是有前提的lock free这个判断和lock i这个写入被我合并成了一个原子动作。在真实硬件上这靠的是 CAS 之类的原子指令如果你的代码是先读一遍lock、再写一遍lock那就是两个原子步建模时也必须拆成两个动作——那时候它跟FlagOnly一样会失败。这是我认为 TLA 最有价值的地方之一它逼你把我在哪一步假设了原子性这件事明确写出来。这个假设平时藏在代码里、藏在 CPU 的内存模型里没人会主动提但一旦 TLA 报错它会把你这个假设直接摊在桌面上。三个版本对比版本共享状态关键假设安全性现实对应FlagOnly两个私有 flag无失败直觉型错误实现Petersonflag turn单字读写原子通过纯读写寄存器场景AtomicLock单个 lock比较并交换原子通过大多数锁实现5.4 重跑 TLC 与覆盖度确认改完之后重新跑除了看有没有报错我还会看两个数字states generatedTLC 生成过的状态数和distinct states found去重后的状态数。如果生成数远大于去重数说明你的模型里有大量重复到达的路径这是正常的——但要警惕一种情况去重后的状态数少得离谱比如只有个位数那大概率是某个动作永远不可达也就是你的Next里漏掉了什么东西。Toolbox 的模型概览里还能看动作覆盖度它会告诉你每个动作被执行了多少次。如果L3(i)的覆盖度是 0说明进程完成这条路径从来没被走过模型是不完整的。这个功能平时没什么存在感但排查某个分支永远进不去这类问题时非常有用。6. 状态空间、性能与 TLC 报错速查6.1 模型规模必须从小往大爬TLC 的状态空间是指数级的AtomicLock这类模型每个进程 3 个状态位置再加一个lock状态上界大致是3^N × (N1)进程数 Npc 组合数lock 取值数状态上界293273274108481540552436145886561959049105904911649539注意这只是上界实际可达状态会少很多但增长趋势骗不了人。我的习惯是先用Procs {0, 1}把不变式调通确认反例轨迹的逻辑讲得通再往{0, 1, 2}扩最后才上{0, 1, 2, 3}。绝大多数互斥/共识类算法的 bug 在 3 个进程时就会暴露直接上 8 个进程的结果通常是等半天然后得到一个你根本读不懂的巨型轨迹。一个反直觉的经验不要一上来就把模型做大。我见过太多人因为第一次跑就设了 6 个进程跑了十分钟内存爆掉然后得出结论TLA 太慢。其实问题在于他们没有分阶段验证建模本身对不对。6.2SYMMETRY和VIEW什么时候能用SYMMETRY是 TLC 的对称性归约。原理是如果Procs {0, 1, 2}里的进程是完全同构的那么进程 0 进临界区和进程 1 进临界区这两条路径在语义上是等价的可以合并只搜一次。声明方式是在.cfg里加SYMMETRY Symm并在规约里定义Symm Permutations(Procs)。但它有严格的使用条件规约必须对所有进程完全对称。如果你的模型里区分了主节点和从节点比如 Raft 里的 Leader 和 Follower那加上SYMMETRY会把不等价的路径合并掉导致 TLC 漏掉真实的反例——这是极其危险的一类错误因为它给你一种验证通过的假象。VIEW是另一个思路定义一个投影函数把状态映射到它的等价类上TLC 只在投影后的状态上做去重。它比SYMMETRY更通用但同样要求你自己论证投影的正确性。我的建议是在你完全想清楚等价关系之前别用这两个东西。先用小模型硬跑慢一点但结论可信。6.3 TLC 常见报错对照表报错或现象大概率原因处理方式Invariant ... is violated不变式被真实破坏读反例轨迹先判断是模型错还是不变式写太强Deadlock reached存在无后继状态补一个空转动作或确认这确实是你要的死锁命令行加-deadlock可以关掉这项检查状态数暴涨、内存爆掉某变量未被约束逐个动作检查是否漏了或UNCHANGED求值异常、提示未定义用了 TLC 不支持的语法看异常里的行号确认算子作用域TLC模块要EXTENDSunknown configuration item.cfg字段名拼错核对SPECIFICATION/INVARIANT/CONSTANTS拼写进程状态永远是初始值动作前提条件写错、永远不可达用覆盖度检查每个动作的执行次数其中某变量未被约束这条要特别说一句它的表现往往不是干脆报错而是状态空间莫名其妙膨胀或者给你一个包含大量无意义跳转的反例轨迹。遇到这两种症状第一件事就是回到Next把每个动作涉及的所有变量列一遍。7. 把 TLA 塞进日常开发流程的三种低成本用法不用一开始就搞全系统形式化验证那是另一个量级的投入。我实际用下来性价比最高的有三种场景。第一种是把并发逻辑的草图先写成 TLA 再写代码。尤其是涉及多个执行体、多把锁、超时重试这种东西。写规约的时间大概是写代码的三分之一但它能在你还没写一行生产代码的时候把设计缺陷暴露出来。上面那个FlagOnly就是典型——如果当初先写 20 行规约能省掉我两天。第二种是排查偶发 bug 时把怀疑的时序写成反例去验证。具体做法是先按我以为的实现建个模型让 TLC 跑一遍看能不能重现那个偶发症状。如果能重现反例轨迹就是给你的排查路线图如果不能说明你对代码的理解和实际实现之间有偏差这本身就是重要信息。第三种是把原子性假设写进代码注释。这个不需要跑 TLC只需要养成一个习惯每次写涉及共享状态的代码明确标出这一段的原子性由什么保证。如果某一段你写不出这个保证那就是一个潜在隐患。这个习惯是我从建模里带出来最有用的副产品。最后分享一个上手阶段的小技巧先改坏再改好。故意把你认为最关键的某一行删掉比如 Peterson 里那个turn Other(i)跑一下看 TLC 报什么错、反例轨迹长什么样。这样做三五次之后你读反例轨迹的速度会明显快起来——因为你会开始预判TLC 会给你哪条路径。这种直觉在真正排查自己模型问题的时候非常管用。至于活性检查、PlusCal 高层语法、以及怎么把一大坨业务代码抽象成可验证的模型那是实践二要啃的东西先把安全不变式这条线走顺。