局部約束與全局約束對WCET分析的影響淺析

孟凡奇

摘 要：循環語句的執行次數對程序的執行時間是有影響的，通常循環次數越多，程序執行時間越長。因此，在最差情況執行時間分析中通常需要指明程序循環語句的執行次數上限。本文簡要分析使用局部約束與全局約束標注循環上限對最差情況執行時間分析結果的影響。

關鍵詞：最差情況執行時間；循環上界；局部約束；全局約束

眾所周知，循環次數對執行時間是有影響的，通常循環次數越多，程序執行時間越長。因此，靜態最差情況執行時間（Worst-case Execution Time，WCET）分析通常都需要知道（自動分析或人工標注）循環上界，以便使WCET估計值更精確[1]。本文將探尋使用“局部”或“全局”約束法標注循環上界會對程序的WCET分析有何影響，據此，我們可以決定何種情況下使用何種方法。

1 局部約束與全局約束

“局部”循環邊界是指循環語句執行1次，其循環體可能的執行次數范圍。“全局”循環邊界是指從程序開始運行到結束，循環語句的循環體可能的全部執行次數范圍。

以下面的代碼為例，第1行for語句的“局部”和“全局”循環邊界都是[0，5]。第2行for語句的局部循環邊界是[0，5]，全局循環邊界是[0，25]。

需要說明的是，由于WCET計算的是最差情況，因此，通常僅需要提供循環上界。我們可以使用“局部”約束法或“全局”約束法為計算WCET的整數線性規劃提供所需的循環上界的表達式。局部約束法使用局部循環上界，分析工具會將局部循環上界轉換成內外層語句執行次數的整數倍數關系。以上面的代碼為例，如果第2個for循環的循環邊界使用局部約束法進行標注，則會生成表達式“line2-5line1=0”，即第1行每執行1次，第2行執行5次。而全局約束使用全局循環邊界，若第2個for使用全局約束，則會生成表達式“line2=25”。

多數情況下，由于局部循環邊界易于獲取，所以局部約束法是較為常見的標注方式。然而，情況并非如此簡單。對于上下文敏感的循環，尤其是非正交多重嵌套循環，獲取內循環的局部循環邊界也并不容易。

2 全局約束與非正交循環

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

以下面的程序片段為例，第10行的while語句的局部循環執行次數既與外層循環的控制變量i有關，同時還與全局變量數組a有關。出于對安全的考慮，此類非正交多重嵌套循環在標注內循環的循環邊界時，往往采用局部循環上界，即所有可能情況下的局部最大循環次數。例如，第10行while語句的局部循環上界是“9”。這樣一來，內層while的全局執行次數會被記為小于等于9×9=81次。而其實際的最大全局執行次數為9+8+7+6+5+4+3+2+1=45次。于是，WCET估計值被嚴重高估了。

要獲得更精確的WCET估計值，可以使用全局約束法標注非正交多重嵌套循環的循環邊界。從表1中可以看出，使用全局約束可以獲得比使用局部約束更精確的WCET估計值。程序fac.c來自于M?lardalen大學的WCET基準程序集。

可以采用“插樁→運行”的動態方法獲取循環的全局執行次數。首先，生成待處理程序的抽象語法樹；然后，在抽象語法樹中尋找循環語句節點；接著，在每一個循環語句節點的第一個子節點之前插裝探針，用于輸出該循環語句在原源程序中的行號；然后，將插樁后的抽象語法樹還原為源程序；最后，這個已經插樁了的源程序獲得各循環語句的執行次數。此方法的優點是易于實現、效率較高。但缺點是必須提供最差輸入，否則獲得的循環執行次數未必是最差情況下的全局循環上界。

3 結束語

局部約束適用于循環上界識別較為容易的正交循環。全局約束適用于非正交循環的內循環語句，可以獲得相較于局部約束更為精確的WCET估計值。因此，當程序中的嵌套循環是正交的，建議使用局部約束標注循環上界，否則建議使用全局約束。

[參考文獻]

[1]呂鳴松，關楠，王義.面向WCET估計的Cache分析研究綜述[J].軟件學報，2014，25（2）：179-199.

[2]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.

[3]呂鳴松.實時系統最壞情況執行時間分析技術的研究[D].東北大學， 2010.