Information Technology Reference
In-Depth Information
this reason, it is not possible yet to test the framework against “real” programs
that contain many currently unsupported instructions and data types.
Ensuring the correctness of program transformations - in particular, compiler
optimizations - is a long-standing research problem. In [6], Leroy gives a nice
technical and historical view of approaches to this question. A primary approach
is to formally prove each transformation correct, over all legal input programs.
This is done, for example, in the CompCert project [5], and in [2], which derives
and proves correct optimizations using denotational semantics and a relational
version of Hoare's logic Formal verification of a full-fledged optimizing compiler
is often infeasible, due to its size, evolution over time, and, possibly, proprietary
considerations.
Translation Validation
offers an alternative to full verification. A
primary assumption of this approach is that the validator has limited knowledge
of the transformation process. Hence, a variety of methods for translation vali-
dation arise (cf. [9,8,11,13,14,12]), each making choices between the flexibility of
the program syntax and the set of possible optimizations that are handled. As
details of the optimization are assumed to be unknown, heuristics are used, which
naturally limits the scope of the method. Recently, [1] proposes a method for
proving equivalence based on relational Hoare logic; it resembles our witnesses,
yet is closer to translation validation and has similar limitations.
Since we assume the optimization process is visible to the witness generator,
the generator is able to make use of auxiliary invariants derived by the opti-
mizer in order to produce a witness. This implies that witness generation is, in
principle, applicable to any optimization.
Acknowledgements.
This material is based on research sponsored by DARPA
under agreement number FA8750-12-C-0166.The U.S. Government is authorized
to reproduce and distribute reprints for Governmental purposes notwithstanding
any copyright notation thereon. The views and conclusions contained herein are
those of the authors and should not be interpreted as necessarily representing
the ocial policies or endorsements, either expressed or implied, of DARPA or
the U.S. Government.
References
1. Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs
for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013.
LNCS, vol. 7734, pp. 29-43. Springer, Heidelberg (2013)
2. Benton, N.: Simple relational correctness proofs for static analyses and program
transformations. In: POPL, pp. 14-25 (2004)
3. de Moura, L., Bjørner, N.: Z3: An ecient SMT solver. In: Ramakrishnan, C.R.,
Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg
(2008)
4. Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program
analysis & transformation. In: CGO, pp. 75-88 (2004),
llvm.org
5. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler
with a proof assistant. In: POPL, pp. 42-54. ACM (2006)
