AI帮你理解科学

AI 生成解读视频

AI抽取解析论文重点内容自动生成视频


pub
生成解读视频

AI 溯源

AI解析本论文相关学术脉络


Master Reading Tree
生成 溯源树

AI 精读

AI抽取本论文的概要总结


微博一下
The main message of this paper is that a practical translation validation infrastructure, able to handle many of the common optimizations in a realistic compiler can be implemented with about the effort typically required to implement one compiler pass, say common subexpression e...

Translation validation for an optimizing compiler

PLDI '02 Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implement..., no. 5 (2000): 83-94

被引用529|浏览111
EI
下载 PDF 全文
引用
微博一下

摘要

We describe a translation validation infrastructure for the GNU C compiler. During the compilation the infrastructure compares the intermediate form of the program before and after each compiler pass and verifies the preservation of semantics. We discuss a general framework that the optimizer can use to communicate to the validator what t...更多

代码

数据

简介
  • Despite a large body of work [CM75, MP67, Mor73, Moo89, You89, WO92] in the area of compiler verification the authors are still far from being able to prove automatically that a given optimizing compiler always produces target programs that are semantically equivalent to their source versions.
  • If the authors cannot prove that a compiler is always correct maybe the authors can at least check the correctness of each compilation
  • This observation has inspired the technique of translation validation [PSS98] whose goal is to check the result of each compilation against the source program and to detect and pinpoint compilation errors on-the-fly.
  • With a translation validation infrastructure for the GNU C optimizing compiler.
  • One might argue that errors in commercial compilers are the least likely source of headaches for most programmers.
  • Compiler testing is bound to become more important and more tedious as more demanding architectures are being used as targets
重点内容
  • Despite a large body of work [CM75, MP67, Mor73, Moo89, You89, WO92] in the area of compiler verification we are still far from being able to prove automatically that a given optimizing compiler always produces target programs that are semantically equivalent to their source versions
  • The main message of this paper is that a practical translation validation infrastructure, able to check the correctness of many of the transformations performed by a realistic compiler, can be implemented with about the effort typically required to implement one compiler pass
  • We demonstrate this in the context of the GNU C compiler for a number of its optimizations while compiling realistic programs such as the compiler itself or the Linux kernel
  • The main message of this paper is that a practical translation validation infrastructure, able to handle many of the common optimizations in a realistic compiler can be implemented with about the effort typically required to implement one compiler pass, say common subexpression elimination
  • We believe this price is small considering the qualitative increase in the effectiveness of compiler testing and error isolation
结论
  • The main message of this paper is that a practical translation validation infrastructure, able to handle many of the common optimizations in a realistic compiler can be implemented with about the effort typically required to implement one compiler pass, say common subexpression elimination
  • The authors demonstrate this in the context of the GNU C compiler for a number of its optimizations.
  • The authors believe that a significant improvement is possible once the authors memoize all constraints that were generated and processed
表格
  • Table1: Sizes of the software systems for which we ran translation validation
  • Table2: A synthesis of the false alarm ratios we observe at present and the validation time for compiling gcc, for several of the passes
Download tables as Excel
相关工作
  • The primary inspiration for this work was the original work on translation validation by Pnueli, Siegel and Singerman [PSS98] and our own work on certifying compilation [NL98, Nec98]. In a sense this project can be seen as tackling the goals laid out in [PSS98] using the symbolic evaluation techniques from [Nec98], in the context of a realistic compiler. Additional innovations were required to handle optimizations like spilling and to overcome the lack of assistance from the optimizer. This is made possible in our case by a few key techniques among which the most important is symbolic evaluation. The advance of the present work over [PSS98] and other similar work [C+97, Goe97], is that the language involved and the range of optimizations handled here are much more ambitious. In [PSS98] translation validation is applied to the non-optimizing compilation of SIGNAL to C. In [C+97] the compiler translates expressions into a fragment of RTL without loops and function calls. In this case, and also in recent work of Kozen [Koz98], validation is simplified considerably by restricting the optimizations such that each source-level construct is compiled into a given pattern in the target code, and no inter-pattern optimizations are allowed.
基金
  • This research was supported in part by the National Science Foundation Grants No CCR-9875171 and CCR0081588, NSF Infrastructure Grant No EIA-9802069, and gifts from AT&T and Intel
引用论文
  • Martin Abadi, Luca Cardelli, P.-L. Curien, and J.-J Levy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, October 1991.
    Google ScholarLocate open access versionFindings
  • Alessandro Cimatti et al. A provably correct embedded verifier for the certification of safety critical software. In Computer Aided Verification. 9th International Conference. Proceedings, pages 202–213. Springer-Verlag, June 1997.
    Google ScholarLocate open access versionFindings
  • Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. ACM SIGPLAN Notices, 35(5):95–107, May 2000.
    Google ScholarLocate open access versionFindings
  • L. M. Chirica and D. F. Martin. An approach to compiler correctness. ACM SIGPLAN Notices, 10(6):96–103, June 1975.
    Google ScholarLocate open access versionFindings
  • Cygnus Solutions. DejaGnu Testing Framework. http://www.gnu.org/software/dejagnu/dejagnu.html.
    Findings
  • Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
    Google ScholarFindings
  • Wolfgang Goerigk. Towards rigorous compiler implementation verification. In Rudolf Berghammer, editor, Proc. of the 1997 Workshop on Programming Languages and Fundamentals of Programming, pages 118–126, 1997.
    Google ScholarLocate open access versionFindings
  • Susan Horowitz, Jan Prins, and Tom Reps. On the adequacy of program dependence graphs for representing programs. In Proceedings of the Fifteenth Annual ACM Symposium on the Principles of Programming Languages, pages 146–157, San Diego, CA, January 1988.
    Google ScholarLocate open access versionFindings
  • Dexter Kozen. Efficient code certification. Technical Report TR 98–1661, Cornell University, January 1998.
    Google ScholarFindings
  • [MCG+99] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25–35, 1999.
    Google ScholarLocate open access versionFindings
  • [Mic99] Microsoft Corporation. Microsoft Developer Network Library, March 1999.
    Google ScholarLocate open access versionFindings
  • J. Strother Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461–492, December 1989.
    Google ScholarLocate open access versionFindings
  • F. Lockwood Morris. Advice on structuring compilers and proving them correct. In Proceedings of the First ACM Symposium on Principles of Programming Languages, pages 144–152, 1973.
    Google ScholarLocate open access versionFindings
  • John McCarthy and James Painter. Correctness of a compiler for arithmetic expressions. In J. T. Schwartz, editor, Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967.
    Google ScholarLocate open access versionFindings
  • George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998. Also available as CMU-CS-98-154.
    Google ScholarFindings
  • George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN’98 Conference on Programming Language Design and Implementation, pages 333– 344, June 1998.
    Google ScholarLocate open access versionFindings
  • Martin Rinard. Credible compilers. Technical Report MIT/LCS/TR-776, Massachusetts Institute of Technology, December 1999.
    Google ScholarFindings
  • Martin Rinard and Darko Marinov. Credible compilation. In Proceedings of the Run-Time Result Verification Workshop, July 1999.
    Google ScholarLocate open access versionFindings
  • G. Ramalingam and Thomas Reps. Semantics of program representation graphs. Technical Report CS-TR-89-900, University of Wisconsin, Madison, December 1989.
    Google ScholarFindings
  • [TMC+96] David Tarditi, J. Gregory Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In PLDI’96 Conference on Programming Language Design and Implementation, pages 181–192, May 1996.
    Google ScholarLocate open access versionFindings
  • [WCES94] Daniel Weise, Roger F. Crew, Michael Ernst, and Bjarne Steensgaard. Value dependence graphs: representation without taxation. In Proceedings of POPL ’94, 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 297–310, January 1994.
    Google ScholarLocate open access versionFindings
  • Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 151–160, 1992.
    Google ScholarLocate open access versionFindings
  • Wuu Yang, Susan Horowitz, and Thomas Reps. A program integration algorithm that accommodates semantics-preserving transformations. acm Transactions of Software Engineering and Methodology, 1(3):310–354, July 1992.
    Google ScholarLocate open access versionFindings
  • William D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5(4):493–518, December 1989.
    Google ScholarLocate open access versionFindings
您的评分 :
0

 

标签
评论
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科