SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 15:55 - 16:10 at Zurich E - ICFP 2021 Papers Chair(s): Cyrus Omar

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 Oct

Displayed time zone: Central Time (US & Canada) change

15:40 - 17:00
ICFP 2021 PapersSIGPLAN Papers at Zurich E
Chair(s): Cyrus Omar University of Michigan
15:40
15m
Talk
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
15m
Talk
Compositional Optimizations for CertiCoq
SIGPLAN Papers
Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton
DOI
16:10
15m
Talk
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
SIGPLAN Papers
Chaitanya Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook
DOI
16:25
15m
Talk
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
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers