skip to main content
research-article

Compositional CompCert

Published: 14 January 2015 Publication History

Abstract

This paper reports on the development of Compositional CompCert, the first verified separate compiler for C.
Specifying and proving separate compilation for C is made challenging by the coincidence of: compiler optimizations, such as register spilling, that introduce compiler-managed (private) memory regions into function stack frames, and C's stack-allocated addressable local variables, which may leak portions of stack frames to other modules when their addresses are passed as arguments to external function calls. The CompCert compiler, as built/proved by Leroy etal 2006--2014, has proofs of correctness for whole programs, but its simulation relations are too weak to specify or prove separately compiled modules.
Our technical contributions that make Compositional CompCert possible include: language-independent linking, a new operational model of multilanguage linking that supports strong semantic contextual equivalences; and structured simulations, a refinement of Beringer etal logical simulation relations that enables expressive module-local invariants on the state communicated between compilation units at runtime. All the results in the paper have been formalized in Coq and are available for download together with the Compositional CompCert compiler.

Supplementary Material

MPG File (p275-sidebyside.mpg)

References

[1]
A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. In ICFP'11: The 16th ACM SIGPLAN International Conference on Functional Programming, 2011.
[2]
A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds, G. Stewart, S. Blazy, and X. Leroy. Program Logics for Certified Compilers. Cambridge, 2014.
[3]
N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP'09: The 14th ACM SIGPLAN International Conference on Functional Programming, 2009.
[4]
N. Benton and C.-K. Hur. Realizability and compositional compiler correctness for a polymorphic language. Technical Report MSR-TR-2010--62, Microsoft Research, 2010.
[5]
L. Beringer, G. Stewart, R. Dockins, and A. W. Appel. Verified compilation for shared-memory C. In ESOP'14: The 23rd European Symposium on Programming, 2014.
[6]
C11. C11 draft standard. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf, April 2011.
[7]
A. Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In PLDI 2007: Programming Language Design and Implementation, 2007.
[8]
A. Chlipala. A verified compiler for an impure functional language. In POPL'10: The 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2010.
[9]
M. A. Dave. Compiler verification: A bibliography. SIGSOFT Software Engineeering Notes, 28(6), 2003.
[10]
D. Ghica and N. Tzevelekos. A system-level game semantics. In MFPS'12: The 28th Conference on the Mathematical Foundations of Programming Semantics, 2012.
[11]
C. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In POPL'12: The 39th ACM SIGACT- SIGPLAN Symposium on Principles of Programming Languages, 2012.
[12]
C. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. Parametric bisimulations: A logical step forward. In POPL'13: The 40th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2013.
[13]
C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL'11: The 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2011.
[14]
X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009.
[15]
X. Leroy. The CompCert C compiler website. http://compcert.inria.fr/compcert-C.html, 2014.
[16]
R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL'13: The 40th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2013.
[17]
H. Liang, X. Feng, and M. Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In POPL'12: The 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2012.
[18]
A. Lochbihler. A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. PhD thesis, Karlsruher Institut für Technologie, July 2012.
[19]
W. E. Mansky. Specifying and Verifying Program Transformations with PTRANS. PhD thesis, University of Illinois, 2014.
[20]
J. Matthews and R. B. Findler. Operational semantics for multi-language programs. In POPL'07: The 34th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2007.
[21]
J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. Mathematical Aspects of Computer Science, 1, 1967.
[22]
M. McKay. Compiler correctness via contextual equivalence. Undergraduate thesis, Carnegie Mellon University, May 2014. J. S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461--492, 1989.
[23]
A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP'14: The 23rd European Symposium on Programming, 2014.
[24]
J. T. Perconti and A. Ahmed. Verifying an open compiler using multi- language semantics. In ESOP'14: The 23rd European Symposium on Programming, 2014.
[25]
J. Sevcík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. Comp-CertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22, 2013.
[26]
P. Wang, S. Cuellar, and A. Chlipala. Compiler verification meets cross- language linking via data abstraction. In OOPSLA'14: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, 2014.

Cited By

View all
  • (2024)Lightweight, Modular Verification for WebAssembly-to-Native Instruction SelectionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624862(231-248)Online publication date: 27-Apr-2024
  • (2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
  • (2022)Verifying optimizations of concurrent programs in the promising semanticsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523734(903-917)Online publication date: 9-Jun-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. compcert
  2. compiler correctness

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)40
  • Downloads (Last 6 weeks)6
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Lightweight, Modular Verification for WebAssembly-to-Native Instruction SelectionProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3617232.3624862(231-248)Online publication date: 27-Apr-2024
  • (2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
  • (2022)Verifying optimizations of concurrent programs in the promising semanticsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523734(903-917)Online publication date: 9-Jun-2022
  • (2021)An Extended Account of Trace-relating Compiler Correctness and Secure CompilationACM Transactions on Programming Languages and Systems10.1145/346086043:4(1-48)Online publication date: 10-Nov-2021
  • (2021)A formal approach to rigorous development of critical systemsJournal of Software: Evolution and Process10.1002/smr.233433:4Online publication date: 1-Apr-2021
  • (2020)Predicate Extension of Symbolic Memory Graphs for the Analysis of Memory Safety CorrectnessProgramming and Computer Software10.1134/S036176882008007146:8(747-754)Online publication date: 22-Dec-2020
  • (2019)Towards certified separate compilation for concurrent programsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314595(111-125)Online publication date: 8-Jun-2019
  • (2019)Semi-automated Reasoning About Non-determinism in C ExpressionsProgramming Languages and Systems10.1007/978-3-030-17184-1_3(60-87)Online publication date: 6-Apr-2019
  • (2019)Robustly Safe CompilationProgramming Languages and Systems10.1007/978-3-030-17184-1_17(469-498)Online publication date: 6-Apr-2019
  • (2017)A Formally Verified NATProceedings of the Conference of the ACM Special Interest Group on Data Communication10.1145/3098822.3098833(141-154)Online publication date: 7-Aug-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media