Formally Verifying Optimizations with Block Simulations - IMAG Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2023

Formally Verifying Optimizations with Block Simulations

Léo Gourdin
Benjamin Bonneau
  • Fonction : Auteur
Sylvain Boulmé
David Monniaux
Alexandre Bérard
  • Fonction : Auteur
  • PersonId : 1255981

Résumé

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 Motion (LCM) or Strength Reduction (SR) were still missing: developing these efficient optimizations together with their formal proofs remained a challenge. Cyril Six et al. have developed efficient formally verified translation validators for certifying the results of superblock schedulers and peephole optimizations. We revisit and generalize their approach into a framework (integrated into CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also Dead Code Elimination (DCE), Constant Propagation (CP), and more noticeably, LCM and SR. In contrast to other approaches to translation validation, we co-design our untrusted optimizations and their validators. Our optimizations provide hints, in the forms of invariants or CFG morphisms, that help keep the formally verified validators both simple and efficient. Such designs seem applicable beyond CompCert.
Fichier principal
Vignette du fichier
BTL_preprint.pdf (770.95 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
licence : Copyright (Tous droits réservés)

Dates et versions

hal-04102940 , version 1 (22-05-2023)
hal-04102940 , version 2 (05-06-2023)
hal-04102940 , version 3 (21-09-2023)

Licence

Copyright (Tous droits réservés)

Identifiants

  • HAL Id : hal-04102940 , version 1

Citer

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard. Formally Verifying Optimizations with Block Simulations. 2023. ⟨hal-04102940v1⟩
274 Consultations
224 Téléchargements

Partager

Gmail Facebook X LinkedIn More