# 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