Formally Verified Loop-Invariant Code Motion and Assorted Optimizations
David Monniaux, Cyril Six
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 the fast compilation.
Topics & Concepts
Computer scienceCompilerCorrectnessInvariant (physics)Loop unrollingDead code eliminationProgram optimizationOptimizing compilerCode generationProgramming languageCode (set theory)CertificationParallel computingLoop fusionSet (abstract data type)Object codeOperating systemPhysicsLawPolitical scienceMathematical physicsKey (lock)Parallel Computing and Optimization TechniquesLogic, programming, and type systemsSecurity and Verification in Computing