research-article

Open access

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler

Authors:

Aurèle Barrière,

Sandrine Blazy,

David PichardieAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL

Article No.: 9, Pages 249 - 277

https://doi.org/10.1145/3571202

Published: 11 January 2023 Publication History

Abstract

Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution, interpretation can be initially used. But after a while, JITs dynamically produce native code for parts of the program they execute often. Although some time is spent compiling dynamically, this mechanism makes for much faster times for the remaining of the program execution. Such compilers are complex pieces of software with various components, and greatly rely on a precise interplay between the different languages being executed, including on-stack-replacement. Traditional static compilers like CompCert have been mechanized in proof assistants, but JITs have been scarcely formalized so far, partly due to their impure nature and their numerous components. This work presents a model JIT with dynamic generation of native code, implemented and formally verified in Coq. Although some parts of a JIT cannot be written in Coq, we propose a proof methodology to delimit, specify and reason on the impure effects of a JIT. We argue that the daunting task of formally verifying a complete JIT should draw on existing proofs of native code generation. To this end, our work successfully reuses CompCert and its correctness proofs during dynamic compilation. Finally, our prototype can be extracted and executed.

References

[1]

Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst., 37, 2 (2015), 7:1–7:31. https://doi.org/10.1145/2701415

Digital Library

[2]

Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, and Jan Vitek. 2021. Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang., https://doi.org/10.1145/3434327

Digital Library

[3]

Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst., 36, 1 (2014), 4:1–4:35. https://doi.org/10.1145/2579080

Digital Library

[4]

Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Towards a verified range analysis for JavaScript JITs. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020. ACM, 135–150. https://doi.org/10.1145/3385412.3385968

Digital Library

[5]

David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microkernels, State Monads and Scalable Refinement. In Proc. of TPHOLs 2008. 5170, Springer, 167–182. https://doi.org/10.1007/978-3-540-71067-7_16

Digital Library

[6]

Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek. 2018. Correctness of speculative optimizations with dynamic deoptimization. https://doi.org/10.1145/3158137

Digital Library

[7]

2022. Java HotSpot Performance Engine. https://openjdk.org/groups/hotspot/

[8]

2022. The Coq proof assistant reference manual. http://coq.inria.fr Version 8.12.1.

[9]

Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi. 2018. Crellvm: verified credible compilation for LLVM. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018. ACM, 631–645. https://doi.org/10.1145/3192366.3192377

Digital Library

[10]

Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. In ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. 1–9. https://hal.inria.fr/hal-01643290

[11]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implementation of ML. In Proceedings of POPL. https://doi.org/10.1145/2535838.2535841

Digital Library

[12]

Peter Lammich and S. Reza Sefidgar. 2019. Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. J. Autom. Reason., 62, 2 (2019), 261–280. https://doi.org/10.1007/s10817-017-9442-4

Digital Library

[13]

Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proceedings of POPL. https://doi.org/10.1145/1111037.1111042

Digital Library

[14]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, https://doi.org/10.1145/1538788.1538814

Digital Library

[15]

Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning, 43, 4 (2009), 363–446. https://doi.org/10.1007/s10817-009-9155-4

Digital Library

[16]

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. https://hal.inria.fr/hal-01238879

[17]

Thomas Letan and Yann Régis-Gianas. 2020. FreeSpec: specifying, verifying, and executing impure computations in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP. https://doi.org/10.1145/3372885.3373812

Digital Library

[18]

Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony C. J. Fox. 2019. Verified compilation on a verified processor. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019. ACM, 1041–1053. https://doi.org/10.1145/3314221.3314622

Digital Library

[19]

Magnus O. Myreen. 2010. Verified just-in-time compiler on x86. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010. ACM, 107–118. https://doi.org/10.1145/1706299.1706313

Digital Library

[20]

Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan. 2017. Verifying efficient function calls in CakeML. PACMPL, 1, ICFP (2017), 18:1–18:27. https://doi.org/10.1145/3110262

Digital Library

[21]

Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, and Adam Chlipala. 2020. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. In Proc. of IJCAR 2020. 12167, Springer, 119–137. https://doi.org/10.1007/978-3-030-51054-1_7

Digital Library

[22]

2022. PyPy Python Implementation. https://www.pypy.org/

[23]

Kazuhiko Sakaguchi. 2018. Program Extraction for Mutable Arrays. In Functional and Logic Programming - 14th International Symposium, FLOPS 2018. 10818, Springer, 51–67. https://doi.org/10.1007/978-3-319-90686-7_4

[24]

Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, and Chung-Kil Hur. 2020. CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proc. ACM Program. Lang., 4, POPL (2020), 23:1–23:31. https://doi.org/10.1145/3371091

Digital Library

[25]

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proc. ACM Program. Lang. POPL 2015. ACM, 275–287. https://doi.org/10.1145/2676726.2676985

Digital Library

[26]

Wouter Swierstra. 2008. Data types à la carte. J. Funct. Program., https://doi.org/10.1017/S0956796808006758

Digital Library

[27]

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. 2016. A new verified compiler backend for CakeML. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016. ACM, 60–73. https://doi.org/10.1145/2951913.2951924

Digital Library

[28]

2022. V8 Javascript Engine. https://v8.dev/

[29]

Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang., 3, POPL (2019), 62:1–62:30. https://doi.org/10.1145/3290375

Digital Library

[30]

Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Formal Methods - 24th International Symposium, FM 2021. 13047, Springer, 61–79. https://doi.org/10.1007/978-3-030-90870-6_4

Digital Library

[31]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., https://doi.org/10.1145/3371119

Digital Library

[32]

Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, and executable formal semantics for LLVM IR. https://doi.org/10.1145/3473572

Digital Library

[33]

Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In Proceedings of the Symposium on Principles of Programming Languages, POPL. https://doi.org/10.1145/2103656.2103709

Digital Library

[34]

Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2013. Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013. ACM. https://doi.org/10.1145/2491956.2462164

Digital Library

Cited By

Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_16
Lei SGuan HJiang JZou YRao Y(2023)A Machine Proof System of Point Geometry Based on CoqMathematics10.3390/math1112275711:12(2757)Online publication date: 18-Jun-2023
https://doi.org/10.3390/math11122757
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

Index Terms

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Just-in-time compilers
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Formally verified speculation and deoptimization in a JIT compiler

Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. ...
A formally verified compiler for Lustre
PLDI '17

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive ...
A Formally Verified Compiler Back-end

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue POPL

January 2023

2196 pages

EISSN:2475-1421

DOI:10.1145/3554308

Editor:

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
514
Total Downloads

Downloads (Last 12 months)296
Downloads (Last 6 weeks)38

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_16
Lei SGuan HJiang JZou YRao Y(2023)A Machine Proof System of Point Geometry Based on CoqMathematics10.3390/math1112275711:12(2757)Online publication date: 18-Jun-2023
https://doi.org/10.3390/math11122757
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

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents