SPOTS: A System for Proving Optimizing Transformations Sound SPOTS is a PVS (Prototype Verification System by SRI) based system for
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:
Download
System Requirements
People
LICENSE This tool is available under the Apache License, version 2.0. Project completed: 2007 |