Proving Soundness of Program Transformations in Optimizing Compilation Based on Temporal Logic
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [16]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    Two kinds of program transformations widely-used in optimizing compilation, statement exchange and variable substitution, are investigated and their soundness conditions are formally defined with CTL-FV, an extension of the temporal logic CTL (computation tree logic). Sound statement exchange Texch and sound variable substitution Tsub are defined with conditioned rewriting rules and their soundness is proved under an inductive proof frame. In addition, based on Texch, the soundess of another transformation, dependence-preserving statement reordering inside basic blocks of programs, is also proved with a constructive method.

    Reference
    [1] Aho AV, Sethi R, Ullman JD. Compilers: Principles, Techniques, and Tools. Boston: Addison-Wesley, 1986.
    [2] Muchnick SS. Advanced Compiler Design and Implementation. San Francisco: Morgan Kaufmann Publishers, 1997.
    [3] Allen R, Kennedy K. Optimizing Compilers for Modern Architectures: A Dependence-Based Approach. San Francisco: Morgan Kaufmann Publishers, 2002.
    [4] Soffa ML. Developing a foundation for code optimization. In: Duesterwald E, ed. Proc. of the 13th Int’l Conf. of Compiler Construction (CC 2004). London: Springer-Verlag, 2004. 1?4.
    [5] Lacey D, Jones ND, Wyk EV, Frederiksen CC. Compiler optimization correctness by temporal logic. Higher-Order and Symbolic Computation, 2004,17(3):173?206.
    [6] Frederiksen CC. Correctness of classical compiler optimizations using CTL. Electronic Notes in Theoretical Computer Science, 2002,65(2):37?51.
    [7] Wand M. Specifying the correctness of binding-time analysis. In: Deusen MV, Lang B, eds. Proc. of the 20th ACM SIGPLAN- SIGACT Symp. on Principles of Programming Languages (POPL’93). New York: ACM Press, 1993. 137?143.
    [8] Wand M, Siveroni I. Constraint systems for useless variable elimination. In: Appel A, Aiken A, eds. Proc. of the 26th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL’99). New York: ACM Press, 1999. 291?302.
    [9] Kobayashi N. Type-Based useless variable elimination. ACM SIGPLAN Notices, 1999,34(11):84?93.
    [10] Kozen D, Patron M. Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd JW, Dahl V, Furbach U, Kerber M, Lau K, Palamidessi C, Pereira LM, Sagiv Y, Stuckey PJ, eds. Proc. of the 1st Int’l Conf. on Computational Logic (CL 2000). London: Springer-Verlag, 2000. 568?582.
    [11] Benton N. Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Notices, 2004, 39(1):14?25.
    [12] Lerner S, Millstein T, Chambers C. Automatically proving the correctness of compiler optimizations. ACM SIGPLAN Notices, 2003,38(5):220?231.
    [13] Necula GC. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000,35(5):83?94.
    [14] Kossatchev AS, Posypkin MA. Survey of compiler testing methods. Programming and Computing Software, 2005,31(1):10?19.
    [15] Tao QM, Zhao C, Guo L. Soundness proof of the program transformation of variable substitution. Technical Report, No.NERCFS20080315, Beijing: National Engineering Research Center for Fundamental Software, Institute of Software, the Chinese Academy of Sciences, 2008 (in Chinese with English abstract). 附中文参考文献:
    [15] 陶秋铭,赵琛,郭亮.变量替换程序变换的保义性证明.科技报告,No.NERCFS20080315,北京:中国科学院软件研究所基础软件国家工程研究中心,2008.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

陶秋铭,赵琛,郭亮.基于时序逻辑证明编译优化程序变换的保义性.软件学报,2009,20(8):2074-2086

Copy
Share
Article Metrics
  • Abstract:5012
  • PDF: 5677
  • HTML: 0
  • Cited by: 0
History
  • Received:December 28,2007
  • Revised:April 30,2008
You are the first2033259Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063