spots
SPOTS: A System for Proving Optimizing Transformations Sound
SPOTS is a PVS (Prototype Verification System by SRI) based system for
Deductive verification of compiler optimizations and
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
Deductive verification spotspvs.tgz
Translation validation spotsgcc.tgz
Installation and user guide
System Requirements
Prototype verification system (PVS) version 3.2
GNU compiler collection (GCC) version 4.1
People
Aditya Kanade (Indian Institute of Science, contact)
Uday P. Khedker (IIT Bombay)
Amitabha Sanyal (IIT Bombay)
Publications
Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
A PVS based framework for validating compiler optimization
Software Engineering and Formal Methods (SEFM) 2006
Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
Structuring optimizing transformations and proving them sound
Electronic Notes in Theoretical Computer Science (ENTCS) 2007
Aditya Kanade
SPOTS: A system for proving optimizing transformations sound
PhD thesis, IIT Bombay, 2007
Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
Validation of GCC optimizers through trace generation
Software Practice and Experience (SPE) 2009
Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
A Logic for Correlating Temporal Properties across Program Transformations
ArXiv Technical Report, 2012
LICENSE
This tool is available under the Apache License, version 2.0.
Project completed: 2007