Compositional optimizations for CertiCoq
Compositional optimizations for CertiCoq
复制标题
CertiCoq 的成分优化
DOI：
10.1145/3473591
复制
发表时间：
2021
影响因子：
--
通讯作者：
Appel, Andrew W.
中科院分区：
文献类型：
--
作者：
Paraskevopoulou, Zoe;Li, John M.;Appel, Andrew W.
组合编译器验证是一个困难的问题，它侧重于使用可能不同的已验证编译器对程序组件进行单独编译。在高级语言中，逻辑关系被广泛用于证明程序转换的正确性；然而，由于它们缺乏传递性，它们不能扩展到多遍编译器的组合验证。唯一已知的适用于高阶语言的多遍编译器的成分验证的技术是参数语言间模拟(PILS)，然而，它比传统的编译器正确性证明技术复杂得多。本文提出了一种新的轻量级组合编译器正确性验证框架。我们证明，通过施加额外的限制，即程序组件是由经过相同中间表示序列的流水线编译的，可以传递地合成逻辑关系证明，以便推导出多遍编译器流水线的端到端组成规范。与传统的逻辑关系框架不同，我们的框架支持保持分歧--即使转换减少了程序步骤的数量。我们通过使用一对关系不变量来参数化我们的逻辑关系来实现这一点。我们应用这一技术来验证从Galina(Coq的规范语言)到C的编译器CertiCoq的多遍、优化的中间端流水线。该流水线优化和闭包-将无类型函数中间语言(ANF或CPS)转换为该语言的没有嵌套函数的子集，从而可以很容易地将代码生成为低级语言。值得注意的是，我们的流水线执行的闭包分配优化比经过验证的编译中的最先进水平更复杂。使用我们新的验证框架，我们证明了我们的流水线的端到端定理，该定理涵盖了终止和发散，适用于整个程序和单独的编译，即使不同的模块以不同的优化进行编译。我们的结果在CoQ证明助手中是机械化的。
Compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages; however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework forlightweight compositional compiler correctness. We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go throughthe same sequence of intermediate representations, logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservation—even when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair ofrelational invariants.We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-program and separate compilation, even when different modules are compiled with different optimizations. Our results are mechanized in the Coq proof assistant.
登录
查看更多内容
用于非纯函数语言的经过验证的编译器
DOI：
--
发表时间：
2010
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
Pilsner：用于高阶命令式语言的组合验证编译器
DOI：
--
发表时间：
2015
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Georg Neis;C. Hur;Jan;Craig McLaughlin;Derek Dreyer;Viktor Vafeiadis
通讯作者：
Viktor Vafeiadis
DOI：
--
发表时间：
1992
期刊：
International Conference on Computational Linguistics
影响因子：
--
作者：
Wlodek Zadrozny
通讯作者：
Wlodek Zadrozny
正确地使用延续进行编译
DOI：
--
发表时间：
2021
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Zoe Paraskevopoulou;Anvay Grover
通讯作者：
Anvay Grover
使用步进索引逻辑关系证明编译器的正确性
DOI：
--
发表时间：
2016
期刊：
Workshop on Logical and Semantic Frameworks with Applications
影响因子：
--
作者：
Leonardo Rodríguez;Miguel Pagano;Daniel Fridlender
通讯作者：
Daniel Fridlender