基于模拟关系的编译优化实现正确性验证方法

doi:10.3969/j.issn.0372-2112.2012.11.005

电子学报 ›› 2012, Vol. 40 ›› Issue (11): 2171-2176.DOI: 10.3969/j.issn.0372-2112.2012.11.005

基于模拟关系的编译优化实现正确性验证方法

徐超^1,2,3, 何炎祥^1,3, 吴伟^1,3, 陈勇^1,3, 刘健博^1,3

1. 武汉大学计算机学院,湖北武汉 430072;
2. 徐州工业职业技术学院,江苏徐州 221000;
3. 软件工程国家重点实验室,湖北武汉 430072

收稿日期:2012-03-15 修回日期:2012-06-13 出版日期:2012-11-25
- 作者简介:
- 徐超 男,1980年出生,湖北红安人,博士生,讲师,CCF会员(E200019473G),研究方向为可信软件和嵌入式系统. E-mail:xuch@whu.edu.cn 何炎祥 男,1952年出生,湖北应城人,博士,教授,博士生导师,研究方向为可信软件、并行分布处理、软件工程和嵌入式系统. E-mail:yxhe@whu.edu.cn 吴伟 男,1985年,河南新县人,博士生,研究方向为可信软件和编译理论. E-mail:wuwei@whu.edu.cn 陈勇 男,1986年出生,湖南冷水江人,博士生,研究方向为可信软件和嵌入式系统. E-mail:cyong@whu.edu.cn
- 基金资助:
- 国家自然科学基金重点项目 (No.91118003); 国家自然科学基金面上项目 (No.61170022)

Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation

XU Chao^1,2,3, HE Yan-xiang^1,3, WU Wei^1,3, CHEN Yong^1,3, LIU Jian-bo^1,3

1. Wuhan University Computer of School,Wuhan,Hubei 430072,China;
2. Xuzhou College of Industrial Technology,Xuzhou,Jiangsu 221000,China;
3. State Key Laboratory of Software Engineering,Wuhan,Hubei 430072,China

Received:2012-03-15 Revised:2012-06-13 Online:2012-11-25 Published:2012-11-25
- Supported by:
- Key Program supported by National Natural Science Foundation of China (No.91118003); National Natural Science Foundation of China (No.61170022)

摘要/Abstract

摘要： 编译器中通常采用各种优化方法来提高目标代码的质量,为了实现较好的效果,一些编译优化算法通常十分复杂,很容易给可靠性和安全性带来隐患.现有的编译器缺陷大部分是由优化阶段引起的.传统的编译优化正确性研究大部分只关注优化算法的正确性,但是只有该算法被正确的实现了才能确保实际运行的优化过程是正确的.本文提出一种基于模拟关系的方法来验证编译优化实现的正确性.在每次优化结束后,我们通过建立优化前代码和优化后代码之间的模拟关系生成优化正确应满足的逻辑条件,然后验证逻辑条件是否成立从而判定编译优化的实现是否正确性.以优化编译中的常量折叠优化和变量替换的验证作为示例显示了本方法的有效性和可靠性.

关键词: 编译优化, 正确性, 模拟关系, 定理证明

Abstract: Many optimization methods are used to raise the quality of target code in the process of compiling.Because some optimization methods for compiling are too complicated,hidden dangers won't be avoided for reliability and security of compiling.The existing defects of compiler are usually caused at the optimization phase.Mostly traditional correctness of compiling optimization only focus on correctness of optimization algorithm,but only when the algorithm is implemented correctly,the optimization process run in practice can be proved to be correct.This paper proposes a method based on simulation relation to verify correctness of compiling optimization realization.We build up simulation relation between code before optimization and code after optimization to generate logic condition that the correctness optimization should satisfy,and then we verify it if logic condition is satisfied or not to judge if compiling optimization realization is correct or not after each optimization is finished.The method is proved to be effective and reliable by verifying statement exchange and variable substitution in the process of optimization compiling.

Key words: compiling optimization, correctness, simulation relation, theorem proving

中图分类号:

TP309.1

徐超, 何炎祥, 吴伟, 陈勇, 刘健博. 基于模拟关系的编译优化实现正确性验证方法[J]. 电子学报, 2012, 40(11): 2171-2176.

XU Chao, HE Yan-xiang, WU Wei, CHEN Yong, LIU Jian-bo. Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation[J]. Acta Electronica Sinica, 2012, 40(11): 2171-2176.

参考文献

[1] Lacey D'Jones ND,Wyk EV,Frederiksen CC.Compiler optimization correctness by temporal logic[J].Higher-Order and Symbolic Computation,2004,17(3):173-206.
[2] Frederiksen CC.Correctness of classical compiler optimizations using CTL[J].Electronic Notes in Theoretical Computer Science,2002,65(2):37-51.
[3] Abo AV,Sethi R,Ullman JD.Compilers:Principles,Techniques,and Tools[M].Boston:Addison-Wesley,1986:86-99.
[4] Kozen D,Patron M.Certification of compiler optimizatious using Kleene algebra with tests .In:Lloyd nE Dahl v,Furbach U.Kerber M,Lau K,Palamidessi C.Pereim LM,Sagiv Y,Stuckey PJ,eds.Proc.of the I st Int'l Conf.on Computational Logic(CL2000) .London:Springer-Verlag,2000.568-582.
[5] Benton N.Simple relational correctness proofs for static analyses and program transformations[J].ACM SIGPLAN Notices,2004.39(1):14-25.
[6] Muchnick SS.Advanced Compiler Design and Implementation[M].San Francisco:Morgan Kaufrnann Publishers,1997:106-110.
[7] Alien R,Kennedy K.Optimizing Compilers for Modem Architectures:A Dependence-Based Approach[M].San Francisco:Morgan Kaufinann Publishers,2002:23-30.
[8] Wand M.Specifying the correctness of binding time analysis .In:Deusen MV,Lang B,eds.Proc.of the 20th ACM SIGPLANSIGACT Symp.on Principles of Programming Languages .New York:ACM Press,1993.137-143.
[9] Wand M,Siveroni I.Constraint systems for useless variable elimination .In:Appel A,Aiken A .eds.Proc.of the 26th ACM SIGPLAN-SlGACT Symp.On Principles of Programming Languages .NewYork:ACMPress,1999.291-302.
[10] Kubayashi N.Type-Based useless variable elimination [J].ACM S1GPLANNotices,1999,34(11):84-93.
[11] Kozen,D Efficient code certification.Technical Report .Cornell Univer-sity,Ithaca,USA,1998:98-166.
[12] Morrisett G,Walker D,Crary K,Glew N.From system F to typed assem-bly language .ACM Transactions on Programming Languages and Systems .Tennessee,USA,1999,21(3):527-568.
[13] Necula,G.Proof-carrying code .In:Proc of the 24th ACM SIGPLAN-SIGACT SYMP .On Principles of Programming Languages,New York,USA,1997.106-119.
[14] 胡定磊,陈书明.基于互补谓词的编译优化[J].电子学报,2006,34(07):1280-1285. HU Ding-lei,CHEN Shu-ming.Optimizing compiler based on complementary predicate[J].Acta Electronica Sinica,2006,34(07):1280-1285.(in Chinese)
[15] 胡定磊,陈书明.低功耗编译技术综述[J].电子学报,2005,33(04):676-681. HU Ding-lei,CHEN Shu-ming.Low power/ energy compilation technology[J].Acta Electronica Sinica,2005,33(04):676-681.(in Chinese)
[16] 唐遇星,邓,周兴铭.基于Trace-Cache的多级动态优化框架设计[J].电子学报,2005,33(11):1946-1951. TANG Yu-xing,DENG Kun,ZHOU Xing-ming.Trace-cache based framework for mult-i level dynamic optimization[J].Acta Electronica Sinica,2005,33(11):1946-1951.(in Chinese)
[17] PC Van Oorschot.Revisiting software protection .In:Proc of 6th international Information Security Conference (ISC'03).Lecture Notes in Computer Science 2851 .Berlin:Springer-Verlag,2006.1-13.
[18] A Appel.Verified software toolchain[J].Programming Languages and Systems,2011,66(02):1-17.
[19] 何炎祥,吴伟,刘陶,等.可信编译理论及其核心实现技术[J].计算机科学与探索,2011,5(1):1-22. HE Yanxiang,WU Wei,LIU Tao.Theory and key implementation techniques of trusted compiler:A survey[J].Journal of Frontiers of Computer Science and Technology,2011,5(1):1-22.(in Chinese)
[20] X Yang,Y Chen,E Eide,J Regehr.Finding and understanding bugs in C compilers .In 32nd Conf.on Programming Language Design and Implementation (PLDI'11) .San Jose,California,2011.283-294.
[21] S Kundu,Z Tatlock,S Lerner.Proving optimizations correct using parameterized program equivalence[J].ACM Sigplan Notices,2009,44(6):327-337.
[22] Lerner S,Millstein T,Chambers C.Automatically proving the correctlless of compiler optimizations[J].ACM SIGPLAN Notices,2003,38(5):220-231.
[23] Necula GC.Translation validation for optimizing compiler[J].Acm Sigplan Notices,2000.35(5):83-94.
[24] Zaks A,Pnueli A.Program analysis for compiler validation .In:Proc.of the 8^th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering .New York,USA,2008.1-7.
[25] 聂久焘,程旭,王克义.一种高效的完全值编号算法[J].电子学报,2010,38(2):416-421. NIE Jiu-tao,CHENG Xu,WANG Ke-yi.An efficient complete global value numbering algorithm[J].Acta Electronica Sinica,2010,38(2):416-421.(in Chinese)

基于模拟关系的编译优化实现正确性验证方法

Verifying Implementation Correctness of Compiling Optimization Based on Simulation Relation

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 10

编辑推荐

Metrics

[1]	陈勇, 徐超, 何炎祥, 沈凡凡. 基于编译优化的软件缺陷预测研究[J]. 电子学报, 2021, 49(2): 216-224.
[2]	曹鹤玲, 姜淑娟, 靳小波, 杨卫东, 薛猛. 怀疑度计算公式受偶然正确性影响理论分析[J]. 电子学报, 2018, 46(6): 1365-1370.
[3]	莫启, 笪建, 代飞, 朱锐, 林雷蕾, 李彤. 正确性保证的私有过程建模方法[J]. 电子学报, 2018, 46(10): 2551-2560.
[4]	钱振江, 刘永俊, 姚宇峰, 汤力, 黄皓, 宋方敏. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017, 45(1): 251-256.
[5]	江南, 何炎祥, 张晓瞳. _mJava到Micro-Dalvik虚拟机的编译验证[J]. 电子学报, 2016, 44(7): 1619-1629.
[6]	曹鹤玲, 姜淑娟, 王兴亚, 薛猛, 钱俊彦. 面向有效错误定位的偶然正确性识别方法[J]. 电子学报, 2016, 44(12): 3026-3031.
[7]	聂久焘;程旭;王克义. 一种高效的完全值编号算法 [J]. 电子学报, 2010, 38(2): 416-421.
[8]	朱允敏, 张丽伟, 王生原, 董渊, 张素琴. 面向多核处理器的低级并行程序验证[J]. 电子学报, 2009, 37(S1): 1-6.
[9]	李信鹏, 赵文, 张世琨, 王立福. RFID网络中发现服务系统的一种形式化规约[J]. 电子学报, 2008, 36(S1): 9-18.
[10]	邓晴莺, 张民选. 基于映射表的寄存器文件设计以及编译器优化[J]. 电子学报, 2008, 36(2): 392-396.