经验证的寄存器分配

形式陈述

寄存器分配把无限供应的伪寄存器集合 $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).

预着色临时量必须落到调用约定指定位置，寄存器类别、保留寄存器和指令隐式操作数也形成约束。证明状态关系的关键不是所有死临时量都相等，而是对当前点每个活跃 $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。插入代码可能需要新鲜临时量；其活跃范围、寄存器类别和不与源值冲突必须重新满足约束。整个变换随后仍需作为语义保持阶段证明，而不是只验证图着色函数返回了一个编号。

直觉

活跃值像同一时刻必须保管的文件，物理寄存器像有限抽屉。生命周期不重叠的文件可以复用抽屉；同时要用的文件必须分开。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$ 且二者不干涉，把它们分到同一寄存器可删除移动；若它们在某条异常路径上同时活跃，而分析漏掉异常边，合并会覆盖仍需的 $v$ 。从SSA 消解得到的并行复制还可能含环，分配器不能用普通顺序移动破坏旧值。

栈槽不是无副作用的无限寄存器。它们改变栈帧大小、对齐和寻址范围，可能与保存的返回地址、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.

形式陈述 ​

形式陈述