Record Details

Validation of GCC optimizers through trace generation

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Validation of GCC optimizers through trace generation
 
Creator KANADE, A
SANYAL, A
KHEDKER, UP
 
Subject compiler optimization
translation validation
gcc
temporal logic
pvs
 
Description The translation validation approach involves establishing semantics preservation of individual compilations. In this paper, we present a novel framework for translation validation of optimizers. We identify a comprehensive set of primitive program transformations that are commonly used in many optimizations. For each primitive, we define soundness conditions that guarantee. that the transformation is semantics preserving. This framework of transformations and soundness conditions is independent of any particular compiler implementation and is formalized in PVS. An optimizer is instrumented to generate the trace of an optimization run in terms of the predefined transformation-primitives. The validation succeeds if (1) the trace conforms to the optimization and (2) the soundness conditions of the individual transformations in the trace are satisfied. The first step eliminates the need to trust the instrumentation. The soundness conditions are defined in a temporal logic and therefore the second step involves model checking. Thus the scheme is completely automatable. We have applied this approach to several intraprocedural optimizations of RTL intermediate code in GNU Compiler Collection (GCC) v4.1.0, namely, loop invariant code motion, partial redundancy elimination, lazy code motion, code hoisting, and copy and constant propagation for sample programs written in a subset of the C language. The validation does not require information about program analyses performed by GCC. Therefore even though the GCC code base is quite large and complex, instrumentation could be achieved easily. The framework requires an estimated 21 lines of instrumentation code and 140 lines of PVS specifications for every 1000 lines of the GCC code considered for validation.
 
Publisher JOHN WILEY & SONS LTD
 
Date 2011-08-17T02:19:14Z
2011-12-26T12:55:17Z
2011-12-27T05:44:02Z
2011-08-17T02:19:14Z
2011-12-26T12:55:17Z
2011-12-27T05:44:02Z
2009
 
Type Article
 
Identifier SOFTWARE-PRACTICE & EXPERIENCE, 39(6), 611-639
0038-0644
http://dx.doi.org/10.1002/spe.913
http://dspace.library.iitb.ac.in/xmlui/handle/10054/9705
http://hdl.handle.net/10054/9705
 
Language en