极客工场

Appearance

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

Formality 回归结果丢失：夜间验证报告缺失速查 ​

更新时间：2026-10-23。FAQ 速查页，属于 EDA 工具排错系列。早上来收昨晚的 Formality 等价性验证回归结果，打开结果目录一看：有的 case 报告文件根本不存在，有的目录整个空了，还有的只剩下最后一次重跑的产物、前一轮的结果不翼而飞。fm_shell 自己的 log 可能写得挺正常，断点往往不在工具而在回归脚本与环境。六成以上是「产物去哪了」的工程问题而非 Formality 本身：清理脚本误删、并发互踩、相对路径落错目录。退出码本身的排查见 Formality 退出码非零，路径类报错的专项见 Formality 路径不存在。

本文要回答的问题 ​

  • fm_shell log 显示验证完成，为什么报告文件不在预期目录里？
  • 只剩最后一次 run 的产物，前一轮结果去哪了？
  • 手工跑一切正常，交给 crontab 跑就丢结果，差在哪？
  • 共享工作区上两个回归并发跑，会互相踩掉对方的产物吗？
  • 怎么让「结果丢失」本身变成一个可见的失败，而不是早上才发现？

一、报错原文与现象 ​

bash
# 结果目录现场
results/2026-10-22/blk_a/  fm_shell.log 存在，缺 reports/pass_fail.rpt
results/2026-10-22/blk_b/  目录存在但内容为空
results/2026-10-22/blk_c/  只有 rerun 一次的产物，首轮结果被覆盖
# fm_shell log 尾部（看着正常）
Info: Verification finished.  (FMR-003)
# 回归脚本 stderr（被忽略的线索）
rm: cannot remove '/proj/fm_runs/blk_b': Directory not empty
mv: cannot stat './reports/pass_fail.rpt': No such file or directory

先校准一个直觉：「log 显示验证完成」只证明 fm_shell 进程走完了，不证明产物落到了你以为的目录。Formality 回归丢结果的排查主线是顺着「fm_shell run → 报告落盘 → 搬运到结果目录 → 归档留存」这条链找断点，每一环都有自己的典型死因。尤其注意 crontab 场景：手工跑和定时跑的环境差异（启动目录、环境变量、挂载可见性）是这类故障的高发区。

二、可能原因总览 ​

现象可能原因处置
整个批次目录空缺共享工作区的定时清理脚本把回归产物当临时文件删了产物目录与临时目录分区，清理脚本加白名单
只剩最后一次 run同名工作目录复用，失败重跑直接覆盖首轮结果工作目录带 run id 或时间戳，禁止复用
crontab 跑丢、手工跑正常crontab 启动目录与手工不同，相对路径产物落错地方脚本开头显式 cd，输出路径全部绝对化
相邻两个 case 结果串了两个回归并发写同一工作目录互踩并发隔离目录或加互斥锁
最后几个 case 缺报告磁盘或配额在回归中段写满，后段写不出磁盘门槛前置检查，专项见磁盘写满篇
归档区长期查不到历史结果没有归档留存策略，结果跑完即被清理按日期目录归档，只读留存区

三、逐条排查展开 ​

清理脚本误删：整批蒸发。 很多团队在工作区上挂了定时清理脚本（清 N 天前的临时文件、清大目录），Formality 回归产物目录的命名或位置恰好落在清理范围内，凌晨回归刚跑完，早上清理脚本就把它当垃圾扫掉了。特征：结果目录的修改时间停在清理脚本的运行时刻之后，系统日志里能翻到对应的 rm 记录；丢的不是个别 case 而是整片目录。处置：产物目录与临时工作目录物理分区（如 results/ 与 scratch/ 分开），清理脚本只扫 scratch 区并加路径白名单；任何「自动删除」逻辑上线前先跑一周 dry-run 只记录不真删。

工作目录复用：重跑覆盖首轮。 回归脚本给每个 case 分配固定名字的工作目录（如 runs/blk_c/），同一 case 当晚被跑了两次（首轮失败后自动重试），第二次启动时把目录清掉重来。如果首轮其实成功了、重跑反而失败，你就拿一份好结果换了一份空目录。特征：目录内所有文件时间戳都集中在最后一次 run 的时间窗，log 开头是干净的工具启动横幅。处置：工作目录固定带「case 名 + run id/时间戳」两段命名，历史 run 保留到汇总确认后再统一清理；失败重跑写入新目录而不是清空旧目录。

相对路径与 crontab 工作目录假设。 这是「手工跑正常、定时跑丢结果」的头号根因：回归脚本里写了相对路径的输出目录（如 ./reports/），手工跑时你站在工程根目录，产物落在预期位置；crontab 启动时工作目录是 HOME 或 crond 的默认目录，产物全落到那边去了，甚至因为权限不够写失败。特征：crontab 跑的批在预期目录全空，但在 HOME 或某个莫名目录里能找到散落的报告文件；fm_shell 报「cannot open file」类错误时路径显示为相对形态，与 Formality 路径不存在 的现场一致。处置：回归脚本第一行显式 cd 到工程根目录，所有输入输出路径绝对化；crontab 条目里把环境准备（module load、环境变量）写全，不依赖登录 shell 的配置。

并发互踩：两个回归写同一目录。 共享工作区上两条回归流水线并发跑（比如 nightly 与人工触发的补测），脚本用了同一套固定工作目录，两边交替写同一批文件，产物互相覆盖甚至写一半被对家清掉。特征：缺失或错乱的 case 每次都不一样（竞态无规律），log 里能看到时间戳交错的两段工具输出。处置：工作目录按「回归实例 id」隔离，天然不重名；必须共享的目录加文件锁，但 NFS 上锁并不可靠，隔离目录才是正解。

磁盘满：前段正常后段失踪。 磁盘或配额在回归中段写满，前面跑完的 case 报告齐全，之后的 run 写报告失败——fm_shell 写不出报告不一定让整个进程崩，可能只打一条告警继续跑完，回归脚本没检查产物存在性就一路绿灯。特征：缺失的 case 全部集中在时间线后段，df 显示磁盘满或刚被清理出空间。处置：回归开始前检查磁盘余量门槛，不足拒跑并报警；每个 run 收尾校验产物件数与大小。专项排查见 Formality 磁盘写满。

归档留存缺失：跑完即清。 结果当天都在，但一周后想回查某个历史回归，发现结果目录已被例行清理——团队没有归档策略，结果目录本身就是临时区。特征：近期结果齐全、历史结果按清理周期成片缺失。处置：建立「按日期目录归档 + 只读留存区」机制——回归收尾把关键产物（报告、log、session 摘要）拷入 archive/YYYY-MM-DD/ 结构的只读区，工作区结果只保留最近 N 天；归档后做件数对账，对不上即报警，不许静默。

eda/ts-formality-regression-result-missing.md D2 示意图

颜色按语义分角色：红是入口现象与三类已定位的根因，蓝是排查动作，绿是「该环节排除、转下一环」或修复验证通过的分流判定，橙是修复动作，紫是防复发收尾。主线是「先定位产物在哪、再追查谁动了它」：第一步永远是确认 fm_shell 到底把报告写去了哪个目录（相对路径问题在这一步现形），位置对了再查目录被谁清掉或盖掉（清理脚本、重跑、并发三类嫌疑），最后才落到归档留存这类长期机制——按这个顺序查，不会被「log 看着正常」带偏。

四、预防与纪律 ​

  • 产物存在性断言：每个 case 结束既查 fm_shell 退出码，又查关键报告文件存在且非空，任一失败即标 FAIL，退出码语义见 Formality 退出码非零。
  • 路径绝对化：回归脚本第一行显式 cd 到工程根目录，输入输出路径全部写绝对路径；crontab 条目自带完整环境准备。
  • 目录唯一化：case 名 + run id 两段命名，失败重跑写新目录，历史 run 保留到汇总确认后再清。
  • 产物与临时区分区：清理脚本只扫临时区并加白名单，自动删除逻辑先 dry-run 一周。
  • 并发隔离：回归实例级目录隔离，不依赖 NFS 文件锁。
  • 归档留存：按日期目录归档进只读留存区，归档后件数对账，「提交 N 个 case、回收 N 份报告」的闭环每次回归自动跑，差集直接报警。

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

本篇是 EDA 排错速查簇中 Formality 系列的「回归结果闭环」FAQ 页：退出码语义见 Formality 退出码非零，路径类报错专项见 Formality 路径不存在，磁盘写满专项见 Formality 磁盘写满；同型问题在 lint 工具侧的对照页见 SpyGlass 回归结果丢失。

一句话总结 ​

Formality 回归结果丢失先认「log 正常不等于产物在位」这个锚点，再按链逐环排查：共享工作区被清理脚本误删、同名目录被失败重跑覆盖、相对路径在 crontab 下落到错误启动目录、并发回归互踩同一工作目录、磁盘满只丢后段 case、没有归档留存策略导致历史结果跑完即清；治本靠每个 case 的「退出码 + 产物存在性」双断言、路径绝对化、目录唯一化和「按日期归档 + 件数对账」，让结果缺失本身成为一个显式报警的失败。