Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion

TL;DR

This paper introduces a lightweight, formally verified approach for global common subexpression elimination and loop-invariant code motion, improving the performance of certified compilers with efficient static analysis.

Contribution

It presents a novel, formally certified method combining unrolling and global subexpression elimination, with proofs of correctness for each pass.

Findings

Significantly narrows the performance gap with state-of-the-art compilers

Uses an efficient verified hashed set for fast static analysis

Each optimization pass is independently proven correct

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.