Formality 磁盘写满速查：No space left on device 与 fm_shell 日志失控处置
更新时间：2026-10-23。FAQ 速查页，面向在共享 Linux 服务器上跑 Formality 形式验证（LEC）回归的入门同学。fm_shell 是典型的「悄悄吃盘」型 EDA 工具：transcript 日志随比对规模无限增长，svf 引导文件一份接一份，自动保存点（checkpoint）按阶段落盘，再加上崩溃时几个 GB 的 core，回归跑一夜把卷打穿并不稀奇。盘满直说时是一句
No space left on device，阴损时比对中途断掉、日志与数据库写了半截，下一轮 fm_shell 读到残文件报的是另一类错误，排查方向容易被带偏。内存与句柄维度（报的是 memory 而非 disk）由 Formality 资源耗尽速查 分工，写满导致进程崩溃的善后见 Formality 段错误崩溃速查，同主题在 SpyGlass 阵营的对照处置见 SpyGlass 磁盘写满速查。
本文要回答的问题
- fm_shell 比对中途报
No space left on device，先救场还是先重跑？ df -h看着还有空间，Formality 为什么还是写不进文件？- 工作目录里到底是谁在吃盘：transcript、svf、core、保存点各占多少？
- NFS 上卷没满却写失败，quota 与个人配额怎么查？
- 回归批量跑时，work 目录与日志的轮转纪律怎么定？
一、报错原文与典型现象
最常见的是写出阶段直接失败，工作目录以 /proj/fm 占位：
Error: Cannot write file "/proj/fm/logs/formality.log":
No space left on device
Error: Unable to save container "/proj/fm/work/FM_CONTAINER": disk full第二种现场在 transcript 与 svf 阶段。日志或引导文件写到一半失败，下一轮 set_svf 或恢复保存点时报的是文件不完整或格式错误：
Error: write failed on "/proj/fm/svf/default.svf"
Error: file "/proj/fm/svf/default.svf" is truncated or corrupted还有三种容易误判的形态。一是 core dump：fm_shell 崩溃时若 ulimit -c 不限大，大设计的 core 单份就是几个 GB，崩两次盘就穿；二是 /tmp 小分区：TMPDIR 没指到大分区，fm_shell 的中间临时文件把系统小分区撑爆，df -h /proj/fm 看着没事但 /tmp 已 100%；三是 NFS 配额：共享卷 df 有空闲，但个人 quota 触顶，写任何文件都失败。要警惕「二次故障」：盘满当次没注意，下一轮读到写了半截的 svf 或容器，报的是损坏类新错误——看到这类报错先回头翻上一轮 transcript 尾部有没有 No space left。
二、占盘大户与病因处置表
| 占盘来源 | 典型位置 | 体量与特征 | 处置 |
|---|---|---|---|
| transcript 日志 | formality.log、各 run 的 transcript | 大设计逐点比对时无限增长，单份可达 GB | 冗余打印关掉，抓完结论归档压缩 |
| core dump | 工作目录或 core_pattern 指定路径 | 崩溃一次数 GB | 日常 ulimit -c 0，排错时按需临时开 |
| svf 引导文件 | svf/ 目录 | 每轮综合/比对一份，长期累积 | 按里程碑保留，老 svf 整批清理 |
| 自动保存点 | work/ 下容器与 checkpoint | 分阶段落盘，回归多轮堆积 | 只留最近 N 轮，跑完即清中间点 |
| 临时文件 | /tmp、TMPDIR 指向分区 | 大设计中间文件撑爆小分区 | TMPDIR 重指大盘，跑完即清 |
| NFS 个人配额 | 家目录与共享卷 | 卷有空闲但个人 quota 满 | quota -s 查限，清理或申请提额 |
| work 目录堆积 | 每次 run 一套工作区 | 回归一夜几十个 run 各数百 MB | 轮转删除，只保留最近 N 轮 |
| inode 耗尽 | 小文件密集的工作目录 | df -h 有余量、df -i 100% | 整目录清小文件，不逐个大文件删 |
表中体量均为典型量级，具体数字以设计规模与所用 Formality 版本（如 2025.06）为准。
三、排查决策图
先判「容量满、inode 满还是配额满」，再用 du 定位大头，最后才动手清理——顺序反了会白删文件。
读这张图抓住一次分叉：红色入口先经蓝色三线同查，切成「容量满」与「inode/配额满」两条互不相干的通道，再汇入蓝色的 du 下钻定位。红色只标现象与命中的根因，蓝色全是排查动作，橙色是这一次的救火动作，紫色闭环是从失败阶段重跑并沉淀防复发策略。不要跳过三线同查直接删大日志——inode 耗尽或配额触顶时删几个 GB 的 transcript 毫无作用，得清小文件密集的整棵工作目录或找存储管理员提配额。
四、逐条排查展开
第一刀：容量、inode、配额三条线一起看。 在工作目录敲：
df -h /proj/fm # 工作卷容量水位
df -h /tmp # TMPDIR 所在分区水位
df -i /proj/fm # 同一卷 inode 水位
quota -s # NFS/共享卷个人配额
du -h --max-depth=2 /proj/fm 2>/dev/null | sort -rh | head -20Use% 打到 100% 是容量写穿，注意要单独看 /tmp——TMPDIR 没重指时 fm_shell 把大中间文件全压在系统小分区上；df -h 还空着但 IUse% 100%，是工作目录里海量小文件吃光了 inode；quota -s 报超限则是卷没满、个人配额满了，这时 df 完全正常，最容易误判。
第二刀：work 目录与保存点轮转，回归场景的头号大户。 回归脚本每夜批量跑，每轮留一套完整工作区（容器 + checkpoint + 日志），几十轮下来轻松吃掉数百 GB。处置口径：回归收尾脚本里加轮转，只保留最近 N 轮（常见取 5 至 10）与标记为里程碑的轮次，其余整目录删除；正在跑的 run 不能动，先确认 fm_shell 进程已退出。手动清时按时间戳排序：ls -dt run_* | tail -n +11 | xargs rm -rf，删前先确认没有人在翻旧结果。中间阶段的自动保存点在比对通过后就没有保留价值，收尾脚本里一并清。
第三刀：transcript、core 与 TMPDIR，三个隐形炸弹。 transcript 在逐点比对大设计时无限膨胀，日常回归把冗余打印关掉（减少无谓的逐行 message），只在定位具体不收敛点时临时开 verbose，抓完结论把日志 gzip 归档再清原文。core dump 默认在崩溃时落盘，日常环境 ulimit -c 0 直接关掉，真要抓崩溃现场再临时打开并指到大盘；历史 core 用 find /proj/fm -name "core*" -size +1G 翻出来删掉。TMPDIR 在跑大设计前显式重指：export TMPDIR=/proj/fm/tmp，并在 run 脚本收尾清理该目录。
顺手交代一句救场顺序：盘满导致 run 中断时，先腾空间再重跑，不要在没腾空间的情况下反复 retry——每次 retry 都会再写一轮半截文件，把盘压得更死，也让后续定位哪份结果可信变得更难。
第四刀：svf 与日志归档，清不动就挪。 svf 是综合传给 Formality 的引导文件，里程碑流片前的轮次要留，日常回归轮次的老 svf 可整批清理；清理前确认对应轮次的报告已归档。日志长期留存一律 gzip 压缩，文本日志压缩率常在九成以上。共享服务器上把 run 工作区从家目录挪到数据卷，家目录配额通常最紧。
五、预防与纪律
- work 目录轮转进脚本：回归收尾自动只留最近 N 轮，里程碑轮次打标签豁免。
- transcript 默认精简：verbose 只在定位问题时临时开，抓完即压缩归档。
- core 默认关：日常
ulimit -c 0，抓崩溃现场再临时开并指大盘。 - TMPDIR 显式重指：跑前
export TMPDIR到大分区，收尾清理。 - svf 按里程碑保留：日常轮次老 svf 整批清，流片相关轮次例外。
- 定期巡检：
du与quota -s纳入例行检查，工作卷预留约 20% 空闲容纳单轮回归峰值。
这一篇在知识体系里的位置
本篇是 EDA 工具排错速查簇的 FAQ 页，专管 Formality 磁盘容量、inode、配额一条线；内存与句柄类资源耗尽（报的是 memory 而非 disk）在 Formality 资源耗尽速查，写满导致进程崩溃的善后见 Formality 段错误崩溃速查，同主题在 SpyGlass 阵营的对照处置见 SpyGlass 磁盘写满速查。
一句话总结
Formality 磁盘写满先 df -h（含 /tmp）、df -i、quota -s 三线同查容量、inode 与配额，再用 du 下钻锁定 transcript 无限增长、core dump、svf 堆积、自动保存点、TMPDIR 小分区与 work 目录堆积这几类大户：work 目录按只留最近 N 轮轮转删除、日志精简并压缩归档、core 日常关闭、TMPDIR 重指大盘，写穿当次的半截 svf 与容器不可信、腾空间后从失败阶段整链重跑，长期靠回归脚本内置轮转清理与定期 du 巡检两条纪律防复发。