Georg Neis
Viktor Vafeiadis
ABSTRACT
Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different verified compilers, it is important to develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports multi-pass compilation), and flexible (applicable to compilers that use different intermediate languages or employ non-standard program transformations). In this paper, building on prior work of Hur et al., we develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS). PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS are transitive: we use them to verify Pilsner, a simple (but non-trivial) multi-pass optimizing compiler (programmed in Coq) from an ML-like source language S to an assembly-like target language T, going through a CPS-based intermediate language. Pilsner is the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Lastly, PILS are flexible: we use them to additionally verify (1) Zwickel, a direct non-optimizing compiler for S, and (2) a hand-coded self-modifying T module, proven correct w.r.t. an S-level specification. The output of Zwickel and the self-modifying T module can then be safely linked together with the output of Pilsner. All together, this has been a significant undertaking, involving several person-years of work and over 55,000 lines of Coq.
- Appendix and Coq development. http://plv.mpi-sws.org/pils.Google Scholar
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. Google ScholarDigital Library
- A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009. Google ScholarDigital Library
- L. Beringer, G. Stewart, R. Dockins, and A. W. Appel. Verified compilation for shared-memory C. In ESOP, 2014.Google ScholarDigital Library
- D. Dobbs, M. Fontana, and S.-E. Kabbaj, editors. Advances in Commutative Ring Theory. CRC Press, 1999.Google Scholar
- D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. JFP, 22(4-5), 2012. Google ScholarDigital Library
- M. Fluet and S. Weeks. Contification using dominators. In ICFP, 2001. Google ScholarDigital Library
- C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011. Google ScholarDigital Library
- C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In POPL, 2012. Google ScholarDigital Library
- C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The transitive composability of relation transition systems. Technical Report MPISWS-2012-002, MPI-SWS, 2012.Google Scholar
- C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. A logical step forward in parametric bisimulations. Technical Report MPI-SWS-2014-003, MPI-SWS, 2014.Google Scholar
- A. Kennedy. Compiling with continuations, continued. In ICFP, 2007. Google ScholarDigital Library
- R. Kumar, M. Myreen, M. Norrish, and S. Owens. CakeML: A verified implementation of ML. In POPL, 2014. Google ScholarDigital Library
- V. Le, M. Afshari, and Z. Su. Compiler validation via equivalence modulo inputs. In PLDI, 2014. Google ScholarDigital Library
- X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009. Google ScholarDigital Library
- J. Matthews and R. B. Findler. Operational semantics for multilanguage programs. In POPL, 2007. Google ScholarDigital Library
- K. S. Namjoshi. A simple characterization of stuttering bisimulation. In FSTTCS, pages 284–296, 1997. Google ScholarDigital Library
- A. Nanevski, V. Vafeiadis, and J. Berdine. Structuring the verification of heap-manipulating programs. In POPL, 2010. Google ScholarDigital Library
- J. T. Perconti and A. Ahmed. Verifying an open compiler using multilanguage semantics. In ESOP, 2014.Google Scholar
- A. Pitts and I. Stark. Operational reasoning for functions with local state. In HOOTS, 1998. Google ScholarDigital Library
- D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. In LICS, 2007. Google ScholarDigital Library
- G. Stewart, L. Beringer, S. Cuellar, and A. W. Appel. Compositional CompCert. In POPL, 2015. Google ScholarDigital Library
- K. Støvring and S. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In POPL, 2007. Google ScholarDigital Library
- E. Sumii and B. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):1–43, 2007. Google ScholarDigital Library
- P. Wang, S. Cuellar, and A. Chlipala. Compiler verification meets cross-language linking via data abstraction. In OOPSLA, 2014. Google ScholarDigital Library
Index Terms
- Pilsner: a compositionally verified compiler for a higher-order imperative language
Recommendations
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP '15Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
A verified compiler for an impure functional language
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to ...
Lightweight verification of separate compilation
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesMajor compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the ...
Comments