基于ＣＴＬ的循環優化變換描述方法

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

關鍵詞：循環優化變換； 分支時序邏輯； 依賴分析

中圖分類號：TP311．5文獻標志碼：A

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

0引言

優化變換是程序的等價性變換，其目的是提高目標程序的執行性能，或縮短目標程序的代碼規模、降低程序的運行功耗等。通常，程序大多數的執行時間都耗費在循環上，旨在發掘和提高循環并發度的優化是現代高性能體系結構下的主要編譯優化方法之一。如果變換后的程序與變換前的程序語義等價，則程序變換是正確的。軟件測試是保證程序變換正確性的方法之一。JTT是一種編譯優化自動化測試工具，用于嵌入式環境下的C++優化編譯器的系統測試和回歸測試[1]。JTT工具的使用能較大地提高被測編譯器系統中優化功能模塊的語句覆蓋率，使得系統的可靠性得到較大改善。然而JTT工具并沒有對優化變換作出精確刻畫，難以生成有針對性的測試用例，從而導致測試冗余。

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

1基于CTL的優化變換描述語言TRANS

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

3基于依賴分析的循環優化形式化描述

在現代編譯器中，循環優化變換通常被用來增強并行性和存儲訪問局部性。許多優化變換包括循環分布、循環合并、循環逆轉、循環交換、循環分片等都是重排序變換，它僅改變代碼的執行次序而不增加或減少任何語句的執行。任何一種重排序變換如果維持程序中每一個依賴，那么此變換將維持該程序的含義。絕大多數的重排序循環優化變換只改變循環嵌套中某一層或某幾層循環的迭代順序，因而它僅需維持部分依賴就可維持程序的含義。該章從依賴保持的角度出發給出了重排序循環優化變換的形式化描述，并以循環逆轉、循環交換為例闡述了該方法。此外，本章關注迭代步長為1的For循環，其他循環可以通過循環規范化轉換為該類型的循環[4]。

3．1循環逆轉

循環逆轉是在循環迭代范圍內改變循環遍歷的方向。下面的代碼：

通過循環逆轉變換為

圖2給出了上面代碼在逆轉前和逆轉后的控制流圖。

為描述循環逆轉，必須從循環嵌套中識別出需要逆轉的循環。假設對n層循環嵌套中的第k層循環作逆轉，那么根據本文2．1節中循環和循環嵌套的宏定義有

4結束語

本文對基于CTL的優化變換描述語言TRANS進行了宏擴展，以宏的形式給出了循環嵌套、循環歸納變量、循環依賴以方向向量的時序邏輯描述，擴展了TRANS語言的描述能力。從依賴保持的角度出發，用時序邏輯公式對重排序循環優化變換的條件進行描述，從而對該類優化變換作出了精確和簡潔的形式化刻畫。今后的工作包括：①由于存在相當一部份的循環優化變換依賴于特定的機器特性，希望將來引入對機器特性的描述，從而對這類優化變換給出刻畫方法；②將這一描述結果用于指導針對編譯優化的測試用例生成，提升JTT工具的測試能力；③在這一描述結果的基礎上，從依賴保持的角度出發，給出循環優化變換正確性的證明。

參考文獻：

[1]朱丹楓.一種用于測試編譯優化的程序控制結構生成算法[D].北京:中國科學院軟件研究所， 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.

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