Compositional Optimizations for CertiCoq
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 \emph{lightweight compositional
compiler correctness}. We demonstrate that by imposing the
additional restriction that program components are compiled by
pipelines that go through \emph{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 \emph{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.
Thu 21 OctDisplayed time zone: Central Time (US & Canada) change
15:40 - 17:00 | |||
15:40 15mTalk | An Order-Aware Dataflow Model for Parallel Unix Pipelines SIGPLAN Papers Shivam Handa Massachusetts Institute of Technology, Konstantinos Kallas University of Pennsylvania, Nikos Vasilakis Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology DOI | ||
15:55 15mTalk | Compositional Optimizations for CertiCoq SIGPLAN Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI | ||
16:10 15mTalk | Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations SIGPLAN Papers Chaitanya S. Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook DOI | ||
16:25 15mTalk | Reasoning about the Garden of Forking Paths SIGPLAN Papers Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||
16:40 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers |