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

摘要：TRANS是基于CTL的優(yōu)化變換描述語言，對TRANS語言作了宏擴(kuò)展，給出了循環(huán)嵌套、循環(huán)歸納變量、循環(huán)依賴及方向向量的時序邏輯描述。從依賴分析的角度對重排序循環(huán)優(yōu)化變換加以考查，并以循環(huán)逆轉(zhuǎn)和循環(huán)交換為例闡述了其形式化描述方法。

關(guān)鍵詞：循環(huán)優(yōu)化變換； 分支時序邏輯； 依賴分析

中圖分類號：TP311．5文獻(xiàn)標(biāo)志碼：A

文章編號：1001－3695(2007)07－0049－03

0引言

優(yōu)化變換是程序的等價性變換，其目的是提高目標(biāo)程序的執(zhí)行性能，或縮短目標(biāo)程序的代碼規(guī)模、降低程序的運(yùn)行功耗等。通常，程序大多數(shù)的執(zhí)行時間都耗費(fèi)在循環(huán)上，旨在發(fā)掘和提高循環(huán)并發(fā)度的優(yōu)化是現(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)化變換作出精確刻畫，難以生成有針對性的測試用例，從而導(dǎo)致測試冗余。

文獻(xiàn)[2]提出了一種基于CTL的程序變換語義等價性的證明方法。它通過歸納法證明程序π和變換后的程序π′的計(jì)算序列之間存在互模擬關(guān)系R，從而證明程序π與程序π′之間的語義等價。證明程序變換的正確性需要對變換作出準(zhǔn)確的形式化描述。文獻(xiàn)[2]給出了優(yōu)化變換描述語言TRANS，采用帶條件的重寫規(guī)則I(xiàn)→I′ if conditions描述變換，變換條件用CTL公式表示。文獻(xiàn)[2]對A.V.Aho等人[3]概括的古典優(yōu)化變換從數(shù)據(jù)流和控制流的角度加以考查，并應(yīng)用TRANS語言進(jìn)行描述，但對文獻(xiàn)[4]中概括的循環(huán)分布、循環(huán)逆轉(zhuǎn)、循環(huán)交換等基于依賴分析的循環(huán)優(yōu)化變換難以適用。

1基于CTL的優(yōu)化變換描述語言TRANS

TRANS是一種基于CTL的優(yōu)化變換描述語言[2]，其描述變換的通用形式依賴于某些條件的一系列動作：

3基于依賴分析的循環(huán)優(yōu)化形式化描述

在現(xiàn)代編譯器中，循環(huán)優(yōu)化變換通常被用來增強(qiáng)并行性和存儲訪問局部性。許多優(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ā)給出了重排序循環(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)變換為

圖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進(jìn)行了宏擴(kuò)展，以宏的形式給出了循環(huán)嵌套、循環(huán)歸納變量、循環(huán)依賴以方向向量的時序邏輯描述，擴(kuò)展了TRANS語言的描述能力。從依賴保持的角度出發(fā)，用時序邏輯公式對重排序循環(huán)優(yōu)化變換的條件進(jìn)行描述，從而對該類優(yōu)化變換作出了精確和簡潔的形式化刻畫。今后的工作包括：①由于存在相當(dāng)一部份的循環(huán)優(yōu)化變換依賴于特定的機(jī)器特性，希望將來引入對機(jī)器特性的描述，從而對這類優(yōu)化變換給出刻畫方法；②將這一描述結(jié)果用于指導(dǎo)針對編譯優(yōu)化的測試用例生成，提升JTT工具的測試能力；③在這一描述結(jié)果的基礎(chǔ)上，從依賴保持的角度出發(fā)，給出循環(huán)優(yōu)化變換正確性的證明。

參考文獻(xiàn)：

[1]朱丹楓.一種用于測試編譯優(yōu)化的程序控制結(jié)構(gòu)生成算法[D].北京:中國科學(xué)院軟件研究所， 2005.

[2]LACEY D. Program transformation using temporal logic specification[D]. Oxford: Oxford University Computing Laboratory， 2003.

[3]AHO A V， SETHI R， ULLMAN J D. Compilers: principles， techniques， and tools[M]. Boston: Addison Wesley， 1986.

[4]ALLEN R， KENNEDY K. Optimizing compilers for modern architectures[M].San Fransisco: Morgan Kaufmann， 2002.

[5]CLARKE E M， EMERSON E A， SISTLA A P. Automatic verification of finite－state concurrent systems using temporal logic specifications[J]. ACM Transactions on Programming Languages and Systems， 1986，8（2）:244－263.

注：“本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文”