基于ＣＴＬ的循環(huán)優(yōu)化變換描述方法

1、基于的循環(huán)優(yōu)化變換描述方法         這篇基于的循環(huán)優(yōu)化變換描述方法的關(guān)鍵詞是循環(huán)優(yōu)化變換,分支時序邏輯,依賴分析,                    摘要：TRANS是基于CTL的優(yōu)化變換描述語言，對TRANS語言作了宏擴展，給出了循環(huán)嵌套、循環(huán)歸納變量、循環(huán)依賴及方向向量的時序邏輯描述。從依賴分析的角度對

2、重排序循環(huán)優(yōu)化變換加以考查，并以循環(huán)逆轉(zhuǎn)和循環(huán)交換為例闡述了其形式化描述方法。        關(guān)鍵詞：循環(huán)優(yōu)化變換; 分支時序邏輯; 依賴分析        0引言        優(yōu)化變換是程序的等價性變換，其目的是提高目標程序的執(zhí)行性能，或縮短目標程序的代碼規(guī)模、降低程序的運行功耗等。通常，程序大多數(shù)的執(zhí)行時間都耗費在循環(huán)上，旨在發(fā)掘和提高循環(huán)并發(fā)度的優(yōu)化

3、是現(xiàn)代高性能體系結(jié)構(gòu)下的主要編譯優(yōu)化方法之一。如果變換后的程序與變換前的程序語義等價，則程序變換是正確的。軟件測試是保證程序變換正確性的方法之一。JTT是一種編譯優(yōu)化自動化測試工具，用于嵌入式環(huán)境下的C+優(yōu)化編譯器的系統(tǒng)測試和回歸測試1。JTT工具的使用能較大地提高被測編譯器系統(tǒng)中優(yōu)化功能模塊的語句覆蓋率，使得系統(tǒng)的可靠性得到較大改善。然而JTT工具并沒有對優(yōu)化變換作出精確刻畫，難以生成有針對性的測試用例，從而導致測試冗余。        文獻2提出了一種基于CTL的程序變換語義等價性的證明方法。它通過歸納法證明程

4、序和變換后的程序的計算序列之間存在互模擬關(guān)系R，從而證明程序與程序之間的語義等價。證明程序變換的正確性需要對變換作出準確的形式化描述。文獻2給出了優(yōu)化變換描述語言TRANS，采用帶條件的重寫規(guī)則II if conditions        1基于CTL的優(yōu)化變換描述語言TRANS        TRANS是一種基于CTL的優(yōu)化變換描述語言2，其描述變換的通用形式依賴于某些條件的一系列動作：    

5、;    3基于依賴分析的循環(huán)優(yōu)化形式化描述        在現(xiàn)代編譯器中，循環(huán)優(yōu)化變換通常被用來增強并行性和存儲訪問局部性。許多優(yōu)化變換包括循環(huán)分布、循環(huán)合并、循環(huán)逆轉(zhuǎn)、循環(huán)交換、循環(huán)分片等都是重排序變換，它僅改變代碼的執(zhí)行次序而不增加或減少任何語句的執(zhí)行。任何一種重排序變換如果維持程序中每一個依賴，那么此變換將維持該程序的含義。絕大多數(shù)的重排序循環(huán)優(yōu)化變換只改變循環(huán)嵌套中某一層或某幾層循環(huán)的迭代順序，因而它僅需維持部分依賴就可維持程序的含義。該章從依賴保持的角度出發(fā)給出了

6、重排序循環(huán)優(yōu)化變換的形式化描述，并以循環(huán)逆轉(zhuǎn)、循環(huán)交換為例闡述了該方法。此外，本章關(guān)注迭代步長為1的For循環(huán)，其他循環(huán)可以通過循環(huán)規(guī)范化轉(zhuǎn)換為該類型的循環(huán)4。        3.1循環(huán)逆轉(zhuǎn)        循環(huán)逆轉(zhuǎn)是在循環(huán)迭代范圍內(nèi)改變循環(huán)遍歷的方向。下面的代碼：        通過循環(huán)逆轉(zhuǎn)變換為     &

7、#160;  圖2給出了上面代碼在逆轉(zhuǎn)前和逆轉(zhuǎn)后的控制流圖。        為描述循環(huán)逆轉(zhuǎn)，必須從循環(huán)嵌套中識別出需要逆轉(zhuǎn)的循環(huán)。假設(shè)對n層循環(huán)嵌套中的第k層循環(huán)作逆轉(zhuǎn)，那么根據(jù)本文2.1節(jié)中循環(huán)和循環(huán)嵌套的宏定義有        4結(jié)束語        本文對基于CTL的優(yōu)化變換描述語言TRANS進行了宏擴展，以宏的形式給出了循環(huán)嵌套、

8、循環(huán)歸納變量、循環(huán)依賴以方向向量的時序邏輯描述，擴展了TRANS語言的描述能力。從依賴保持的角度出發(fā)，用時序邏輯公式對重排序循環(huán)優(yōu)化變換的條件進行描述，從而對該類優(yōu)化變換作出了精確和簡潔的形式化刻畫。今后的工作包括：由于存在相當一部份的循環(huán)優(yōu)化變換依賴于特定的機器特性，希望將來引入對機器特性的描述，從而對這類優(yōu)化變換給出刻畫方法;將這一描述結(jié)果用于指導針對編譯優(yōu)化的測試用例生成，提升JTT工具的測試能力;在這一描述結(jié)果的基礎(chǔ)上，從依賴保持的角度出發(fā)，給出循環(huán)優(yōu)化變換正確性的證明。        參考文獻： 

9、;       1朱丹楓.一種用于測試編譯優(yōu)化的程序控制結(jié)構(gòu)生成算法D.北京:中國科學院軟件研究所, 2005.        2LACEY D. Program transformation using temporal logic specificationD. Oxford: Oxford University Computing Laboratory, 2003.      &#

10、160; 3AHO A V, SETHI R, ULLMAN J D. Compilers: principles, techniques, and toolsM. Boston: Addison Wesley, 1986.        4ALLEN R, KENNEDY K. Optimizing compilers for modern architecturesM.San Fransisco: Morgan Kaufmann, 2002.        5CLARKE E M, EMERSON E A, SISTLA A P. Automatic verification of finite-stat