research-article

Pilsner: a compositionally verified compiler for a higher-order imperative language

Authors:

Jan-Oliver Kaiser,

Craig McLaughlin,

Viktor VafeiadisAuthors Info & Claims

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

Pages 166 - 178

https://doi.org/10.1145/2784731.2784764

Published: 29 August 2015 Publication History

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.

References

[1]

Appendix and Coq development. http://plv.mpi-sws.org/pils.

[2]

A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006.

Digital Library

[3]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009.

Digital Library

[4]

L. Beringer, G. Stewart, R. Dockins, and A. W. Appel. Verified compilation for shared-memory C. In ESOP, 2014.

Digital Library

[5]

D. Dobbs, M. Fontana, and S.-E. Kabbaj, editors. Advances in Commutative Ring Theory. CRC Press, 1999.

[6]

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.

Digital Library

[7]

M. Fluet and S. Weeks. Contification using dominators. In ICFP, 2001.

Digital Library

[8]

C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011.

Digital Library

[9]

C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In POPL, 2012.

Digital Library

[10]

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.

[11]

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.

[12]

A. Kennedy. Compiling with continuations, continued. In ICFP, 2007.

Digital Library

[13]

R. Kumar, M. Myreen, M. Norrish, and S. Owens. CakeML: A verified implementation of ML. In POPL, 2014.

Digital Library

[14]

V. Le, M. Afshari, and Z. Su. Compiler validation via equivalence modulo inputs. In PLDI, 2014.

Digital Library

[15]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009.

Digital Library

[16]

J. Matthews and R. B. Findler. Operational semantics for multilanguage programs. In POPL, 2007.

Digital Library

[17]

K. S. Namjoshi. A simple characterization of stuttering bisimulation. In FSTTCS, pages 284–296, 1997.

Digital Library

[18]

A. Nanevski, V. Vafeiadis, and J. Berdine. Structuring the verification of heap-manipulating programs. In POPL, 2010.

Digital Library

[19]

J. T. Perconti and A. Ahmed. Verifying an open compiler using multilanguage semantics. In ESOP, 2014.

[20]

A. Pitts and I. Stark. Operational reasoning for functions with local state. In HOOTS, 1998.

Digital Library

[21]

D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. In LICS, 2007.

Digital Library

[22]

G. Stewart, L. Beringer, S. Cuellar, and A. W. Appel. Compositional CompCert. In POPL, 2015.

Digital Library

[23]

K. Støvring and S. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In POPL, 2007.

Digital Library

[24]

E. Sumii and B. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):1–43, 2007.

Digital Library

[25]

P. Wang, S. Cuellar, and A. Chlipala. Compiler verification meets cross-language linking via data abstraction. In OOPSLA, 2014.

Digital Library

Cited By

Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Zhang LWang YWu JKoenig JShao Z(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
https://dl.acm.org/doi/10.1145/3632914
Kanabar HKorban KMyreen M(2024)Verified Inlining and Specialisation for PureCakeProgramming Languages and Systems10.1007/978-3-031-57267-8_11(275-301)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_11
Show More Cited By

Index Terms

Pilsner: a compositionally verified compiler for a higher-order imperative language
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP '15

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 ...
A verified compiler for an impure functional language
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We 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 Languages

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

August 2015

436 pages

ISBN:9781450336697

DOI:10.1145/2784731

General Chair:
Kathleen Fisher
Tufts University, USA
,
Program Chair:
John Reppy
University of Chicago, USA

ACM SIGPLAN Notices Volume 50, Issue 9
ICFP '15
September 2015
436 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2858949
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP'15

Sponsor:

SIGPLAN

ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2015

BC, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
297
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)3

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Zhang LWang YWu JKoenig JShao Z(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
https://dl.acm.org/doi/10.1145/3632914
Kanabar HKorban KMyreen M(2024)Verified Inlining and Specialisation for PureCakeProgramming Languages and Systems10.1007/978-3-031-57267-8_11(275-301)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_11
Guéneau AHostert JSpies SSammler MBirkedal LDreyer D(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
https://dl.acm.org/doi/10.1145/3622823
Sewell TMyreen MTan YKumar RMihajlovic AAbrahamsson OOwens S(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
https://dl.acm.org/doi/10.1145/3591266
Sammler MSpies SSong YD'Osualdo EKrebbers RGarg DDreyer D(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
https://dl.acm.org/doi/10.1145/3571220
Bahr PHutton G(2022)Monadic compiler calculation (functional pearl)Proceedings of the ACM on Programming Languages10.1145/35476246:ICFP(80-108)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547624
Cheung LO'Connor LRizkallah CPopescu AZdancewic S(2022)Overcoming restraint: composing verification of foreign functions with cogentProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503686(13-26)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503686
El-Korashy ABlanco RThibault JDurier AGarg DHriţcu C(2022)SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919680(64-79)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919680
Paraskevopoulou ZLi JAppel A(2021)Compositional optimizations for CertiCoqProceedings of the ACM on Programming Languages10.1145/34735915:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473591
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents