孟凡奇

(東北電力大學信息工程學院，吉林吉林132012)

最差情況執(zhí)行時間(Worst－case Execution Time，WCET)是指程序P在處理器X上的執(zhí)行時間上限b。對于任何輸入，程序P在處理器X上的執(zhí)行時間都不超過b［1］。對于某些具有實時性要求的安全關鍵系統(tǒng)而言，其控制程序的執(zhí)行時間一旦超出預定的截止時間則可能造成災難性的后果。例如汽車的防抱死制動系統(tǒng)，如果控制程序計算延遲較大，則緊急制動時的距離就會增加，那意味著交通事故發(fā)生的可能性和嚴重性都會增加。因此，近年來很多領域的安全標準(例如 DO－178、ISO－26262、IEC－61508和CENELEC EN－50128)都要求提供系統(tǒng)中程序的最差情況執(zhí)行時間，以證明軟件沒有違背相關的安全目標［2］。

由于程序的WCET受到其自身結構、目標處理器的屬性和狀態(tài)以及系統(tǒng)運行環(huán)境的多重影響，因此獲得精確的WCET幾乎是不可能的，只能通過測量或者分析給出一個估計值［3］。目前，常用的WCET估計方法主要有動態(tài)測量與靜態(tài)分析兩類方法。在此基礎上又演化出混合方法、基于模擬的方法以及基于機器學習的方法［4］等等。

動態(tài)測量是通過實際運行程序觀察其執(zhí)行時間的方法［5］。由于難以窮盡程序所有可能的執(zhí)行路徑，因此，測量的WCET往往小于(至多等于)程序實際的WCET［6］。這意味著，用此值判定程序一定能在截止時間內完成是不可信的［7］(本領域稱之為“不安全”)。所以動態(tài)測量的方法通常用于非安全關鍵領域(如航模)。

靜態(tài)方法無需運行待測程序，而是通過對程序控制流的分析計算WCET。由于有堅實的理論基礎，因此計算出的WCET比實際的大(是安全的)。也就是說，如果此WCET值能夠滿足截止時間要求，那么實際的WCET一定會在安全截止時間之內。

靜態(tài)分析方法是安全關鍵領域中程序WCET估計的主流，其中最常用的是隱藏路徑枚舉技術(implicit path enumeration technique，IPET)。其核心思想是針對程序控制流圖中每個基本塊的執(zhí)行次數建立一系列線性約束，并通過整數規(guī)劃求解執(zhí)行時間最大值［8］。

盡管隱藏路徑枚舉技術能夠獲得大于實際WCET的估計值，但是傳統(tǒng)的局部約束法過于保守，尤其是對于含有非正交多重嵌套循環(huán)(或遞歸)語句的程序，會使WCET估計值過高。從軟件開發(fā)的角度看，過高的估計值會使程序的性能被嚴重低估，從而增添不必要的優(yōu)化工作，抬高開發(fā)成本，甚至延誤工期。從任務調度的角度看，過高的估計值會浪費大量的系統(tǒng)資源，有時還會由于資源緊張而導致任務無法調度。本文余下部分首先用實驗說明含非正交多重嵌套循環(huán)(或遞歸)語句的程序WCET被高估的現象及原因;然后提出針對這種高估的二次修正方法;最后用實驗說明該方法的有效性。

1 循環(huán)邊界對WCET估計精度的影響實驗

眾所周知，程序的循環(huán)次數對執(zhí)行時間是有影響的，通常循環(huán)次數越多，程序執(zhí)行時間越長。因此，目前所有的靜態(tài)方法在計算WCET之前都需要知道(自動分析或人工標注)循環(huán)邊界(循環(huán)次數的上下界)，以便使 WCET 估計值更精確［9－10］。

定義1 循環(huán)邊界是指循環(huán)語句的循環(huán)體在程序正常運行的情況下所有可能的執(zhí)行次數范圍。局部循環(huán)邊界是指循環(huán)語句執(zhí)行1次，其循環(huán)體可能的執(zhí)行次數范圍。全局循環(huán)邊界是指程序執(zhí)行1次，循環(huán)語句的循環(huán)體可能的全部執(zhí)行次數范圍。

需要說明的是，由于WCET計算的是最差情況，因此，通常僅需要提供循環(huán)上界。以下面的代碼為例，第1行for語句的“局部”和“全局”循環(huán)上界都是5。第2行for語句的局部循環(huán)上界是5，全局循環(huán)上界是25。

可以使用局部約束法或全局約束法為計算WCET的整數線性規(guī)劃提供所需的循環(huán)上界的表達式。局部約束法使用局部循環(huán)上界，WCET分析工具會將局部循環(huán)上界轉換成內外層語句執(zhí)行次數的整數倍關系。以上面的代碼為例，如果第2行for語句的循環(huán)邊界使用局部約束法，則會生成類似“l(fā)ine2=5 line1”的表達式，其含義為第1行for語句每執(zhí)行1次，第2行for語句執(zhí)行5次。而全局約束法使用全局循環(huán)邊界，若第2個for語句使用全局約束，則會生成類似“l(fā)ine2=25”的表達式，即程序執(zhí)行1次，第2行for語句的循環(huán)體會執(zhí)行25次。

通常情況下，由于局部循環(huán)邊界易于獲取，所以局部約束法是較為常見的循環(huán)邊界標注方法。然而，對于上下文敏感的循環(huán)，尤其是非正交多重嵌套循環(huán)，獲取內循環(huán)語句的局部循環(huán)邊界并不容易。

定義2 若嵌套循環(huán)中內層循環(huán)的執(zhí)行次數完全或部分地依賴于外層循環(huán)能夠直接修改的變量，則稱此嵌套循環(huán)為“非正交”嵌套循環(huán)。

以下面的程序為例，第8行的while語句的局部循環(huán)執(zhí)行次數既與外層循環(huán)的控制變量i有關(第7行j取i的值)，同時還與全局變量數組a的取值有關。因此，其局部循環(huán)邊界并非一目了然。出于對安全的考慮，此類非正交多重嵌套循環(huán)在標注內循環(huán)語句的循環(huán)邊界時，往往采用局部循環(huán)上界，即所有可能情況下的局部最大循環(huán)次數。在此程序中，由于第6行while的循環(huán)上界是9，第8行while語句的局部循環(huán)上界也是9(當i=10時)。這樣一來，內層while的全局執(zhí)行次數會被記為小于等于9×9=81次。而其實際的最大全局執(zhí)行次數為9+8+7+6+5+4+3+2+1=45次。于是，采用傳統(tǒng)局部約束法計算的WCET被嚴重高估了。

要獲得更為精確的WCET估計值，可以使用全局約束法標注非正交多重嵌套循環(huán)的循環(huán)邊界。為了驗證上述分析，我們做了實驗(1)。我們從瑞典馬拉達倫大學的WCET基準程序中選擇了“select.c”和“fac.c”作為實驗對象。其中，“select.c”有 3 重嵌套，共4個非正交的循環(huán)?！癴ac.c”有一個非正交的循環(huán)嵌套遞歸。我們通過修改程序輸入的方法，為“select.c”生成8個變體，連同原程序一共9個實驗對象。為“fac.c”生成3個變體，共4個實驗對象。

圖1 采用不同約束獲得的WCET估計值與觀測值的對比(select程序集)

為了使硬件方面的不確定性降到最低，我們配置的目標處理器沒有采用分支預測和指令Cache，沒有采用亂序執(zhí)行，指令取值隊列大小為4，重排序緩沖區(qū)為16。實驗工具采用新加坡國立大學的Chronos。此時的WCET觀測值可認為是實際的WCET。實驗結果如圖1(select程序集)、表1(fac程序集)所示。

表1 采用不同約束獲得的WCET估計值與觀測值的對比(單位:Cycle)

圖1中全部9個程序，表1中全部4個程序，使用全局約束獲得的WCET估計值都比使用局部約束的低，但比觀測值要高。這說明，對于非正交多重循環(huán)嵌套，使用全局約束法獲得的WCET估計值比使用局部約束法更精確，同時也是安全的。

2 基于IPET的WCET預測二次修正法

使用全局約束法可以修正傳統(tǒng)局部約束法在估計含非正交多重嵌套循環(huán)程序的WCET時的過高估計值，從而使其更精確。盡管如此，人們總是希望獲得更為精確的WCET估計值。因此，我們針對采用了亂序執(zhí)行、Cache和分支預測結構的復雜處理器，待分析程序含有非正交多重嵌套循環(huán)或遞歸的情況，提出了WCET估計的二次修正方法。該方法的前提假設是:在對復雜處理器上運行的某些程序的WCET進行估計時，不能僅使用全局約束法替代局部約束法在標注循環(huán)邊界或遞歸深度時所起的作用。為了更好的說明本方法，我們做了以下一組實驗。

實驗(2)的實驗目的是在簡單處理器上，對比局部約束、全局約束對WCET估計值的影響。實驗對象是:fac基準程序，輸入值n=5。外層循環(huán)的循環(huán)上界為6;局部遞歸深度上界為6，全局遞歸深度上界為21。目標處理器配置同實驗(1)。試驗結果如表2所示。

從表2中不難看出，當僅使用局部約束時，WCET隨著標注的遞歸深度的增加而增加。而當加入全局約束時，局部遞歸深度d≤3不可行，因為全局遞歸上界是21，此時d*6＜21，整數線性規(guī)劃不可行(也沒意義)。而當d≥4時，WCET值不會隨著標注的遞歸深度而增加。這表明，對于程序fac而言，在目標處理器沒有采用亂序執(zhí)行、分支預測時，若全局約束正確，局部約束除了會因為設置過小而沒有意義以外，不起任何作用。即，全局約束替代了局部約束在標注循環(huán)邊界時的作用。

實驗(3)的實驗目的是在復雜處理器上，對比局部約束、全局約束對WCET估計值的影響。實驗對象與實驗(2)相同。目標處理器配置如表3所示。實驗結果如表4所示。

表2 實驗(2)WCET估計值、觀測值的對比(非亂序，fac(n=5))(單位:Cycle)

表3 實驗(3)的目標處理器配置

表4 實驗(3)WCET估計值、觀測值對比(亂序，fac(n=5))(單位:Cycle)

與實驗(2)相比，實驗(3)的結果卻反映了另外一種情況，當目標處理器采用亂序執(zhí)行、分支預測時，全局約束不能替代局部約束在標注循環(huán)邊界時的作用。從表4中容易看出，即使正確約束了遞歸的全局執(zhí)行次數為21，WCET還是會隨著標注的遞歸深度增加而增加，只不過估計值會比僅局部約束的小。類似的現象我們在“select”程序的變體(輸入為10，30)中也發(fā)現過。這表明，我們之前的假設情況是存在的，即在估計某些在復雜處理器上運行的程序的WCET時，僅使用全局約束法是不夠的。

既然有些時候必須使用局部約束，這就帶來了一個新的問題:隱藏路徑枚舉法在計算WCET時要使用整數線性規(guī)劃。而整數線性規(guī)劃要求約束表達式中的值必須是整數［11－12］。同時，局部約束法是用嵌套語句的局部循環(huán)上界表達內外循環(huán)的執(zhí)行次數關系。但實際上這種關系未必都是整數倍，于是，即便結合全局約束與局部約束，WCET估計值必然還會存在一定的高估。我們用以下的實驗(4)來說明這個問題。

實驗(4)的實驗目的是對比不同約束法獲得的WCET估計值。實驗對象是基準程序fac的4個變體。目標處理器采用表3的配置。實驗結果如表5所示。

表5 實驗(4)不同約束方法獲得的WCET估計值(單位:Cycle)

以表5中的fac011為例，“局部約束”是僅采用局部約束法(即，僅使用局部最大遞歸深度“6”)獲得的WCET估計值?！叭旨s束”是在局部約束的基礎上，添加了全局約束(即，添加了全局遞歸執(zhí)行次數“21”)獲得的WCET估計值。“一次修正”是用被嵌套語句的全局執(zhí)行次數除以外層語句的全局次數所得的商再加1作局部約束，從而修正了原來使用局部執(zhí)行次數上限作約束所產生的高估值。(即，將原來的局部最大遞歸深度由“6”修正為“┌21/(5+1)┐ =4”)，從而獲得更精確的WCET?！岸涡拚笔窃谝淮涡拚幕A上，進一步將局部遞歸深度修正為21/(5+1)=3.5的近似值，從而使WCET又精確了一些。需要說明的是，二次修正不是直接修改遞歸深度，因為整數線性規(guī)劃不允許輸入非整數。

從表5中不難看出，隨著循環(huán)邊界越來越精確，所得的WCET越來越精確，這說明循環(huán)邊界對WCET的預測有很大影響。同時，盡管全局約束能夠在一定程度上使WCET更精確，但由于前述某些情況的存在，使得全局約束不能完全替代局部約束的作用。而又由于嵌套語句的執(zhí)行次數關系未必是整數倍，所以使用全局約束獲得的WCET仍有繼續(xù)修正的空間。我們的二次修正方法正是針對這種情況提出來的，其基本流程如圖2所示。

圖2 基于IPET的WCET預測二次修正法的基本流程

我們以程序fac的兩個變體:fac02(n=10)(11，66)和fac011(n=5)(6，21)為例，進一步說明二次修正方法的原理。這兩個程序外層是一個循環(huán)，內層嵌套的是遞歸。首先，fac02的外層循環(huán)上限是11，內層遞歸的最大遞歸深度是11，內層遞歸的全局執(zhí)行次數是66。然后，計算嵌套內外層的執(zhí)行次數是否是整數倍關系。fac02的所有嵌套(實際上就1個)的內外層執(zhí)行次數(66/11=6)是整數倍，因此二次修正的隊列為空。此程序僅需將局部約束用“6”替代“11”做“一次修正”即可。

fac011的外層循環(huán)上限是6，內層遞歸的最大遞歸深度是6，內層遞歸的全局執(zhí)行次數是21。首先，fac011的嵌套非整數倍(21/6=3.5)，進入修正隊列。然后，用┌21/6┐=4和21分別設為內層遞歸的局部和全局約束，計算WCETbgn。因為此嵌套的層次n=2，所以使用┌21/6┐+1=5替代內層嵌套的局部約束，并計算WCETadd。用WCET2=(WCETbgn－WCETadd)/(5*6－4*6)計算每1次遞歸的執(zhí)行時間。最終的WCET=WCETbgn－WCET2*(4*6－21)。其中(4*6－21)是局部遞歸深度設置為4時，全局遞歸執(zhí)行次數比實際的21次多出的次數。

3 二次修正方法的有效性及安全性分析

二次修正方法的效果需要從有效性及安全性兩個方面加以分析。首先，二次修正的目的是獲得更加精確的WCET估計值。如果這個方法確實能夠獲得比傳統(tǒng)方法(局部約束和全局約束)更加精確的WCET估計值，我們則認為該方法是有效的。其次，二次修正后的結果必須是安全的，否則就失去了修正的意義。如果修正后的WCET仍然大于實際的WCET，我們則認為該方法是安全的。

為了證明二次修正法的有效性，我們可以對比實驗(4)的結果(表5所示)。從中不難看出，使用二次修正法獲得的WCET的確比使用局部約束及全局約束獲得的WCET更加精確，這說明該方法是有效的。為了驗證二次修正方法的安全性，我們又做了實驗(5)。實驗對象是fac和select程序集。目標處理器的配置與實驗(1)相同，即不用亂序執(zhí)行等復雜硬件特性，從而使硬件方面的不確定性將至最低。此時，觀測得到的WCET可認為是實際的WCET。實驗結果如表6所示。

表6 實驗(5)二次修正法獲得的WCET估計值與觀測值的對比(單位:Cycle)

從表6中可以看到，二次修正獲得的WCET全部大于實際的WCET。這說明本文提出的二次修正方法是安全的，能夠用于評估程序的執(zhí)行時間是否能夠滿足截止時間要求。

4 結 論

某些含有非正交多重循環(huán)嵌套的程序，當其在采用亂序執(zhí)行的復雜處理器上執(zhí)行時，僅使用全局約束未必能替代局部約束在估計其WCET時所起的作用。其原因可能在于源碼與編譯后的目標代碼很難一一對應起來，因此在源碼中標注的循環(huán)邊界并沒有被映射到所有相應的目標代碼上。這意味著僅使用全局約束獲得的WCET仍有繼續(xù)精確的空間。理論上可以在源碼上加注更多的全局約束以使WCET更精確，但更多的約束可能導致整數線性規(guī)劃不可解。

針對上述需要全局約束和局部約束同時起作用的情況，我們提出了二次修正方法。其中，第1次修正將用內循環(huán)的局部循環(huán)上界表示的局部約束修正為內循環(huán)全局循環(huán)上界除以其外循環(huán)全局循環(huán)上界所得的商再加1。在此基礎上，第2次修正是再將內循環(huán)的局部約束修正為實際值。盡管二次修正方法中的第2次修正沒有第1次修正的效果明顯，但從對計算精度的不懈追求角度看，畢竟使得WCET估計值更精確了一些。

本文的貢獻在于發(fā)現了上述全局約束不能替代局部約束的問題，并且針對這一問題提出了二次修正方法，能夠獲得更為精確且安全的WCET估計值。該方法的不足之處在于需要多次進行WCET的分析與計算，會比較耗時。未來的工作是進一步研究程序源碼與目標代碼之間的映射方法，提高映射精度，從而從根本上消除由于約束過多或過少造成的WCET不可求解或估計值過大的問題。

［1］Li X，Liang Y，Mitra T，et al.Chronos:A timing analyzer for embedded software［J］.Science of Computer Programming，2007，69(1):56－67.

［2］Wilhelm R，Grund D.Computation takes time，but how much［J］.Communications of the ACM，2014，57(2):94－103.

［3］呂鳴松.實時系統(tǒng)最壞情況執(zhí)行時間分析技術的研究［D］.沈陽:東北大學，2010.

［4］孔亮亮，江建慧，肖杰，等.ARM 程序執(zhí)行周期估計的基于模擬的非線性方法［J］.計算機研究與發(fā)展，2012，49(2):392－401.

［5］Kosmidis L，Quinones E，Abella J，et al.Achieving timing composability with measurement－based probabilistic timing analysis［C］//In IEEE International Symposium on Object/component/service－oriented Real－time distributed computing(ISORC).2013:1－8.

［6］張保民，吳國偉，姚琳.程序最壞執(zhí)行時間極值統(tǒng)計方法［J］.計算機工程與應用，2010，46(26):67－71.

［7］Cazorla F J，Quinones E，Vardanega T，et al.Proartis:Probabilistically analyzable real－time systems［J］.ACM Transactions on Embedded Computing Systems(TECS)，2013，12(2s):94－119.

［8］Li Y T S，Malik S.Performance analysis of embedded software using implicit path enumeration［J］.ACM SIGPLAN Notices，1995，30(11):88－98.

［9］Knoop J，Kovács L，Zwirchmayr J.An Evaluation of WCET Analysis using Symbolic Loop Bounds［J］.Proc.of WCET，2011.

［10］Blazy S，Maroneze A，Pichardie D.Formal Verification of Loop Bound Estimation for WCET Analysis［M］//Verified Software:Theories，Tools，Experiments.Springer Berlin Heidelberg，2014:281－303.

［11］徐屹.基于優(yōu)化模型的廣義最小二乘法及其應用［J］.東北電力大學學報，2013，33(6):11－14.

［12］曲朝陽，陳師，楊帆，等.基于雙層次分析的變電站數據分類方法［J］.東北電力大學學報，2014，34(2):61－65.