research-article

Lazy Code Transformations in a Formally Verified Compiler

Author:

Léo GourdinAuthors Info & Claims

ICOOOLPS 2023: Proceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems

Pages 3 - 14

https://doi.org/10.1145/3605158.3605848

Published: 17 July 2023 Publication History

Abstract

Translation validation verifies the results of an untrusted translator—called an oracle—at the compiler’s runtime using a validator. This approach enables validating intricate optimizations without having to prove them directly. Parametrizing such a validator with hints provided by oracles greatly simplifies its integration within a formally verified compiler—such as CompCert. However, generating those hints requires adapting state-of-the-art optimizations.

The co-design of a validation framework supporting a class of optimizations led us to improve the Lazy Code Motion (LCM) and Lazy Strength Reduction (LSR) data-flow algorithms of Knoop, Rüthing, and Steffen. We propose an efficient implementation in OCaml combining both LCM and LSR, operating over basic-blocks, and whose result is checked by a Coq-verified validator. We show how to generate invariant annotations from the data-flow equations as hints for the defensive validation, and we introduce several algorithmic refinements w.r.t. the original papers.

Our solution is fully integrated within CompCert, and to the best of our knowledge, it is the first formally verified strength-reduction of loop-induction variables.

References

[1]

Jan Andersson. 2020. Development of a NOEL-V RISC-V SoC Targeting Space Applications. In 2020 50th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W). 66–67. https://doi.org/10.1109/DSN-W50199.2020.00020

[2]

Andrew W. Appel. 1998. SSA is Functional Programming. SIGPLAN Not., 33, 4 (1998), apr, 17–20. issn:0362-1340 https://doi.org/10.1145/278283.278285

Digital Library

[3]

Rastislav Bodík, Rajiv Gupta, and Mary Lou Soffa. 1998. Complete Removal of Redundant Expressions. In Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI ’98). Association for Computing Machinery, New York, NY, USA. 1–14. isbn:0897919874 https://doi.org/10.1145/277650.277653

Digital Library

[4]

Sylvain Boulmé. 2021. Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). Université Grenoble Alpes. https://hal.archives-ouvertes.fr/tel-03356701

[5]

John Cocke and Ken Kennedy. 1977. An algorithm for reduction of operator strength. Commun. ACM, 20, 11 (1977), Nov., 850–856. issn:0001-0782, 1557-7317 https://doi.org/10.1145/359863.359888

Digital Library

[6]

Keith D. Cooper, L. Taylor Simpson, and Christopher A. Vick. 2001. Operator strength reduction. ACM Transactions on Programming Languages and Systems, 23, 5 (2001), Sept., 603–625. issn:0164-0925, 1558-4593 https://doi.org/10.1145/504709.504710

Digital Library

[7]

Delphine Demange. 2012. Semantic Foundations of Intermediate Program Representations. Ph. D. Dissertation. École Normale Supérieure de Cachan, France. http://people.irisa.fr/Delphine.Demange/papers/DemangePhD.pdf EAPLS Best PhD Dissertation Award 2012. Gilles Kahn PhD Thesis Award 2013

[8]

Delphine Demange and Yon Fernandez de Retana. 2016. Mechanizing conventional SSA for a verified destruction with coalescing. In 25th International Conference on Compiler Construction. Barcelona, Spain. https://doi.org/10.1145/2892208.2892222

Digital Library

[9]

Delphine Demange, David Pichardie, and Léo Stefanesco. 2015. Verifying Fast and Sparse SSA-based Optimizations in Coq. In 24th International Conference on Compiler Construction, CC 2015. London, United Kingdom. https://doi.org/10.1007/978-3-662-46663-6_12

[10]

Stefano Di Mascio, Alessandra Menicucci, Eberhard Gill, Gianluca Furano, and Claudio Monteleone. 2019. Leveraging the Openness and Modularity of RISC-V in Space. 16 (2019), 1–19. https://doi.org/10.2514/1.I010735

[11]

Heiko Falk, Sebastian Altmeyer, Peter Hellinckx, Björn Lisper, Wolfgang Puffitsch, Christine Rochange, Martin Schoeberl, Rasmus Bo Sørensen, Peter Wägemann, and Simon Wegener. 2016. TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016), Martin Schoeberl (Ed.) (OpenAccess Series in Informatics (OASIcs), Vol. 55). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 2:1–2:10. https://doi.org/10.4230/OASIcs.WCET.2016.2

[12]

Jonathan S. Golan. 1999. Semimodules over Semirings. In Semirings and their Applications. Springer Netherlands, Dordrecht. 149–161. isbn:978-90-481-5252-0 978-94-015-9333-5 https://doi.org/10.1007/978-94-015-9333-5_14

[13]

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, and Alexandre Bérard. 2023. Formally Verifying Optimizations with Block Simulations. May, https://hal.science/hal-04102940 preprint

[14]

M.R. Guthaus, J.S. Ringenberg, D. Ernst, T.M. Austin, T. Mudge, and R.B. Brown. 2001. MiBench: A free, commercially representative embedded benchmark suite. In Proceedings of the Fourth Annual IEEE International Workshop on Workload Characterization. WWC-4 (Cat. No.01EX538). IEEE, Austin, TX, USA. 3–14. isbn:978-0-7803-7315-0 https://doi.org/10.1109/WWC.2001.990739

[15]

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. Toulouse, France. 1–9. https://hal.inria.fr/hal-01643290

[16]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM, 19, 7 (1976), 385–394. https://doi.org/10.1145/360248.360252

Digital Library

[17]

Jens Knoop, Oliver Ruthing, and Bernhard Steffen. 1995. Optimal Code Motion: Theory and Practice. ACM Transactions on Programming Languages and Systems, 16 (1995), Sept., https://doi.org/10.1145/183432.183443

Digital Library

[18]

Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1992. Lazy code motion. In Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation - PLDI ’92. ACM Press, San Francisco, California, United States. 224–234. isbn:978-0-89791-475-8 https://doi.org/10.1145/143095.143136

Digital Library

[19]

Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1993. Lazy Strength Reduction. Journal of Programming Languages, 1 (1993), 71–91. https://www.clear.rice.edu/comp512/Lectures/Papers/Knoop-LazyStrengthReduction.pdf

[20]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), HAL:inria-00415861. http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

[21]

Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning, 43, 4 (2009), 363–446. http://xavierleroy.org/publi/compcert-backend.pdf

[22]

Tao Lu. 2021. A Survey on RISC-V Security: Hardware and Architecture. arxiv:2107.04175 arXiv:2107.04175 [cs]

[23]

David Monniaux, Léo Gourdin, Sylvain Boulmé, and Olivier Lebeltel. 2023. Testing a Formally Verified Compiler. In Tests and Proofs - 17th International Conference, TAP 2023, Held as Part of STAF 2023, July, 2023, Proceedings. to appear, Springer. https://hal.science/hal-04096390

[24]

David Monniaux and Cyril Six. 2021. Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. In LCTES ’21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021, Jörg Henkel and Xu Liu (Eds.). ACM, 85–96. https://doi.org/10.1145/3461648.3463850

Digital Library

[25]

E. Morel and C. Renvoise. 1979. Global optimization by suppression of partial redundancies. Commun. ACM, 22, 2 (1979), Feb., 96–103. issn:0001-0782, 1557-7317 https://doi.org/10.1145/359060.359069

Digital Library

[26]

George C. Necula. 2000. Translation validation for an optimizing compiler. 83–94. https://doi.org/10.1145/349299.349314

Digital Library

[27]

A. Pnueli, M. Siegel, and E. Singerman. 1998. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and Bernhard Steffen (Eds.). 1384, Springer Berlin Heidelberg, Berlin, Heidelberg. 151–166. isbn:978-3-540-64356-2 978-3-540-69753-4 https://doi.org/10.1007/BFb0054170 Series Title: Lecture Notes in Computer Science

[28]

Louis-Noël Pouchet. 2012. the Polyhedral Benchmark suite. http://web.cs.ucla.edu/~pouchet/software/polybench/

[29]

Silvain Rideau and Xavier Leroy. 2010. Validating register allocation and spilling. In Compiler Construction (CC 2010). 6011, Springer, 224–243. http://gallium.inria.fr/~xleroy/publi/validation-regalloc.pdf

Digital Library

[30]

Hanan Samet. 1976. Compiler testing via symbolic interpretation. In Proceedings of the 1976 Annual Conference, Houston, Texas, USA, October 20-22, 1976, John A. Gosden and Olin G. Johnson (Eds.). ACM, 492–497. https://doi.org/10.1145/800191.805648

Digital Library

[31]

Cyril Six, Sylvain Boulmé, and David Monniaux. 2020. Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang., 4, OOPSLA (2020), 129:1–129:29. https://hal.archives-ouvertes.fr/hal-02185883

Digital Library

[32]

Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino. 2022. Formally Verified Superblock Scheduling. In Certified Programs and Proofs (CPP ’22). Philadelphia, United States. https://hal.archives-ouvertes.fr/hal-03200774

[33]

Chengnian Sun, Vu Le, Qirun Zhang, and Zhendong Su. 2016. Toward understanding compiler bugs in GCC and LLVM. In Proceedings of the 25th International Symposium on Software Testing and Analysis. ACM, Saarbrücken Germany. 294–305. isbn:978-1-4503-4390-9 https://doi.org/10.1145/2931037.2931074

Digital Library

[34]

Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion. 316–326. http://gallium.inria.fr/~xleroy/publi/validation-LCM.pdf

[35]

Andrew Waterman, Yunsup Lee, David Patterson, Krste Asanovic, Volume I User level Isa, Andrew Waterman, Yunsup Lee, and David Patterson. 2014. The RISC-V instruction set manual. Volume I: User-Level ISA’, version, 2 (2014).

[36]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. 283–294. https://doi.org/10.1145/1993498.1993532

Digital Library

[37]

Zhide Zhou, Zhilei Ren, Guojun Gao, and He Jiang. 2021. An empirical study of optimization bugs in GCC and LLVM. Journal of Systems and Software, 174 (2021), April, 110884. issn:01641212 https://doi.org/10.1016/j.jss.2020.110884

Cited By

Monniaux DTimany ATraytel DPientka BBlazy S(2024)Memory Simulations, Security and Optimization in a Verified CompilerProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636952(103-117)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636952
Gourdin LBonneau BBoulmé SMonniaux DBérard A(2023)Formally Verifying Optimizations with Block SimulationsProceedings of the ACM on Programming Languages10.1145/36227997:OOPSLA2(59-88)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622799

Index Terms

Lazy Code Transformations in a Formally Verified Compiler
1. General and reference
  1. Cross-computing tools and techniques
    1. Performance
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. Compilers
      1. Retargetable compilers

Recommendations

Formally Verifying Optimizations with Block Simulations

CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing C compiler. Indeed, some optimizations of “gcc ‍-O1” such as Lazy Code ...
Formally verified superblock scheduling
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks ...
Verified validation of lazy code motion
PLDI '09

Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICOOOLPS 2023: Proceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems

July 2023

26 pages

ISBN:9798400702488

DOI:10.1145/3605158

General Chairs:
Eric Jul
University of Oslo, Norway
,
Dimi Racordon
Northeastern University, USA

Copyright © 2023 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 July 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICOOOLPS '23

Sponsor:

SIGSOFT

ICOOOLPS '23: 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems

July 17, 2023

WA, Seattle, USA

Acceptance Rates

Overall Acceptance Rate 11 of 14 submissions, 79%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
29
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)1

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Monniaux DTimany ATraytel DPientka BBlazy S(2024)Memory Simulations, Security and Optimization in a Verified CompilerProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636952(103-117)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636952
Gourdin LBonneau BBoulmé SMonniaux DBérard A(2023)Formally Verifying Optimizations with Block SimulationsProceedings of the ACM on Programming Languages10.1145/36227997:OOPSLA2(59-88)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622799

View Options

Get Access

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