Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

Formally Verified Loop-Invariant Code Motion and Assorted Optimizations

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.
Document type :
Journal articles
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03628646
Contributor : David Monniaux Connect in order to contact the contributor
Submitted on : Monday, April 4, 2022 - 11:03:37 AM
Last modification on : Friday, May 13, 2022 - 7:05:59 PM

Files

CSE3_TECS_article.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

David Monniaux, Cyril Six. Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. ACM Transactions on Embedded Computing Systems (TECS), ACM, inPress, ⟨10.1145/3529507⟩. ⟨hal-03628646⟩

Share

Metrics

Record views

31

Files downloads

36