论文部分内容阅读
循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用，证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题．形式化证明一个羽翼丰满的优化编译器本质上是不可行的，可以使用替代的方法，即不是证明优化编译器本身，而是形式化证明每一次循环变换前后编译对象的正确性．提出一种新颖的基于扩展逻辑变换系统肚TS来证明循环优化正确性的方法．系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则，经谓词抽象将源程序与目标程序转换为形式化Radl语言后，使用uTS的派生规则