SPOTS: A System for Proving Optimizing Transformations Sound

SPOTS is a PVS (Prototype Verification System by SRI) based system for

  1. Deductive verification of compiler optimizations and
  2. Translation validation of GCC optimizations.

The key observation in this work is that many optimizations (e.g. common subexpression elimination, dead code elimination, loop invariant code motion, lazy code motion) can be specified as sequential compositions of primitive program transformations. Further, for each of the primitive transformations, we can define temporal logic soundness conditions. If a soundness condition holds on the input program, the transformed program is guaranteed to be semantically equivalent to the input program. These optimizations differ in their heuristics for selecting program points where the primitives should be applied and other details like which expressions to optimize form. These choices are resolved through different dataflow analyses. Thus, the proof of semantics preservation by an optimization in our setting reduces to showing that the dataflow analysis (on which the optimization is based on) implies the soundness conditions of the primitive transformations. We have developed a new temporal logic proof system, called the temporal transformation logic, for verification. The proof rules and primitive transformations with several example optimization specifications are encoded and proved in PVS.

For translation validation, an optimizer implementation is instrumented to generate a trace of its execution as a sequence of primitive program transformations. The trace is independently checked for its conformance with the compilation run. The translation validation succeeds if the temporal logic soundness conditions of every primitive transformation, in the trace, model checks on the input program to the transformation. For model checking and transformation simulation in PVS, we have given executable semantics to the primitive program transformations and temporal logic operators in boolean matrix algebra.

Case Studies The following case studies were performed with SPOTS:

  • Deductive verification: Common subexpression elimination, dead code elimination, partial dead code elimination, lazy code motion, loop invariant code motion, optimal code motion.
  • Translation validation: Loop invariant code motion (5K LOC), partial redundancy elimination through lazy code motion and code hoisting (6.8K LOC), copy and constant propagation (100 LOC) from GCC 4.1.

Download

System Requirements

  • Prototype verification system (PVS) version 3.2
  • GNU compiler collection (GCC) version 4.1

People

Publications

LICENSE

This tool is available under the Apache License, version 2.0.

Project completed: 2007