💻 computer science

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

本文提出了一种结合小步和大步语义的验证方法，通过引入抽象行为语义接口并扩展共归纳大步语义以处理发散，成功在 CompCert 编译器中实现了包括循环展开在内的多种循环优化，同时确保了语义保持定理的完整性。

原作者： David Knothe, Oliver Bringmann

发布于 2026-02-24

📖 1 分钟阅读☕ 轻松阅读

原作者： David Knothe, Oliver Bringmann

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个关于**如何更聪明地给编译器“做手术”**的故事。

想象一下，编译器就像一位超级厨师，它的任务是把人类写的菜谱（源代码）翻译成机器能懂的指令（机器码）。为了保证这道菜做出来味道没变（程序行为正确），厨师必须非常小心，不能把“糖”变成“盐”，也不能把“煮”变成“炸”。

在这个领域，过去大家主要用两种方法来检查厨师有没有乱来：

小步走（Small-Step）： 就像慢动作回放。你盯着厨师的每一个动作：切一下、放一点盐、翻个面。这种方法非常精确，适合检查那些只改动了一点点细节的操作（比如把 2+2 直接算成 4）。
大步走（Big-Step）： 就像看最终结果。你不管中间切了多少次菜，直接看：“这道菜从生到熟，最后端上桌的样子对不对？”这种方法很直观，特别适合处理那些结构大变的操作，比如把“循环煮汤”改成“一次性倒进锅里煮”。

问题的出现：厨师的困境

以前，著名的编译器 CompCert（可以理解为业界最严谨的“米其林三星”编译器）决定只用“小步走”的方法。理由是：这样更统一，不容易出错。

但是，这就带来了一个麻烦：当厨师想要做大手术（比如“循环展开”，把“煮 10 次汤”改成“直接煮 10 锅汤”）时，用“小步走”去检查每一个微小的动作，就像是用放大镜去数蚂蚁，既累人又容易把复杂的结构搞乱。这就导致 CompCert 以前不敢轻易做这些高级的循环优化。

这篇论文的解决方案：混合双打

这篇论文的作者提出：为什么要二选一呢？我们可以“混搭”啊！

他们设计了一个通用的“行为翻译官”（Behavioral Semantics），就像是一个通用的货币兑换点。

不管你是用“小步走”还是“大步走”来描述程序，都可以先兑换成这种通用的“行为货币”。
这样，编译器就可以灵活地：在需要精细操作的地方用“小步走”，在需要大刀阔斧改结构的地方（比如循环优化），切换到“大步走”模式，做完后再换回“小步走”继续后续流程。

核心比喻：修路 vs. 看地图

为了让你更明白，我们可以打个比方：

小步走（小步语义） 就像是修路工。他拿着锤子，一下一下地敲路面。如果路要稍微挪个位置，他得把每一块砖都重新敲一遍。这很稳，但太慢了。
大步走（大步步语义） 就像是城市规划师。他直接看地图，说：“把这条弯曲的环路直接拉直，或者把这段路直接复制 10 份。”他不在乎中间哪块砖怎么放，只在乎起点和终点以及**路上的风景（输出结果）**有没有变。

以前的 CompCert 只允许修路工干活，所以规划师（做循环优化）没法进场，因为修路工看不懂规划师的蓝图。

这篇论文 说：我们给修路工和规划师都发一本通用的“行为手册”。

规划师进场，用他的“大步走”方法把路改好了（比如把循环展开）。
然后，他把手册交给修路工。修路工一看手册，发现：“哦，原来规划师这么改，虽然过程不一样，但最终的路况和风景跟我之前一步步修出来的是一样的！”
于是，整个工程既有了大优化的速度，又保留了小步走的严谨性。

他们具体做了什么？

作者们在 CompCert 里真的这么干了，他们实现了几个以前不敢做的“大手术”：

循环展开（Loop Unrolling）： 比如代码里写“循环 10 次”，他们直接把它变成“重复写 10 遍代码”。这就像把“绕着操场跑 10 圈”的指令，直接变成“在跑道上画 10 个圈，一次性跑完”。这能极大提高速度。
循环去开关（Loop Unswitching）： 把循环里的一些判断条件（比如“如果是晴天就浇水，下雨就停”）提到循环外面去。就像把“每浇一次水都要看天”改成“先看天，如果是晴天，就连续浇 10 次水”。

为什么这很重要？

更聪明： 以前因为怕出错，编译器不敢做这些复杂的优化，导致程序跑得不够快。现在敢做了，程序性能会提升。
更安全： 虽然优化变大了，但因为用了“行为翻译官”和严格的数学证明，我们100% 确定优化后的程序和原来的程序在行为上是一模一样的。
更灵活： 证明了以后，编译器可以像搭积木一样，哪里需要精细就哪里用小步走，哪里需要大刀阔斧就用大步走。

总结

这篇论文就像是在告诉编译器开发者：“别死守一种方法！小步走适合微调，大步走适合大改。只要你们能互相‘翻译’（通过行为语义），就可以强强联手，既保证安全，又提升性能。”

他们成功地把这种理论变成了现实，让著名的 CompCert 编译器第一次能够安全、自动地进行这些复杂的循环优化了。这对于那些对安全性要求极高的领域（如航空航天、医疗设备）来说，意味着未来的软件既快又稳。

这是一份关于论文《Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations》（结合小步和大步语义验证循环优化）的详细技术总结。

1. 研究背景与问题 (Problem)

背景：
验证编译器（如 CompCert）旨在通过机器检查的数学证明，保证编译过程不改变源程序的“可观察行为”。传统的验证方法主要依赖小步语义（Small-step Semantics），它通过描述程序状态的单步执行来定义行为，非常适合处理指令选择、常量传播等局部代码变换。

核心问题：
尽管小步语义通用性强，但在处理结构性变换（Structural Transformations），特别是循环优化（如循环展开、循环解耦）时，显得不够直观且证明过程极其复杂。

小步语义的局限： 证明循环优化通常需要构建复杂的“模拟关系（Simulation Relation）”，必须显式地追踪中间状态，并手动维护大量的不变量（Invariants）。对于涉及控制流图（CFG）结构改变的优化，这种逐步匹配的方法非常繁琐。
大步语义的缺失： 大步语义（Big-step/Natural Semantics）从高层概念描述程序执行（如“循环执行直到退出”），非常适合处理结构性变换。然而，CompCert 为了统一性，已完全弃用大步语义，转而使用小步语义。这导致 CompCert 官方版本中缺乏对复杂循环优化的验证支持。
现有方案的不足： 近年来虽有基于小步语义的循环优化验证方法（如基于 CFG 同态或翻译验证），但它们依赖解释器，且仅适用于特定类型的变换，通用性和模块化程度较低。

目标：
提出一种混合方法，将大步语义的优势引入现有的小步语义验证管道中，从而在保持 CompCert 整体正确性定理完整性的前提下，验证新的循环优化。

2. 方法论 (Methodology)

论文提出了一种**行为语义（Behavioral Semantics）**框架，作为连接小步语义和大步语义的通用接口。

2.1 行为语义抽象

作者定义了一个最小化的公共接口，统一了两种语义对程序行为的描述。程序行为被定义为三种情况：

终止 (Termination)： 产生有限轨迹 $t$ 并到达最终状态。
发散 (Divergence)： 产生轨迹 $\tau$ （可以是有限或无限）并无限运行。
出错 (Going Wrong)： 产生部分轨迹 $t$ 后无法继续，且未到达终止或发散状态。

通过定义行为精化（Refinement）和行为保持（Preservation），证明了如果源程序 $p$ 和目标程序 $p'$ 在行为上等价（ $p \equiv p'$ ），则编译正确。

2.2 扩展的大步语义 (Extended Coinductive Big-Step Semantics)

为了弥补传统大步语义在表达力上的不足（特别是处理发散行为），作者对 Leroy 的共归纳大步语义进行了关键扩展：

通用轨迹支持： 传统大步语义通常只能处理无限轨迹的发散。作者引入了共归纳判断，允许发散产生有限或无限的通用轨迹 $\tau$ 。
Guard 机制： 在发散规则中引入自然数 $n$ 和 guard 条件，确保在最多 $n$ 步规则应用后，必须产生非空的轨迹前缀。这解决了“空循环发散产生任意轨迹”的歧义问题，使其表达力达到与小步语义同等水平。
部分执行 (Partial Evaluation)： 引入部分执行判断，用于处理“出错”情况，无需单独定义复杂的“出错”谓词。

2.3 管道集成策略

在 CompCert 的 Cminor 中间语言层，作者构建了一个混合管道：

前半段： 使用标准的小步语义进行常规编译。
中间段（Cminor）： 切换到大步语义，在此层级执行循环优化（如循环解耦、完全循环展开）。
后半段： 切换回小步语义，继续后续编译。

关键证明步骤：

证明 Cminor 的小步语义与扩展后的大步语义是行为等价的（Soundness & Completeness）。
利用**前向保持（Forward Preservation）**证明优化变换的正确性。
利用**确定性（Determinacy）和接收性（Receptiveness）**性质，将前向保持推导为双向行为保持（Equivalence），从而无缝融入 CompCert 的整体正确性证明链。

3. 关键贡献 (Key Contributions)

统一的行为语义框架： 定义了从大小步语义中提取的通用行为谓词，并证明了其性质（如确定性、接收性）及保持定理。这使得在不同语义风格之间进行变换验证成为可能。
表达力等效的大步语义扩展： 扩展了共归纳大步语义，使其能够处理有限和无限轨迹的发散，解决了传统大步语义无法精确区分“死循环”和“无限轨迹”的问题，使其在表达能力上与小步语义对等。
CompCert 中的新循环优化验证：
- 循环解耦 (Loop Unswitching)： 将循环内独立的条件分支提升到循环外部。
- 完全循环展开 (Full Loop Unrolling)： 将固定次数的循环完全展开为顺序代码。
- While True 优化： 消除不产生任何事件且无法退出的死循环体。
- 注：这些优化在 CompCert 官方版本中此前未被验证过。
混合验证管道的实现： 成功将大步语义变换插入到 CompCert 的小步语义管道中，并证明了所有顶层正确性定理（包括链接、分离编译等）依然成立。

4. 实验结果与验证 (Results)

实现细节： 作者在 CompCert 的 Rocq (Coq) 实现中完成了上述工作。代码已开源。
证明复杂度对比：
- 大步语义证明： 对于循环解耦和展开，证明主要依赖结构归纳法。例如，循环解耦的证明只需简单的展开和归纳，无需处理复杂的中间状态匹配。
- 小步语义证明（对比）： 若在小步语义下证明同样的循环解耦，需要定义复杂的“状态匹配谓词”（Match Predicate），该谓词必须显式地追踪循环条件 $c$ 的求值状态、独立性不变量以及续体（Continuation）的匹配。这导致证明代码膨胀且难以复用。
具体案例：
- 循环展开： 成功验证了将 for (i=1; i<11; i++) 展开为 10 次顺序乘法，并结合常量传播计算出 $10!$ 的结果。
- 代码量： 尽管需要证明终止、部分执行和发散三种情况，循环展开的完整定义和证明（不含辅助引理）仅约 700 行 Rocq 代码，体现了模块化优势。

5. 意义与影响 (Significance)

方法论创新： 打破了“验证编译器必须统一使用单一语义风格”的教条。论文证明，小步语义适合局部变换，大步语义适合结构性变换，两者可以共存并互补。
提升验证效率与模块化： 使用大步语义进行循环优化验证，避免了繁琐的逐步模拟（Step-by-step simulation）和中间状态不变量的手动编织。证明过程更加自然、模块化，且易于复用（如 indep_spec 引理在多个优化中复用）。
推动 CompCert 功能扩展： 为 CompCert 引入复杂的循环优化铺平了道路，使其在保持高可信度的同时，能生成更高效的机器码。
通用性： 虽然以 CompCert 为例，但该框架（行为抽象、扩展的共归纳大步语义）可应用于其他验证编译器或中间语言，特别是那些具有归纳定义结构（Inductive Structure）的语言。
局限性讨论： 作者也指出，大步语义需要处理归纳和共归纳证明的重复工作，且对非归纳定义的语言（如基于 CFG 的 RTL）支持较难（需引入块结构或控制流抽象）。此外，大步语义目前不支持 goto 语句。

总结：
该论文通过引入行为语义抽象和扩展大步语义，成功解决了在验证编译器中验证复杂循环优化的难题。它不仅证明了混合语义方法的可行性，还展示了其在简化证明逻辑、提高模块化程度方面的巨大优势，为未来验证编译器的优化策略提供了新的范式。