Formal Verification of Coalescing Graph-Coloring Register Allocation

Formal Verification of Coalescing Graph-Coloring Register Allocation
复制标题

合并图着色寄存器分配的形式验证

DOI：
--
复制
发表时间：
2010
期刊：
European Symposium on Programming
影响因子：
--
通讯作者：
A. Appel
A. Appel
中科院分区：
--
文献类型：
--
作者：
Sandrine Blazy;Benoît Robillard;A. Appel

文献摘要

被引文献

相似文献

迭代寄存器合并（IRC）是一种通过图形着色执行寄存器分配的广泛使用的启发式。现有编译器中的许多实现（或多或少地忠实地）在1996年发布的命令算法。在其中一些实施中发现了一些错误。 在本文中，我们对整个IRC算法进行了正式验证（COQ）。我们详细介绍了可以用作IRC参考的规范。我们还定义了寄存器干扰图的理论；我们实施了IRC算法的纯粹功能版本，并证明了实施的总正确性。我们将IRC算法自动提取到CAML中会产生具有竞争性能的程序。这项工作已集成到经过验证的编译器中。
Iterated Register Coalescing (IRC) is a widely used heuristic for performing register allocation via graph coloring. Many implementations in existing compilers follow (more or less faithfully) the imperative algorithm published in 1996. Several mistakes have been found in some of these implementations. In this paper, we present a formal verification (in Coq) of the whole IRC algorithm. We detail a specification that can be used as a reference for IRC. We also define the theory of register-interference graphs; we implement a purely functional version of the IRC algorithm, and we prove the total correctness of our implementation. The automatic extraction of our IRC algorithm into Caml yields a program with competitive performance. This work has been integrated into the CompCert verified compiler.