Pilsner: a compositionally verified compiler for a higher-order imperative language
Pilsner: a compositionally verified compiler for a higher-order imperative language
复制标题
Pilsner：用于高阶命令式语言的组合验证编译器
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
Georg Neis;C. Hur;Jan;Craig McLaughlin;Derek Dreyer;Viktor Vafeiadis
编译器验证对于构建完全验证的软件是必不可少的，但大多数先前的工作（如CompCert）都集中在验证整个程序编译器上。为了支持独立编译并能够链接来自不同验证编译器的结果，重要的是开发一个编译器正确性的组合概念，该概念是模块化的（在链接下保留），可传递的（支持多遍编译）和灵活的（适用于使用不同中间语言或采用非标准程序转换的编译器）。在本文中，在Hur等人先前工作的基础上，本文提出了一种基于参数化语言间模拟（PILS）的组合编译器验证方法。PILS是模块化的：它们以支持单独编译的方式启用编译器验证。PILS是可传递的：我们使用它们来验证Pilsner，一个简单的（但不平凡的）多遍优化编译器（用Coq编程），从ML类源语言S到汇编类目标语言T，经过基于CPS的中间语言。Pilsner是第一个用于高阶命令式语言的多遍编译器，可以进行组合验证。最后，PILS是灵活的：我们使用它们来另外验证（1）Zwickel，S的直接非优化编译器，和（2）手工编码的自修改T模块，被证明是正确的w.r.t. S级规格。Zwickel和自修改T模块的输出可以与Pilsner的输出安全地连接在一起。总的来说，这是一项重大的任务，涉及几个人年的工作和超过55，000行的Coq。
Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different verified compilers, it is important to develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports multi-pass compilation), and flexible (applicable to compilers that use different intermediate languages or employ non-standard program transformations). In this paper, building on prior work of Hur et al., we develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS). PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS are transitive: we use them to verify Pilsner, a simple (but non-trivial) multi-pass optimizing compiler (programmed in Coq) from an ML-like source language S to an assembly-like target language T, going through a CPS-based intermediate language. Pilsner is the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Lastly, PILS are flexible: we use them to additionally verify (1) Zwickel, a direct non-optimizing compiler for S, and (2) a hand-coded self-modifying T module, proven correct w.r.t. an S-level specification. The output of Zwickel and the self-modifying T module can then be safely linked together with the output of Pilsner. All together, this has been a significant undertaking, involving several person-years of work and over 55,000 lines of Coq.