Lazy Code Transformations in a Formally Verified Compiler
In: Proceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems (ICOOOLPS '23) ; ICOOOLPS '23: 18th ACM International Workshop on Implementation, 2023
Online
Konferenz
Zugriff:
International audience ; 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.
Titel: |
Lazy Code Transformations in a Formally Verified Compiler
|
---|---|
Autor/in / Beteiligte Person: | Gourdin, Léo ; VERIMAG (VERIMAG - IMAG) ; Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ) ; Université Grenoble Alpes (UGA) ; ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011) ; ANR-15-IDEX-0002,UGA,IDEX UGA(2015) |
Link: | |
Zeitschrift: | Proceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems (ICOOOLPS '23) ; ICOOOLPS '23: 18th ACM International Workshop on Implementation, 2023 |
Veröffentlichung: | HAL CCSD ; ACM, 2023 |
Medientyp: | Konferenz |
DOI: | 10.1145/3605158.3605848 |
Schlagwort: |
|
Sonstiges: |
|