[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3461648.3463850acmconferencesArticle/Chapter ViewAbstractPublication PagescpsweekConference Proceedingsconference-collections
research-article

Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion

Published: 22 June 2021 Publication History

Abstract

We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination. This approach is lightweight: each pass comes with a simple and independent proof of correctness. Experiments show the approach significantly narrows the performance gap between the CompCert certified compiler and state-of-the-art optimizing compilers. Our static analysis employs an efficient yet verified hashed set structure, resulting in fast compilation.

References

[1]
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
[2]
Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2012. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS2). HAL:hal-00653367.
[3]
Timothy Bourke, Lélio Brun, and Marc Pouzet. 2020. Mechanized semantics and verified compilation for a dataflow synchronous language with reset. Proceedings of the ACM on Programming Languages, 4, POPL (2020), January, 1–29. https://doi.org/10.1145/3371112
[4]
Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. 2014. Implementing and Reasoning About Hash-consed Data Structures in Coq. J. Autom. Reasoning, 53, 3 (2014), 271–304.
[5]
Patrick Cousot. 1978. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Université scientifique et médicale de Grenoble. Grenoble, France. https://tel.archives-ouvertes.fr/tel-00288657/document
[6]
Delphine Demange, David Pichardie, and Léo Stefanesco. 2015. Verifying Fast and Sparse SSA-Based Optimizations in Coq. In Compiler Construction (CC), Björn Franke (Ed.) (LNCS, Vol. 9031). Springer, 233–252. https://doi.org/10.1007/978-3-662-46663-6_12
[7]
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2011. Towards Formally Verified Optimizing Compilation in Flight Control Software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems, DATE Workshop PPES 2011, March 18, 2011, Grenoble, France., Philipp Lucas, Lothar Thiele, Benoit Triquet, Theo Ungerer, and Reinhard Wilhelm (Eds.) (OASICS, Vol. 18). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 59–68. https://doi.org/10.4230/OASIcs.PPES.2011.59
[8]
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
[9]
Gary Arlen Kildall. 1973. A Unified Approach to Global Program Optimization. In Principles of Programming Languages (POPL). Association for Computing Machinery, New York, NY, USA. 194–206. isbn:9781450373494 https://doi.org/10.1145/512927.512945
[10]
Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), HAL:inria-00415861.
[11]
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
[12]
2016. SSA-based Compiler Design, Fabrice Rastello (Ed.). Springer. isbn:978-1441962010 An updated version is available from http://ssabook.gforge.inria.fr/latest/book.pdf
[13]
Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 471–482. https://doi.org/10.1145/2491956.2462183
[14]
Jean-Baptiste Tristan. 2009. Formal verification of translation validators. Ph.D. Dissertation. Paris Diderot University, France. https://tel.archives-ouvertes.fr/tel-00437582
[15]
Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified validation of lazy code motion. In Programming Language Design and Implementation (PLDI), Michael Hind and Amer Diwan (Eds.). ACM Press, 316–326. https://doi.org/10.1145/1542476.1542512
[16]
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Programming Language Design and Implementation (PLDI). ACM Press, 283–294.

Cited By

View all
  • (2023)Formally Verifying Optimizations with Block SimulationsProceedings of the ACM on Programming Languages10.1145/36227997:OOPSLA2(59-88)Online publication date: 16-Oct-2023
  • (2023)Formally Verified EVM Block-OptimizationsComputer Aided Verification10.1007/978-3-031-37709-9_9(176-189)Online publication date: 17-Jul-2023
  • (2022)The Trusted Computing Base of the CompCert Verified CompilerProgramming Languages and Systems10.1007/978-3-030-99336-8_8(204-233)Online publication date: 5-Apr-2022

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
LCTES 2021: Proceedings of the 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems
June 2021
162 pages
ISBN:9781450384728
DOI:10.1145/3461648
  • General Chair:
  • Jörg Henkel,
  • Program Chair:
  • Xu Liu
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: 22 June 2021

Permissions

Request permissions for this article.

Check for updates

Badges

Author Tags

  1. Coq
  2. common subexpression elimination
  3. invariants
  4. optimization
  5. verified compilers
  6. verified hashed sets

Qualifiers

  • Research-article

Conference

LCTES '21
Sponsor:

Acceptance Rates

Overall Acceptance Rate 116 of 438 submissions, 26%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)23
  • Downloads (Last 6 weeks)2
Reflects downloads up to 07 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Formally Verifying Optimizations with Block SimulationsProceedings of the ACM on Programming Languages10.1145/36227997:OOPSLA2(59-88)Online publication date: 16-Oct-2023
  • (2023)Formally Verified EVM Block-OptimizationsComputer Aided Verification10.1007/978-3-031-37709-9_9(176-189)Online publication date: 17-Jul-2023
  • (2022)The Trusted Computing Base of the CompCert Verified CompilerProgramming Languages and Systems10.1007/978-3-030-99336-8_8(204-233)Online publication date: 5-Apr-2022

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media