经验证的寄存器分配

形式陈述

寄存器分配把无限供应的伪寄存器集合 $T$ 映射到有限物理寄存器与栈槽：

\operatorname{loc}:T\to\operatorname{Reg}\uplus\operatorname{Slot}.

在每个控制流图程序点 $\ell$ 计算活跃集合 $\operatorname{Live}(\ell)$ 。干涉约束既包括同一点同时需要的值，也包括每条保留指令的写入目标与该指令之后其余活跃值：即使目标本身已经死亡，这次写入仍不能覆盖将来要读的值。合法分配要求相容类别中

(u,v)\in I\Longrightarrow \operatorname{loc}(u)\ne\operatorname{loc}(v).

例如 u:=1; d:=0; return u 中，d 从不活跃，但保留的 d:=0 仍要求 d 与活跃的 u 使用不同位置；否则程序会返回 0。也可以先可靠地消除这条死写入，再按剩余指令建立约束。

预着色临时量必须落到调用约定指定位置，寄存器类别、保留寄存器和指令隐式操作数也形成约束。证明状态关系的关键不是所有死临时量都相等，而是对当前点每个活跃 $t$ ，目标位置 $\operatorname{loc}(t)$ 中的值等于源伪寄存器环境中的值。

对普通块，活跃性可用后向单调数据流分析，由

\operatorname{In}(B)=\operatorname{Use}(B)\cup (\operatorname{Out}(B)\setminus\operatorname{Def}(B)),\qquad \operatorname{Out}(B)=\bigcup_{S\in\operatorname{succ}(B)}\operatorname{In}(S)

求不动点。异常边、调用返回和隐式寄存器使用必须进入 $succ$ 与 Use/Def；漏一条边会少造干涉边，使一个表面合法的着色覆盖仍会被读取的值。

当寄存器不足时，allocator 将值 spill 到独立栈槽，并在使用前后插入 load/store。插入代码可能需要新鲜临时量；其活跃范围、寄存器类别和不与源值冲突必须重新满足约束。整个变换随后仍需作为语义保持阶段证明，而不是只验证图着色函数返回了一个编号。

活跃变量分析补充这里使用的逐指令逆序计算、块内先用后定义及φ的边使用规则；死代码消除则明确何时可以先删除纯总的无用赋值。后者仍不能省略本页对保留写入、调用clobber和spill重写的约束。

直觉

活跃值像同一时刻必须保管的文件，物理寄存器像有限抽屉。生命周期不重叠的文件可以复用抽屉；同时要用的文件必须分开。spill 是把文件暂存到有编号的档案柜，真正使用时再搬回抽屉。验证要保证每次读取都拿到正确文件，而不仅是“抽屉数量没有超限”。

calling convention 把部分抽屉预先指定为参数、返回值、caller-saved 或 callee-saved。跨调用仍活跃的值若放在会被调用者破坏的寄存器中，就必须保存恢复或改用安全位置。这个约束来自外部函数边界，无法由过程内干涉图单独推出。

例子与边界

设目标只有两个可分配寄存器，并假定地址由固定基址寄存器提供、二地址加法可覆盖已死亡的输入，考虑

t_1:=\operatorname{load}(A);\quad t_2:=\operatorname{load}(B);\quad t_3:=\operatorname{load}(C);\quad u:=t_2+t_3;\quad y:=t_1+u.

第三次 load 后三者同时活跃，形成三角干涉，两个寄存器无法同时容纳。可把 $t_1$ spill 到栈槽 $S_0$ ：先 load 并 store $t_1$ ，再让 $t_2,t_3$ 占两寄存器；以其中一个寄存器原地计算 $u$ 后，另一个寄存器腾出，再从 $S_0$ reload $t_1$ 完成最终加法。这个调度每一步至多占两个可分配寄存器。若误让 $S_0$ 与另一个同时活跃 spill 共用槽，或在寄存器尚未死亡时覆盖它，最后结果会错误。

复制合并的边界同样可算。若有 $u\leftarrow v$ 且二者不干涉，把它们分到同一寄存器可删除移动；若后续某条异常路径重新定义 $u$ 却仍需旧的 $v$ ，而分析漏掉该路径，合并就会覆盖仍需的值。允许复制专用的干涉边例外时，必须证明复制时两值相同，并继续检查后续所有写入约束。从SSA 消解得到的并行复制还可能含环，分配器不能用普通顺序移动破坏旧值。

基础调用约定与栈帧给出一套可复算的参数、帧偏移与保存恢复轨迹；GC根映射进一步要求在移动收集后更新或重载仍要使用的指针位置。这些实现接口与本页的活跃值保持义务配合，但不能由合法图着色单独保证。

栈槽不是无副作用的无限寄存器。它们改变栈帧大小、对齐和寻址范围，可能与保存的返回地址、callee-saved 区域或动态栈对象冲突。目标机器若要求某类浮点值只能放特定寄存器，纯粹的无类型图着色即使没有同色干涉也不合法。

callee-saved 分配还要与 prologue/epilogue 成对：函数若使用这类寄存器，入口保存旧值，每个正常或异常返回路径都恢复；caller-saved 中跨调用活跃的值则需在调用周围保存或 spill。spill 槽必须与源程序可访问内存、其他栈对象和不同调用帧分离。证明常以栈帧布局或 memory injection 表达这种分离，不能只比较寄存器环境。

推论与应用

一种小可信基架构让外部 allocator 产生位置映射与重写程序，再以翻译验证检查：所有干涉边颜色不同、预着色与类别正确、spill 槽分离、每条重写指令满足局部状态关系。只要 checker 的 soundness 已证，启发式着色器本身可留在可信基外；checker 拒绝时则必须停止或回退。

具体候选可由图着色分配或线性扫描产生，迭代合并再协调复制偏好与干涉。溢出与重物化给出带显式保留暂存器的可执行重写，并按实际路径计算访存；这些生成算法共同接受本页的位置与值保持合同，启发式质量另行比较。

另一种架构直接验证分配算法。无论哪种，证明还要与指令选择、栈布局和调用约定阶段组合。分配结果“在测试机上能运行”只覆盖少量路径；中断、异常、递归调用和极端寄存器压力会暴露未检查的 clobber 与 spill 错误，因此都应由语义关系统一覆盖。

参考资料

Sandrine Blazy, Benoît Robillard, and Andrew W. Appel, “Formal Verification of Coalescing Graph-Coloring Register Allocation,” in ESOP 2010, LNCS 6012, pp. 145–164.
Lal George and Andrew W. Appel, “Iterated Register Coalescing,” ACM TOPLAS 18(3), 1996, pp. 300–324.
Xavier Leroy, “A Formally Verified Compiler Back-end,” Journal of Automated Reasoning 43(4), 2009, §§7–8.

形式陈述 ​

反向链接

形式陈述