极客工场

Appearance

共 2,748 字预计阅读约 9 分钟

Formality 偶发不确定失败：同一脚本两次 verify 结果不同排查速查 ​

更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。Formality 最折磨人的失败不是稳定报错——稳定报错照表查就行——而是同一设计、同一脚本，昨天 pass 今天 fail，换台机器又 pass。这类「薛定谔的 verify」九成因不在工具而在环境：超时边界的任务被负载推过线、两台机器库版本差了一个小版本、NFS 读抖了一下、并行度把内存顶到临界点。排查方法论只有一条主线：先把环境固化到能稳定复现，再谈定位。真超时（稳定复现、每次都卡同一处）的线见 Formality 运行卡死/超时，资源直接爆掉的线见 Formality 资源耗尽。

本文要回答的问题 ​

  • 同一脚本两次 verify，一次 pass 一次 inconclusive，是谁在抖？
  • failing point 时有时无，和机器负载、超时设置是什么关系？
  • 多台回归机器结果不一致，怎么判断是库版本还是环境变量差异？
  • 怎么固化环境、做出最小复现，把「偶发」变「必现」？

一、报错原文与现象 ​

text
Info: Verifying ...
***** Verification completed with 1 failing point *****
Error: 1 failing compare point: r:/WORK/top/u_cnt/out[3]  (FM-370)
（隔天同一 commit 重跑）
***** Verification is successful. *****
Status:  SUCCEEDED

偶发问题的现场特征：错误内容每次都「像真的」——failing point 有名字、有锥逻辑、能单独 report，但它只在某些运行里出现。先锚定三件事：这次失败跑在哪台机器、当时负载多少、用的哪份库。答案多半在这三个变量的组合里。

二、可能原因总览 ​

现象特征可能原因处置
负载高时 inconclusive/fail、空闲时 passverification_timeout 压在边界，负载把任务推过线超时放宽到 p95 两倍、错峰回归
换台机器结果就不同回归池各机 Formality 版本或补丁不一致统一版本、启动时 transcript 打版本号
偶发读文件失败或内容对不上NFS 抖动/缓存读到旧网表输入产物挪本地盘、校验 md5
多路并行时挂、单跑正常并行任务把内存/句柄顶到临界点单机并发数降档、ulimit 对齐
同机同人两次结果不同TMPDIR、ulimit、环境变量被 shell 初始化改动提交脚本显式 env -i 白名单起环境
effort low 时 fail、调高就 pass难点锥在 effort 边界，求解器路径不稳定难点区域单独加 effort 并记录
inconclusive 比例随时间段波动license 借用/共享机器 IO 争抢放大运行时长固定回归时间窗、IO 错峰

三、逐条排查展开 ​

第一条线：超时边界的任务被负载推过线，是偶发 fail 的头号嫌疑。 verification_timeout 按「上次跑完时间」拍脑袋设的值，往往就压在边界上——机器空闲时 verify 在 58 分钟收工，负载一高就撞 60 分钟的线，超时按 inconclusive 收场，而 inconclusive 里的难点锥有时被报成 failing point。判别：把失败时段的机器负载（uptime / 调度系统记录）调出来，和空闲时段对比；失败的 verify 耗时是否紧贴 timeout。处置：超时改按历史分段耗时的 p95 两倍校准，failing 与 inconclusive 分开统计——前者是真不等价，后者只是没跑完，不能混为一谈。

第二条线：多台机器结果不一致，先对版本再对库。 回归池里有的机器装着 2024.09、有的装着 2025.06，小版本之间求解器启发式不同，边界锥的结论就可能翻转；更隐蔽的是库文件——某台机器 NFS 挂载的库目录被人更新了一半。判别：transcript 开头的版本横幅、对输入文件算 md5 逐机对比。处置：回归池版本统一切齐，启动脚本里显式 which fm_shell 与版本号落盘；库版本协商问题见 Formality 版本不匹配。

第三条线：NFS 抖动让「读到的设计」本身不一致。 网表写在 NFS 上，上游综合还在写、Formality 就开始读，读到的是截断或新旧混合的内容；NFS 属性缓存也会让刚更新的文件读到旧版本。形态是偶发且无法复现——因为第二次跑时文件已经写完了。判别：失败 run 的输入文件 md5 与成功 run 不同，或读取时间戳紧贴上游写入完成时间。处置：输入产物先 rsync 到本地盘再跑，或对上游产物做「写完标志文件 + md5 校验」两道闸。

第四条线：并行度把资源顶到临界点。 单机同时塞 8 路 Formality，单路正常时内存占一半，齐发时互相挤到 swap、IO 排队、句柄耗尽——每一路单独看都「偶发」，合在一起是必现的。判别：失败是否集中在多任务齐发时段；dmesg 里有没有 OOM 痕迹。处置：单机并发数按物理内存除以单路峰值 RSS 降档，ulimit（虚拟内存、句柄、栈）在提交脚本里显式设定，别继承提交者的交互 shell 配置。资源形态与超限处置详见 Formality 资源耗尽。

第五条线：环境变量差异是最容易被忽略的抖动源。 TMPDIR 指到快满的盘、ulimit 在不同登录方式下不同、LD_LIBRARY_PATH 被某个项目的环境模块改过——这些都不会让 fm_shell 起不来，只会让行为微妙地不同。判别：失败与成功两次的 env 输出 diff。处置：提交脚本用 env -i 加白名单变量起干净环境，把「环境」本身纳入版本管理。

第六条线：effort 与求解器路径的固有不确定性。 effort low 下求解器走启发式捷径，同一个难点锥这次证出来了、下次没证出来，结论在 pass 与 inconclusive 之间晃。这不是 bug，是 effort 预算与问题难度的关系。处置：难点区域单独 set_dont_verify 摘出来加 effort 专项攻关；effort 选择本身要进脚本版本管理，不允许「手工调一下试试」不留痕。

下图把六条线的分流逻辑画成一张决策图，先看它再动手。

eda/ts-formality-flaky-nondeterministic.md D2 示意图

颜色按语义分角色：红是偶发失败这个入口现象，蓝是排查分流动作（先固定机器、负载、库这三个变量再按形态分线），橙是五条修复动作各自落地，绿是「难点锥单独加 effort」这条确认设计侧问题后的专项通道，紫是收尾——把固化环境与最小复现沉淀成档案。主线是：不固定环境就谈不上排查，先把机器、库、环境变量三件事钉死，剩下的偶发自然会收敛成必现。

四、固化环境与最小复现方法论 ​

偶发问题的终局只有两种：收敛成必现，或者证明是环境扰动并消除扰动源。操作次序固定：

  1. 钉死环境：同机、同库、同脚本、同环境变量（env -i 白名单）、单机独占（无并行任务），连跑三次。三次结果一致，偶发变必现，按常规 failing point 流程排查；三次仍不一致，扰动在更底层（IO、内核调度、共享存储），继续往下钉。
  2. 最小复现：把 failing point 用 set_dont_verify 反向隔离——先摘掉其他所有 compare point 只留这一个，看是否还偶发。复现成本从「全设计几小时」降到「单锥几分钟」，迭代速度完全不同。
  3. 记录 diff 而不是记录结论：每次失败落盘的不只是 pass/fail，而是机器名、负载、版本横幅、输入 md5、env 全量、耗时。偶发问题靠横向 diff 这堆元数据定位，不靠盯着单次 transcript 冥想。
  4. 回归结果要留痕：历史回归结果丢失会让「这个问题从哪天开始出现」无法回答，回归产物的保留纪律见 Formality 回归结果丢失。

五、预防与纪律 ​

  • 超时按 p95 两倍校准：不拍脑袋设 verification_timeout，failing 与 inconclusive 分开统计、分开处置。
  • 回归池版本统一切齐：版本横幅每次落盘，池内不允许存在第二个小版本。
  • 输入产物本地盘化加 md5 校验：NFS 只做归档不做在线读取，上游产物带写完标志。
  • 提交脚本 env -i 白名单：ulimit、TMPDIR、LD_LIBRARY_PATH 显式设定，环境纳入版本管理。
  • 单机并发按内存配额：并发数等于物理内存除以单路峰值 RSS，写进调度配置不靠自觉。
  • effort 选择进脚本版本管理：任何 effort 调整必须留痕可回滚，禁止口头「调一下试试」。

这一篇在知识体系里的位置 ​

本篇是 EDA 排错速查簇中「Formality 偶发不确定失败」节点的 FAQ 页：稳定复现的卡死与超时见 Formality 运行卡死/超时，资源超限的确定形态见 Formality 资源耗尽，库与工具版本协商见 Formality 版本不匹配，回归产物保留纪律见 Formality 回归结果丢失。

一句话总结 ​

Formality 偶发不确定失败的根因九成因在环境而不在工具：超时边界被负载推过线、回归池版本不一致、NFS 抖动读到混合内容、并行顶到资源临界点、环境变量被 shell 初始化改动、effort 预算压在难度边界——排查主线是先钉死机器、库、环境变量三个变量把偶发收敛成必现，再用 set_dont_verify 做最小复现、靠元数据横向 diff 定位扰动源，长期靠超时校准、版本切齐、输入本地化、env 白名单与并发配额五件套让每次失败都能当场复现。