读PLDI 04 Best Paper Award 《Automatically Proving the Correctness of Compiler Optimizations》
By Sorin Lerner.Todd Millstein and Craig Chambers in Washington U
本博自从接触编译器到现在,几乎都每天都能听到bug这个关键字,编译器中的bug很痛苦,首先,人写的程序很复杂,编译器设计者很难想出所有的情况并一并处理之;其次,编译器的bug很难调,要先排除程序本身的错,接着需要知道到底是分析时出错还是变换时出错;还有这些错都是在怎样的分析和变换中出了错;最后还要担心错误会不会越不越多,没有对编译器整体的理解,很难给编译器打上正确的补丁,从而有可能这个例子补对了,其他又错了一片.
作者在文章里就编译优化正确性的自动证明做了一些尝试,这些尝试在读完文章之后觉得很了不起,只是这里面提到的工作做下来,也是需要很大的积累和投入.作者的尝试我概括如下:将优化分为转换和具体优化两个部分.代码的转换是所有优化都要做的,而并非所有的转换都是优化,所以作者通过增加利益驱动模块来判断某个转换是否是优化,这样优化的自动证明问题,就变成了某个转换正确性的自动证明问题;正确性的定义:转换前后的语义保持不变.接着作者按照转换依据的信息来自转换语句之前还是之后,将转换分成两种模式,即前向转换模式和后向转换模式.然后分别对这两种模式进行讨论,而自动证明也分别针对这两种模式来论述. Continue reading »
近期评论