A compiler optimizer analyzes and transforms programs to improve their performance.
However, a mistake in the design or the implementation
of an optimizer can proliferate in the form of bugs in the softwares compiled through it.
The issue of soundness of optimizers can be addressed at two levels:
(1) One time guarantees can be obtained at the design level by verifying optimization specifications and
(2) run-time guarantees can be obtained at the implementation level by validating optimizations performed.
We have developed an approach which is uniformly applicable at both the levels.
Verification of optimization specifications
Optimizations with similar objectives comprise of similar program transformations.
Consequently, their proofs of semantic preservation also consist of similar patterns.
To simplify specification, we structure optimizing transformations as
sequential compositions of
primitive program transformations. For each primitive,
we identify
soundness conditions which guarantee that the transformation is semantics preserving.
Proving soundness of an optimization therefore reduces to merely showing that
the soundness conditions of the underlying primitives are satisfied. This avoids repeated proofs of semantic equivalence.
We use a temporal logic to specify both program analyses and soundness conditions.
Since programs are transformed step-by-step, we need to correlate temporal properties
across transformations of programs which is not possible with the temporal logic proof system. We therefore develop a logic called
temporal transformation logic and use it to verify optimization specifications.
Tool overview:
Our deductive verification tool is based on the PVS system.
An optimization is specified in the PVS language as opt.pvs.
It defines relevant local data flow properties,
global program analyses, and an optimizing transformation.
Primitive program transformations and their soundness conditions are provided
in the OVerification library developed by us.
The specification is type checked and the tool VCGEN generates
verification conditions. The verification conditions are discharged
using the PVS theorem prover. The proofs are derived in the temporal transformation
logic encoded in the TTL library.
|
|
|
|
Formal specifications and proofs:
We have verified specifications of the following optimizations.
Common subexpression elimination. Dead code elimination.
Partial dead code elimination. Lazy code motion.
Loop invariant code motion. Optimal code motion.
|
|
Requirements:
Prototype verification system (PVS) 3.2
Download:
spotspvs.tgz (distributed under GNU GPL)
Installation and user guide:
PDF
|
Runtime validation of compiler optimizations
Our intuitive formulation of optimizing transformations as sequences of primitive program transformations
enables a novel runtime validation scheme. We
instrument an optimizer implementation
to generate a trace of its execution in terms of predefined primitive transformations.
The validation of the optimization run involves two steps:
- Conformance of trace:
The trace is simulated on the input program being optimized. If the output program thus
obtained matches with the optimized program generated by the optimizer then the
trace conforms with the execution of the optimizer.
- Model checking soundness conditions:
The temporal logic soundness conditions of the primitive transformations used in the trace
are model checked on the appropriate versions of the input program being optimized.
If the soundness conditions are satisfied then the trace preserves semantics.
Consequently, the optimizer also preserves semantics of the particular input
program.
Tool overview:
We have applied the runtime validation technique to several optimization routines of GCC 4.1.
We consider optimizations of RTL intermediate code. The instrumentation code
records the input and output programs of the optimization routine and
generates a trace of the optimization run. These are converted to a PVS file (say test.c.pvs).
The PVS file is type checked and interpreted using the TTL and OVerification libraries.
The validation is performed using the PVS ground evaluator.
The runtime validation technique does not require any information about program analyses performed by GCC.
Therefore even though the GCC code base is quite large and complex,
instrumentation is easy.
Our tool required an estimated 21 lines of instrumentation code for every 1000 lines of the GCC code considered for validation.
|
|
|
|
GCC optimizers: We have validated the following GCC optimizer implementations on sample C programs.
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).
|
|
Requirements:
Prototype verification system (PVS) 3.2
GNU compiler collection (GCC) 4.1
Download:
spotsgcc.tgz (distributed under GNU GPL)
Installation and user guide:
PDF
|
Publications
A logic for correlating temporal properties across program transformations (Under submission)
Validation of GCC optimizers through trace generation (Journal: SPE 2009)
Structuring optimizing transformations and proving them sound (ENTCS 2007)
A PVS based framework for validating compiler optimizations (SEFM 2006)
SPOTS: A system for proving optimizing transformations sound (PhD thesis)
