Jean-Baptiste Tristan
Greg Morrisett
ABSTRACT
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the design of such a validator for LLVM's intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present the results of our preliminary experiments on a set of benchmarks that include GCC, a perl interpreter, SQLite3, and other C programs.
- LLVM 2.8. http://llvm.org.Google Scholar
- SQLite 3. http://www.sqlite.org.Google Scholar
- The Motor Industry Software Reliability Association. Guidelines for the use of the c language in critical systems. http://www.misra.org.uk, 2004.Google Scholar
- Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. TVOC: A translation validator for optimizing compilers. In Computer Aided Verification, volume 3576 of Lecture Notes in Computer ScienceLNCS, pages 291--295. Springer, 2005. Google ScholarDigital Library
- SPEC CPU2006. http://www.spec.org/cpu2006/.Google Scholar
- Paul Havlak. Construction of thinned gated single-assignment form. In Proc. 6rd Workshop on Programming Languages and Compilers for Parallel Computing, pages 477--499. Springer Verlag, 1993. Google ScholarDigital Library
- John Hopcroft. An n log n algorithm for minimizing states of a finite automaton. In The Theory of Machines and Computations, 1971.Google ScholarCross Ref
- Aditya Kanade, Amitabha Sanyal, and Uday Khedker. A PVS based framework for validating compiler optimizations. In 4th Software Engineering and Formal Methods, pages 108--117. IEEE Computer Society, 2006. Google ScholarDigital Library
- Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languagessymp. Principles of Progr. Lang, pages 42--54. ACM Press, 2006. Google ScholarDigital Library
- E. Moggi. Computational lambda-calculus and monads. In 4th Logic in computer science, pages 14--23. IEEE, 1989. Google ScholarDigital Library
- George C. Necula. Translation validation for an optimizing compiler. In Programming Language Design and Implementation Prog. Lang. Design and Impl. 2000, pages 83--95. ACM Press, 2000. Google ScholarDigital Library
- Amir Pnueli and Anna Zaks. Validation of interprocedural optimization. In Proc. Workshop Compiler Optimization Meets Compiler Verification (COCV 2008), Electronic Notes in Theoretical Computer Science. Elsevier, 2008.Google Scholar
- Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, volume 1384 of Lecture Notes in Computer ScienceLNCS, pages 151--166. Springer, 1998. Google ScholarDigital Library
- Xavier Rival. Symbolic transfer function-based approaches to certified compilation. In 31st symposium Principles of Programming Languagessymp. Principles of Progr. Lang, pages 1--13. ACM Press, 2004. Google ScholarDigital Library
- Simulink. http://mathworks.com.Google Scholar
- Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: A new approach to optimization. In 36th Principles of Programming Languages, pages 264--276. ACM, 2009. Google ScholarDigital Library
- Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In 37th Principles of Programming Languages, pages 83--92. ACM Press, 2010. Google ScholarDigital Library
- Peng Tu and David Padua. Efficient building and placing of gating functions. In Programming Language Design and Implementation, pages 47--55, 1995. Google ScholarDigital Library
- Daniel Weise, Roger F. Crew, Michael D. Ernst, and Bjarne Steensgaard. Value dependence graphs: Representation without taxation. In 21st Principles of Programming Languages, pages 297--310, 1994. Google ScholarDigital Library
Index Terms
- Evaluating value-graph translation validation for LLVM
Recommendations
Alive2: bounded translation validation for LLVM
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and ImplementationWe designed, implemented, and deployed Alive2: a bounded translation validation tool for the LLVM compiler’s intermediate representation (IR). It limits resource consumption by, for example, unrolling loops up to some bound, which means there are ...
Evaluating value-graph translation validation for LLVM
PLDI '11Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In ...
Translation and Run-Time Validation of Loop Transformations
This paper presents new approaches to the validation of loop optimizations that compilers use to obtain the highest performance from modern architectures. Rather than verify the compiler, the approach of translation validation performs a validation ...
Comments