ABSTRACT
Major 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 correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple "closed simulations" used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et al. have done, involves major changes and extensions to its original verification. In this paper, we show that if we aim somewhat lower---to prove correctness of separate compilation, but only for a *single* compiler---we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler.
- Andrew W. Appel. Program Logics for Certified Compilers. Cambridge University Press, 2014. Google ScholarDigital Library
- Nick Benton and Chung-Kil Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP, 2009. Google ScholarDigital Library
- Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. Verified compilation for shared-memory C. In ESOP, 2014.Google ScholarDigital Library
- The CompCert C compiler. http://compcert.inria.fr/.Google Scholar
- Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In POPL, 2015. Google ScholarDigital Library
- Chung-Kil Hur and Derek Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011. Google ScholarDigital Library
- Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. The marriage of bisimulations and Kripke logical relations. In POPL, 2012. Google ScholarDigital Library
- Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The transitive composability of relation transition systems. Technical Report MPI-SWS-2012-002, MPI-SWS, 2012.Google Scholar
- Ramana Kumar, Magnus Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In POPL, 2014. Google ScholarDigital Library
- Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. Google ScholarDigital Library
- Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009. Google ScholarDigital Library
- Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. In ICFP, 2015. Google ScholarDigital Library
- James T. Perconti and Amal Ahmed. Verifying an open compiler using multi-language semantics. In ESOP, 2014.Google Scholar
- Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, and Yuchen Fu. A compositional semantics for verified separate compilation and linking. In CPP, 2015. Google ScholarDigital Library
- SepCompCert. http://sf.snu.ac.kr/sepcompcert/.Google Scholar
- J. Souyris. Industrial use of CompCert on a safety-critical software product, February 2014. Talk slides available at: http://projects. laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf.Google Scholar
- Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. Compositional CompCert. In POPL, 2015. Google ScholarDigital Library
- Peng Wang, Santiago Cuellar, and Adam Chlipala. Compiler verification meets cross-language linking via data abstraction. In OOPSLA, 2014. Google ScholarDigital Library
Index Terms
- Lightweight verification of separate compilation
Recommendations
CompCertM: CompCert with C-assembly linking and lightweight modular verification
Supporting multi-language linking such as linking C and handwritten assembly modules in the verified compiler CompCert requires a more compositional verification technique than that used in CompCert just supporting separate compilation. The two ...
Lightweight verification of separate compilation
POPL '16Major 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 ...
A simple separate compilation mechanism for block-structured languages
A very simple and efficient technique for the introduction of separate compilation facilities into compilers for block-structured languages is presented. Using this technique, programs may be compiled in parts while the compile-time checking advantages ...
Comments