“Model checking Part IV”这个系列走到第四篇默认你已经把基本概念过了一遍状态空间、时态逻辑、Kripke结构以及最原始的那套“穷举所有可达状态”的验证思路。可一旦你真的拿它去验证工业级系统立刻就会撞上三堵墙状态爆炸、反例不可信、抽象不收敛。这一篇我重点讲的就是把“能跑通的玩具模型”升级成“能解决实际问题的验证流程”的那部分内容包括有界模型检查、BDD 与 SAT/SMT 路线的取舍、抽象细化以及我在真项目里踩过的那些和反例有关的坑。如果你正准备把模型检查用在通信协议、分布式锁、缓存一致性模块这类系统上这篇应该比前三篇更贴近你的实际处境。我们不是要推翻前面学到的东西而是把符号编码、约束求解、反例定位这些技术串成一条能落地的工具链。1. 第四部分该聊什么从“能跑通”到“跑得深”1.1 前三部分留下的缺口前三讲通常会覆盖这几件事如何把并发系统建模成状态转移系统如何用 LTL/CTL 描述“最终会发生”“永远不会发生”这类性质以及如何用显式状态搜索去验证小规模系统。问题在于一旦状态数超过千万量级显式枚举就基本到头了。举个实际例子一个只有 20 个布尔状态变量、10 个并发组件的协议模块完整状态空间的上界就是 2 的 20 次方也就是一百多万个状态。如果带上了数据通路比如 32 位计数器、数组缓冲区那状态数奔着指数级就去了压根不是暴力搜索能扛住的。前三讲也可能提过一些符号化思路但往往只停留在理论层面告诉你 BDD 能压缩布尔函数SAT 求解器能处理可满足性问题却没有回答一个最关键的问题真遇到一个验证不过的性质你拿到的反例到底是系统里的真实缺陷还是建模时引入的假象Part IV 要补的正是这个缺口。它关注的不是“怎么写出正确的形式化定义”而是“怎么让模型检查器给出可以被工程决策信任的结论”。1.2 第四部分的核心主线这一篇的主线可以总结成一句话在有限的计算资源下把验证结论变成可战斗的信号。所谓“可战斗”包含三层意思。第一层规模要可控。不能一上来就把整个系统的所有变量全部编码进去必须知道什么时候该用 BDD什么时候该转向 SAT/SMT什么时候该做抽象。第二层反例要可用。模型检查器说“这里有错”你得能把这个错误轨迹翻译回真实系统切到仿真器或代码里复现而不是对着一个抽象的赋值组合发呆。第三层收敛要可预期。用抽象细化时不能无限循环下去每一轮都得有明确的进步信号。顺着这条主线第四部分会分别讨论符号模型检查里的两条技术路线有界模型检查的具体编码方式以及反例引导的抽象细化流程。这些主题看起来是并列的实际操作中它们是互补的。通常的做法是先用有界模型检查快速找反例找到可疑路径后再用更精确的符号方法确认最后如果系统规模实在太大再用抽象把无关细节剥掉。1.3 适用边界这套技术不是万能药要说清楚适用范围得先泼一盆冷水模型检查适合验证“有限状态系统”的性质不是所有软件都能套用。如果系统有动态创建进程、无界队列、复杂浮点运算模型检查的直接效果就很差。Part IV 里的内容主要面向的是以下几类场景场景典型特征推荐路线顺序电路控制逻辑同步时钟、寄存器状态有限BDD 符号模型检查通信协议状态机并发有限状态机消息类型有限SAT 有界模型检查 增量求解带数据路径的协议计数器、数组、整数参与判断SMT 求解 谓词抽象软件模块的轻量验证循环边界可控变量取值有限先抽象再验证再用反例定位表格里的分类不是绝对的但它能帮你快速判断第一刀切在哪里。如果你的系统带有大量算术运算却一上来就选纯 BDD 路线大概率会在中间节点爆炸上卡死。反过来如果系统主要是同步控制逻辑非要绕道 SMT 做位向量展开反而把简单问题复杂化。技术选型没有绝对优劣只有匹配不匹配。2. 符号模型检查的两条路线BDD 与 SAT/SMT 怎么选2.1 BDD 为什么是经典底牌BDD全称二叉决策图它做的事情是把一个布尔函数表示成有向无环图。同一个函数在特定变量序下可能被压缩得非常小也可能膨胀得巨大。模型检查领域里BDD 最经典的应用是符号化表示状态集合和转移关系然后通过不动点计算得出所有可达状态。因为很多实际系统的状态集合并不是随机分布而是有很强的结构性BDD 能把指数级的状态空间压缩成可操作的多项式级表示。我个人的经验是BDD 在同步有限状态机上表现特别稳定。比如一个带有定时器、模式寄存器、输入缓存的状态机只要变量序选得好中间节点数往往只有状态数开根号左右的量级。这里“变量序选得好”是门手艺。同样的逻辑变量序不同BDD 大小可能差出几个数量级。实际操作中把控制变量放在前面、数据变量放在后面或者按状态寄存器的时钟层级排列通常比随机排序靠谱得多。BDD 路线的代价也很明显。第一它需要一次性构建出整个不动点过程需要的结构内存峰值可能很高。第二变量序搜索本身是 NP 难问题工程上靠启发式和人工经验。第三一旦系统加入了复杂的算术比较BDD 表示位向量的乘法运算时节点数会迅速膨胀。所以如果你验证的对象是带 32 位计数器、有乘除法运算的数据通路纯 BDD 不是一个好主意。2.2 SAT/SMT 有界验证不追求全集先找反例有界模型检查的思路和 BDD 完全不一样。它不去显式构造所有可达状态而是把“是否存在一个长度不超过 k 的路径使得某个坏性质发生”编码成布尔可满足性问题然后用 SAT 求解器去解。为什么这个思路有效因为实际项目中绝大多数错误都能在比较短的路径里暴露出来。你不需要证明整个状态空间都安全只需要证明系统在图模型检查深度 k 步内没有反例或者找到一个反例。把路径长度定为 k 之后验证条件是一个巨大的命题公式。这个公式的规模随 k 线性增长但变量数和子句数都不算夸张。真正让 SAT 路线跑得快的原因有两个。第一现代 SAT 求解器基于 CDCL 算法它能从冲突中学到新子句大幅剪枝。第二增量求解机制很关键。验证 k 步时求解器保留前一轮学习到的冲突子句在验证 k1 步时重用这样每增加一步只需新增少量约束而不是从头再来。SMT 则更进一步。它不只是布尔逻辑能直接处理整数、实数、数组、位向量等理论。比如一个协议里有counter 0的判断SMT 求解器能直接对算术不等式做推理不需要先展开成 32 个布尔变量。这给软件验证带来了很大方便。实际工程中我经常用 SMT 路线的模型检查器去验证带路径条件的分布式模块效率比纯 SAT 高很多。2.3 选型经验法则我做了不少项目之后总结出一张自己的选型表不一定放之四海皆准但能减少早期试错时间路线内存曲线强项弱项常用场景BDD可能中途暴涨可达性分析、全局安全证明变量序敏感算术展开困难同步控制器、状态机SAT随 k 近似线性找短反例极快支持增量证明无法直接处理复杂算术协议、乱序执行验证SMT与理论复杂度相关整数、数组、位向量混合建模特定理论组合可能不可判定/较慢软件验证、数据通路选型时我一般先问三个问题。第一个我要证明的是“有反例”还是“无反例”如果是找反例SAT 是首选路径长度可以逐步拉长。如果是要证明全局安全BDD 的全可达状态计算更直接。第二个系统里的数据是否高度结构化计数器、指针、数组频繁参与条件判断那就别硬编码成位向量直接上 SMT。第三个并发交互是否复杂并发组件多了以后公平性约束特别重要SAT/SMT 在加公平约束时比 BDD 方便得多。3. 有界模型检查实操从建模到反例定位3.1 状态机建模把系统翻译成转移关系有界模型检查的第一步是把原始系统整理成三个部分状态变量、初始状态谓词、转移关系谓词。很多人容易在这里图省事直接把代码里的变量全部罗列出来。这样做不是不行而是会带来两个问题一是状态变量太多求解器压力大二是无效变量会把反例轨迹搅得特别乱很难定位到真正的错误点。我用一个简化例子说明建模骨架。假设要验证某个模块的“半计数”逻辑模式为 0 时计数器加一模式为 1 时计数器减半并且我们要求计数器不会在模式 1 时取到 1。# 概念性建模示意不代表具体工具语法 state_vars [counter, mode, buf] init And( Eq(counter, 0), Eq(mode, 0), Eq(buf, 0) ) trans Or( # 模式 0计数加一模式切换到 1 And(Eq(mode, 0), Eq(next(mode), 1), Eq(next(counter), counter 1)), # 模式 1计数取半模式切换到 0 And(Eq(mode, 1), Eq(next(mode), 0), Eq(next(counter), int(counter / 2))) ) safety Not(And(Eq(counter, 1), Eq(mode, 1)))这段示意代码看起来简单但有两个细节值得强调。第一我用next(counter)表示下一时刻的状态变量转移关系必须显式约束每个状态变量的下一状态值。漏掉任何一个状态变量的更新求解器就会自动把它当作自由变量反例里会出现“变量凭空变化”的现象。第二转移关系要保证是“完全的”也就是任意状态下至少有一个合法后继。如果有些状态没有后继模型检查器可能按照“死锁即错误”处理也可能自动添加自环两种情况都会干扰反例分析。3.2 展开 k 步验证条件的生成有了初始谓词 I转移谓词 T安全属性 P验证 k 步内是否存在反例的条件可以写成下面这个公式VC(k, P) I(s0) ∧ T(s0, s1) ∧ T(s1, s2) ∧ ... ∧ T(s_{k-1}, s_k) ∧ (¬P(s0) ∨ ¬P(s1) ∨ ... ∨ ¬P(s_k))这个公式读起来很直观。它要求从初始状态出发连续执行 k 次转移并且在某一步上安全属性 P 不成立。如果整个公式可满足求解器给出的一组赋值就是一个反例如果不可满足说明在 k 步以内不存在反例我们可以把 k 加一再试。实际操作中我不建议把 k 一次调得太大。先设成 10跑一遍如果没有反例再逐步翻倍。为什么这么做因为公式规模随 k 线性增加但 SAT 求解难度往往不是线性的。一次性追求 k100 可能会碰到一个超大规模问题而分步增长配合增量求解反而能在更短时间内收敛。增量求解在这里的价值是求解器保留之前学习到的冲突子句k 从 10 涨到 11 时只需要新增 T(s10, s11) 和 ¬P(s11) 的约束上一轮排掉的搜索空间不会重新探索。3.3 从 SAT 赋值到可执行反例SAT 求解器返回的赋值是一个大列表每个状态变量在每一时刻的取值、每个输入变量的取值。把它直接贴到 bug 报告里别人根本看不懂。你必须把它加工成一条可读的执行轨迹。加工过程包括三步。第一步按时间顺序抽取每一时刻的状态变量值生成s0 - s1 - ... - sk。第二步检查每一步是否都满足系统的转移关系。第三步提取出导致属性失败的“关键事件”比如在第五步模式被切换到了 1同时计数器正好等于 1。第三步往往能暴露建模问题。最常见的情况是求解器“作弊”了它把某个输入变量在某两步之间随意变化但在真实系统里输入可能是受约束的。比如协议中一条消息发出后下一周期不能立刻收到响应。如果你没在转移关系里加入这个时序约束SAT 求解器就会构造出一条现实中不可能出现的路径。所以拿到反例之后第一步不是认错而是先做“可执行性审查”。审查方法很简单把反例里的输入序列单独提出来放到系统仿真器里跑一遍看能不能复现同样的状态变化。如果复现不了问题大概率在建模约束遗漏而不是系统缺陷。反例的长度也需要优化。一般来说模型检查器给出的反例不一定最短但我们可以用 unsat core 或者二分搜索来裁剪。思路是去掉轨迹中某些中间状态看剩下的转移是否仍然可行。我通常先检查整个反例里哪些变量在整条轨迹中完全没有变化把这些变量从赋值里删掉通常就能让反例短不少。再进一步可以把 k 逐步缩小不断求解“是否存在更短反例”直到找到最短反例。最短反例的好处不只是报告好看更重要的是人眼能看得懂定位代码缺陷时效率高很多。4. 抽象与细化拿不充分的抽象换取规模4.1 状态爆炸的结构性来源状态爆炸不是随机的。它通常来自三个源头并发组合、数据位宽、无界队列。并发组件 A 有 10 个状态组件 B 有 10 个状态组合起来最多 100 个状态还勉强可控但组件数量是 5 个、10 个时组合状态数就是各组件状态数的乘积涨得非常快。数据位宽则更直接一个 32 位寄存器有 2 的 32 次方种取值哪怕只有一个这样的寄存器精确状态空间就已经大得离谱。抽象的作用就是在这三类爆炸源上“偷工减料”。它不是做假的验证而是故意丢掉一部分信息让状态空间小到可以完全验证。比如对于缓冲区我们不需要精确知道缓冲区里有几条消息只需要知道“空”“满”“非空非满”这三个状态。对于计数器很多时候只需要知道“等于 0”“大于 0”“超过阈值”而不是每一个具体整数值。这种粗粒度表示如果验证通过在真实系统里也一定是安全的前提是抽象保持了足够的安全性。这里必须说清楚“抽象”的可靠性方向。模型检查里用的一般是“过近似”也就是抽象系统包含真实系统的所有行为甚至还要多一些虚假行为。这样做保证了一件事如果抽象系统里某个坏性质不可能发生那真实系统里也一定不可能发生。反过来如果抽象系统里出现了反例这个反例可能不是真实存在的我们把它叫“假反例”。处理假反例就是下一节要讲的细化过程。4.2 CEGAR 循环反例引导抽象细化CEGAR全称是反例引导的抽象细化它把“抽象”和“验证”串成一个循环。流程大致是这样先用一组非常粗的谓词构造抽象模型比如只关心“锁是否被持有”。在抽象模型上验证目标属性。如果验证通过那就万事大吉因为抽象系统覆盖了真实系统的全部行为。如果验证失败得到一条抽象反例。把抽象反例放到真实系统里执行看它是不是真的可执行。如果真实系统也能走到这一步说明找到了真实缺陷。如果真实系统里走不通说明反例是假的分析它在哪一步失败、缺了哪个关键谓词把新谓词加进抽象模型回到第 2 步。这个循环听起来很顺但工程实现里最难的环节是第 7 步。为什么难因为一个假反例可能对应着很多种可能的细化方式。比如抽象模型只区分了“缓冲区不为空”但真实系统里一次取消息操作需要同时满足“缓冲区非空”和“当前模式是读取模式”。只加一个谓词可能消除当前这条假反例但很快会冒出另一条形状相似的反例。所以细化选择必须吃透反例被拒的根本原因而不是随便补一个看着相关的条件。我习惯把 CEGAR 里的每一轮都记录下来本轮反例的起点、终点、在哪一步被真实执行拒绝、新增了哪个谓词。如果连续三轮新增谓词后反例仍然在同一个状态附近打转我会暂停加谓词先去看抽象模型里这个状态附近的转移关系是不是整体建模有误。很多时候问题不是谓词不够多而是抽象模型里某些转移被“过度概括”了比如把本应互斥的两个动作建模成了可以同时发生。4.3 谓词选择的实际细节谓词抽象里一个经典案例是验证带锁的并发模块。最初你可能只需要三个谓词锁被持有、线程标识等于本地线程、等待队列非空。这三个谓词已经能把“两个线程同时进入临界区”这类错误暴露出来。但等你验证更复杂的公平性属性比如“某个线程最终一定会进入临界区”就需要增加关于调度顺序的谓词比如当前优先级最高、本轮已经让出过。选择谓词时有个常见的倾向把能想到的条件全都放进模型。这样做其实是把抽象模型重新推向了状态爆炸。谓词数量从个位数涨到十几二十个以后抽象状态数量按 2 的谓词数次方增长即使每个谓词只是一个布尔值20 个谓词就有一百万个抽象状态。所以在细化循环里新增谓词必须“能消灭一整类假反例”而不是只修当前这一条。检测办法是把已经拒绝掉的反例保存成回归集合加完新谓词后重新跑一遍这些旧反例如果它们还在抽象模型里出现说明细化没有命中关键条件得换一个角度。另一个实操经验是用“区间抽象”替代“值抽象”。假设系统里有一个计数器它参与counter 10的判断那么抽象时不需要保留 counter 的完整范围只需要维护几个区间counter 0、1-10、11-100、100。这样既保留了对属性判断足够的信息又避开了大位宽变量的状态爆炸。区间抽象配合谓词抽象是我在处理带数据路径协议时最常用的组合。5. 我踩过的坑反例可信度与收敛性排查5.1 反例给出却“跑不下去”建模问题还是系统问题我在验证一个分布式锁模块时遇到过一件特别折腾的事。模型检查器洋洋洒洒给出了一条 12 步反例显示锁在两步之间被两个不同线程同时持有。我拿到反例后兴奋地去仿真器里复现结果怎么跑都跑不出这个结果。折腾了大半天最后发现建模时漏了一条约束线程 A 释放锁之后锁的持有者标识必须在下一个周期才能切换给线程 B。我没有在转移关系里规定“释放操作和获取操作不能在同一个周期同时生效”于是 SAT 求解器就构造出了一条同时释放又获取的魔法路径。这个坑的通用教训是拿到反例先别急着改系统先审查模型的可执行性。检查三个地方。第一转移关系里有没有给每个输入变量加合法的时序约束比如“消息到达至少需要两个周期”。第二有没有给并发组件的交错加互斥约束。第三初始状态和立即可达状态之间有没有隐含的稳定条件。只要这三处有遗漏反例就可能是模型允许而系统不允许的伪反例。还有一个更隐蔽的问题公平性约束。并发系统验证时如果某个分支可以无限次被选择而不违反台面约束SAT 求解器可能找到一条依赖“不公平调度”的反例。真实系统里调度器不会永远饿死某个组件但模型里如果不加公平性约束验证结果就会过于保守。这时候需要在验证条件里加入公平性限制比如“每个等待中的组件在 n 步之内至少被调度一次”。5.2 细化总是不收敛追踪反例集合而非单条反例CEGAR 循环最容易出现的问题是每次新增一个谓词反例就会换一件马甲重新出现。比如第一轮的反例是“线程 A 在缓冲区满时写入”第二轮的新反例是“线程 B 在缓冲区满时写入”它们本质上是同一类问题。如果我只是机械地根据当前反例加谓词那每一轮都只补一个小窟窿永远无法收敛。我的做法是把每一条被拒绝的假反例都保存成一个独立的文件然后在下一次细化后全量回归。这个回归不是说重新跑完整模型检查而是把那批旧反例当作约束重新执行可执行性检查。如果某条旧反例在新抽象模型下依然是可行的那说明新增的谓词并没有覆盖它对应的真实拒绝原因。这时候不要继续加谓词而是把旧反例聚到一起找出它们的共同前缀在共同位置引入新的状态变量分割往往比加一堆局部谓词更有效。收敛性还有一个潜在问题抽象模型本身不是“良构”的比如转移关系里包含了从任何抽象状态到任何抽象状态的自由迁移导致假反例无穷无尽。遇到这种问题我会检查抽象转移关系是否保持了“合取精化”性质。简单理解就是真实系统里不能发生的事情抽象模型里也不能凭空冒出来。如果发现抽象转移关系过于宽松先修正转移关系的过近似程度再考虑增加谓词。5.3 资源受限超时后的第一反应不是加内存模型检查器超时是家常便饭。很多人第一反应是把内存调大、把超时阈值调大或者干脆换一台更强的机器。但在工业项目里我更看重的是先用逻辑手段排除不必要的计算量。对于 SAT/SMT 有界模型检查最重要的一个概念是“验证深度”。验证到 k 步没有反例只能说明这一长度内没有缺陷但不等于系统全局安全。要得到全局结论必须让 k 超过系统的最长简单路径长度也就是系统状态的“直径”。如果你能证明状态的直径不超过某个上界那么验证到那个边界即可收工否则就得说明白“只保证 k 步内的安全”。增量求解在这种场景下特别划算。我通常会做一个循环k 从 10 开始每次增加 5求解器复用上一轮学到的冲突子句。图上显示在前 20 次迭代里大部分时间耗在变量决策上真正的排序和预处理开销反而小。后来我发现把求解器的“活跃变量阈值”调高一点让频繁出现的决策变量更快被赋值能让很多协议性质的验证时间直接减半。这类参数调整没有通用最优值只能在你的特定例子上做网格式小实验。对称性破缺是另一个常常被忽略的提速点。许多协议的多个副本行为是完全相同的比如一组同类客户端、一组同类服务端。如果你不告诉求解器这些副本是对称的它会把本质相同的错误在每种排列下各找一遍浪费大量时间。工程上常用一种简单的对称性破缺手段给每个副本分配一个静态序号并增加约束“副本 i 的某关键变量 副本 i1 的某关键变量”。这个约束看起来是加了条件实际是让求解器不再枚举对称重复的解效果非常明显。回到这一部分开头提到的那个分布式锁项目。最终让我定位到根因的不是某一轮新增的复杂谓词也不是更快的求解器而是我很朴素地把一条反例切成了一段 4 步的最小核心在仿真器里逐步对比每一步的系统状态。那一次经历让我彻底明白模型检查工具解决的是“从海量状态里找出一条致命轨迹”的问题而工程师解决的是“让这条轨迹在真实系统里能走通”的问题。这两件事结合起来才是一次有说服力的验证。后续我再做协议验证时都会规定自己拿到反例后先做三步查输入约束、查公平性、查可复现性。过程很机械但从来不会白费功夫。