计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2012年
9期
1863-1873
,共11页
循环优化%可信编译%扩展逻辑变换系统%循环变换%辅助证明算法
循環優化%可信編譯%擴展邏輯變換繫統%循環變換%輔助證明算法
순배우화%가신편역%확전라집변환계통%순배변환%보조증명산법
循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义.
循環優化對于提高Cache性能、髮掘程序的併行性以及減少執行循環的開銷都有著重要的作用,證明帶循環優化功能的現代編譯器的正確性已成為可信編譯的一箇挑戰性的問題.形式化證明一箇羽翼豐滿的優化編譯器本質上是不可行的,可以使用替代的方法,即不是證明優化編譯器本身,而是形式化證明每一次循環變換前後編譯對象的正確性.提齣一種新穎的基于擴展邏輯變換繫統μTS來證明循環優化正確性的方法.繫統μTS在邏輯變換繫統TS的基礎上擴展瞭若榦條派生規則,經謂詞抽象將源程序與目標程序轉換為形式化Radl語言後,使用μTS的派生規則能證明常見循環變換的正確性,如循環融閤、循環分配、循環交換、循環反轉、循環分裂、循環脫皮、循環調整、循環展開、循環鋪蓋、循環判斷外提、循環不變代碼外提等.循環優化可以看作一繫列循環變換的組閤,從而繫統μTS能證明循環優化的正確性.為瞭支持自動化證明循環優化的正確性併齣示證據,進一步提齣瞭一箇輔助證明算法.最後通過一箇典型實例對這一方法進行瞭詳細的闡述,實際效果錶明瞭該方法的有效性.該方法對設計高可信優化編譯器具有重要的指導意義.
순배우화대우제고Cache성능、발굴정서적병행성이급감소집행순배적개소도유착중요적작용,증명대순배우화공능적현대편역기적정학성이성위가신편역적일개도전성적문제.형식화증명일개우익봉만적우화편역기본질상시불가행적,가이사용체대적방법,즉불시증명우화편역기본신,이시형식화증명매일차순배변환전후편역대상적정학성.제출일충신영적기우확전라집변환계통μTS래증명순배우화정학성적방법.계통μTS재라집변환계통TS적기출상확전료약간조파생규칙,경위사추상장원정서여목표정서전환위형식화Radl어언후,사용μTS적파생규칙능증명상견순배변환적정학성,여순배융합、순배분배、순배교환、순배반전、순배분렬、순배탈피、순배조정、순배전개、순배포개、순배판단외제、순배불변대마외제등.순배우화가이간작일계렬순배변환적조합,종이계통μTS능증명순배우화적정학성.위료지지자동화증명순배우화적정학성병출시증거,진일보제출료일개보조증명산법.최후통과일개전형실례대저일방법진행료상세적천술,실제효과표명료해방법적유효성.해방법대설계고가신우화편역기구유중요적지도의의.
