Skip to main content

Compositional optimizations for CertiCoq

Author(s): Paraskevopoulou, Zoe; Li, John M; Appel, Andrew W

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1hh6c58j
Full metadata record
DC FieldValueLanguage
dc.contributor.authorParaskevopoulou, Zoe-
dc.contributor.authorLi, John M-
dc.contributor.authorAppel, Andrew W-
dc.date.accessioned2023-12-24T00:00:39Z-
dc.date.available2023-12-24T00:00:39Z-
dc.date.issued2021-08en_US
dc.identifier.citationParaskevopoulou, Zoe, John M. Li, and Andrew W. Appel. "Compositional optimizations for CertiCoq." Proceedings of the ACM on Programming Languages 5, no. ICFP (2021): pp. 1-30. doi:10.1145/3473591en_US
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1hh6c58j-
dc.description.abstractCompositional 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.en_US
dc.format.extent1 - 30en_US
dc.language.isoen_USen_US
dc.relation.ispartofProceedings of the ACM on Programming Languagesen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleCompositional optimizations for CertiCoqen_US
dc.typeJournal Articleen_US
dc.identifier.doi10.1145/3473591-
dc.identifier.eissn2475-1421-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
CompositionalOptimizationsCertiCoq.pdf390.15 kBAdobe PDFView/Download


Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.