Affordable Access

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

Authors
  • Monniaux, David
  • Six, Cyril
Publication Date
May 01, 2021
Source
HAL-INRIA
Keywords
Language
English
License
Unknown
External links

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.

Report this publication

Statistics

Seen <100 times