TY - JOUR
T1 - Compositional optimizations for CertiCoq
AU - Paraskevopoulou, Zoe
AU - Li, John M.
AU - Appel, Andrew W.
N1 - Funding Information:
This material is based upon work supported in part by the National Science Foundation under Grant No. CCF-1521602 and Grant No. CCF-2005545. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation. The first author was supported by Computing Innovation Fellows 2020 Project during part of this research. We wish to thank the anonymous reviewers for their insightful comments and Norman Ramsey for his valuable feedback in the final revision of this paper.
Publisher Copyright:
© 2021 Owner/Author.
PY - 2021/8
Y1 - 2021/8
N2 - 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 for lightweight compositional compiler correctness. We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the 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 of relational 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.
AB - 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 for lightweight compositional compiler correctness. We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the 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 of relational 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.
KW - A-normal form
KW - closure conversion
KW - compilation by transformation
KW - compositional compiler correctness
KW - lambda lifting
KW - logical relations
KW - separate compilation
UR - http://www.scopus.com/inward/record.url?scp=85113344592&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85113344592&partnerID=8YFLogxK
U2 - 10.1145/3473591
DO - 10.1145/3473591
M3 - Article
AN - SCOPUS:85113344592
SN - 2475-1421
VL - 5
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - ICFP
M1 - 3473591
ER -