Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion
Programming Languages
2021-05-05 v1
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.
Cite
@article{arxiv.2105.01344,
title = {Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion},
author = {David Monniaux and Cyril Six},
journal= {arXiv preprint arXiv:2105.01344},
year = {2021}
}