Sigurd Schneider

The design and implementation of the linear verified compiler (LVC) is my PhD project.

In my master's thesis, I developed a term-based approach to static single assignment that leverages that SSA is functional programming (Appel, Kelsey). LVC is a verified compiler that uses this approach to realize SSA-based optimizations, in particular sparse conditional constant propagation (Wegman, Zadeck) and SSA-based register allocation including spilling (Rosemann, Schneider, Hack). LVC realizes compilation as program transformation to a low-level fragment of the intermediate language (Kelsey, Hudak). LVC's intermediate language IL supports this approach by providing two semantic interpretations, a functional one (variables are binders) and an imperative one (variables are imperative locations). The two semantic interpretations provide a semantic framework for SSA programs, in particular, we claim IL makes it easier to rename apart an imperative program as the usual dominance-based approach.

The development of LVC is available at GitHub. I extended the intermediate language in the formal development with mutually recursive function definitions to be more realistic - a time-consuming mistake. The CoqDoc documentation is available here.

A Verified Compiler for a Linear Function/Imperative Intermediate Language
Reviewers/Advisors: Prof. Sebastian Hack, Prof. Gert Smolka
Third Reviewer: Prof. David Pichardie
Submission: April 2018
Defense date: 16. November 2018
Download Coq development Thesis

Abstract

This thesis describes the design of the verified compiler LVC. LVC's main novelty is the way its first-order, term-based intermediate language IL realizes the advantages of static single assignment (SSA) for verified compilation. IL is a term-based language not based on a control-flow graph (CFG) but defined in terms of an inductively defined syntax with lexically scoped mutually recursive function definitions. IL replaces the usual dominance-based SSA definition found in unverified and verified compilers with the novel notion of coherence. The main research question this thesis studies is whether IL with coherence offers a faithful implementation of SSA, and how the design influences the correctness invariants and the proofs in the verified compiler LVC. To study this question, we verify dead code elimination, several SSA-based value optimizations including sparse conditional constant propagation and SSA-based register allocation approach including spilling. In these case studies, IL with coherence provides the usual advantages of SSA and improves modularity of proofs. Furthermore, we propose a novel SSA construction algorithm based on coherence, and leverage the term structure of IL to obtain an inductive proof method for simulation proofs. LVC is implemented and verified with over 50,000 lines of code using the proof assistant Coq. To underline practicability of our approach, we integrate LVC with CompCert to obtain an executable compiler that generates PowerPC assembly code.