skip to main content
10.1145/2676726.2676985acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
  • (2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
  • (2024)Fully Composable and Adequate Verified Compilation with Direct Refinements between Open ModulesProceedings of the ACM on Programming Languages10.1145/36329148:POPL(2160-2190)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compcert
  2. compiler correctness

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

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)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
  • (2024)Refinement Composition LogicProceedings of the ACM on Programming Languages10.1145/36746458:ICFP(573-601)Online publication date: 15-Aug-2024
  • (2024)Fully Composable and Adequate Verified Compilation with Direct Refinements between Open ModulesProceedings of the ACM on Programming Languages10.1145/36329148:POPL(2160-2190)Online publication date: 5-Jan-2024
  • (2024)TapChecker: A Lightweight SMT-Based Conflict Analysis for Trigger-Action ProgrammingIEEE Internet of Things Journal10.1109/JIOT.2024.337455611:12(21411-21426)Online publication date: 15-Jun-2024
  • (2024) : A simplified and abstract multicore hardware model for large scale system software formal verification Journal of Systems Architecture10.1016/j.sysarc.2023.103049147(103049)Online publication date: Feb-2024
  • (2024) : A template to build verified thread-local interfaces with software scheduler abstractions Journal of Systems Architecture10.1016/j.sysarc.2023.103046147(103046)Online publication date: Feb-2024
  • (2023)Melocoton: A Program Logic for Verified Interoperability Between OCaml and CProceedings of the ACM on Programming Languages10.1145/36228237:OOPSLA2(716-744)Online publication date: 16-Oct-2023
  • (2023)Cakes That Bake Cakes: Dynamic Computation in CakeMLProceedings of the ACM on Programming Languages10.1145/35912667:PLDI(1121-1144)Online publication date: 6-Jun-2023
  • (2023)DimSum: A Decentralized Approach to Multi-language Semantics and VerificationProceedings of the ACM on Programming Languages10.1145/35712207:POPL(775-805)Online publication date: 11-Jan-2023
  • (2023)The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingProceedings of the ACM on Programming Languages10.1145/35712177:POPL(689-717)Online publication date: 11-Jan-2023
  • 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