一種面向瞬時故障的容錯技術的形式化方法

朱丹丹，劉久富，陳 柯，梁娟娟

（南航航空航天大學 自動化學院，江蘇 南京 210016）

當高能粒子撞擊到晶體管或處理器的線路，引起狀態的改變，即是瞬時故障的發生。這些粒子不會永久損壞硬件，但可能改變存儲值和狀態標志。隨著技術的發展，處理器制造的趨勢將導致瞬時故障率的增高。頻率更高，晶體管密度更大，工作電壓減小以及特征尺寸的減小，都將會導致處理器更容易受到瞬時故障的影響。瞬時故障可能會導致許多重大問題，例如，2003年美國的Los Alamos，ASCQ超級計算機經常因為軟件錯誤而崩潰。

所有的解決方法都是基于冗余技術，主要分為2種：一種基于硬件的解決方案，如看門狗計數器、看門狗協處理器和Infrastructure IP （I-IP）；一種基于軟件的解決方案，如ECCA算法、RSCF算法和CFCSS算法[1]和SWIFT算法[2]等。有些研究者提出了混合解決方案，使用冗余的硬件和軟件，發揮各自的優點，如CRAFT算法。但是，使用這些方法生成正確的容錯代碼十分困難，而且幾乎沒有關于證明這些技術的正確性的研究。攜帶證明的代碼PCC[3]是驗證不可信的低級代碼的一種技術。在攜帶證明的代碼系統中，編譯器負責產生：低級代碼和安全性證明。若要運行程序代碼，運行程序的主機只需驗證其證明是否正確，以確保代碼的運行不會出乎意料。一般來說，安全性證明要包括保證內存安全和類型安全。類型化匯編語言（TAL）是一種標準的程序安全性證明的方式[4]。TAL是基于RISC風格的類型化匯編語言，并可以作為編譯器的目標語言，而且支持一些代碼優化算法。TAL類型系統的可靠性被嚴格證明，這說明了任何良類型 （welltyped）的程序代碼都是類型安全的。

1 機器模型

機器的硬件模型是基于一種精簡RISC體系架構的，具有支持控制流錯誤檢測和與內存映射輸出設備安全交互的特點。軟件采用兩獨立的計算線程，分別為綠色（G）計算和藍色（B）計算，綠色計算起主導作用。在寫數據到內存映射輸出設備之前，要檢查兩份計算的結果是否相等。如果結果不相等，機器將發出檢測到故障的信號。圖1總結了機器狀態語法。

圖1 指令語法和機器狀態Fig.1 Syntax of instructions and machine states

匯編程序的執行規定使用小步操作語義，它是機器狀態（∑）到其他機器狀態的映射。這些機器狀態∑由寄存器組R、代碼堆C、存儲隊列Q、數據堆M和指令ir組成。有兩個程序計數器寄存器（pcG和pcB），沒有故障時這兩個寄存器的值相同。還有一個的特殊綠色目的寄存器gd。M中的地址0不是一個有效的代碼地址。為了實現容錯，在內存和處理器之間有一個特殊的存儲隊列Q，用于檢測故障。存儲隊列Q是一個地址-值（address-value）對隊列。用上劃線符號來表示對象序列。

一個抽象的機器狀態（∑）也可能具有錯誤的形式fault，這表明硬件發現了一個瞬時故障；或者具有普通狀態（R，C，M，Q，ir）形式。為了便于某些定理的證明，根據所屬計算，我們為每寄存器值附上相應的顏色標簽（綠色或藍色）。但這些標簽對運行時程序的行為沒有影響。

1.1 故障模型

1.2 指令操作語義

圖2 存儲指令操作規則Fig.2 Operational rules for store instructions

假設機器執行綠色存儲指令stGrd，rs，執行前的程序狀態為（R，C，M，Q，stGrd，rs），執行后兩程序計數器加 1，寄存器文件R中其他寄存器不變；代碼堆C和數據堆M不變；地址-值對（Rval（rd），Rvol（rs））放在隊列 Q 的隊尾（規則 stG-queue）。藍色存儲指令stBrd，rs有些不同， 它重新得到隊頭的 （n，n′）地址-值對，并檢查它和（Rval（rd），Rvol（rs））相等，然后將其存入數據堆（規則stB-mem）。如果兩個地址-值對不相等，硬件發出故障信號（規則stB-mem-fail）。存儲指令要成對出現，而且綠色存儲一定先于藍色存儲，這樣才能達到容錯的效果。未給出指令操作語義與此類似。

2 類型系統

2.1 類型定義

TAL類型系統的首要目標是確保在瞬時故障出現時程序是良類型程序的。類型系統的語法如圖3所示。

圖3 TAL類型語法Fig.3 TAL type syntax

TAL類型系統是以匯編語言類型理論和霍爾邏輯（Hoare Logic）基礎的，由3部分組成：靜態表達式、類型和環境。靜態表達式分為整型（類別κint）或和存儲型（類別κmem）。整型表達式包含變量，常量，簡單的算術運算，和存儲空間中的數值（sel Em，En表示位于Em中的地址En處的整數）。存儲型表達式包含變量，空存儲（emp），和存儲更新（upd Em，En1，En2表示更新的存儲空間Em，其中的地址En1存儲數值En2）。表達式環境Δ是變量到類別的映射，包含在編譯時用于靜態表達式各種自由變量。代替S表示靜態表達式Ε代替靜態表達式變量x。類型包括程序改變標簽Ζ、基本類型b（數值類型）、寄存器類型t、寄存器文件類型Γ和結果類型RT。環境包括堆定型環境Ψ和靜態環境Θ。

2.2 定型規則

TAL類型系統定型規則包括：數值定型規則、類型化斷言之間的子定型規則、指令定型規則和機器狀態定型規則。圖4只給出了存儲指令定型規則，其他規則類似。

圖4 存儲指令定型規則Fig.4 Typing rules for store instructions

3 類型安全和容錯性

3.1 類型安全

TALFT類型系統的可靠性可以使用 “類型系統可靠性＝前進性+保持性”的方法來證明。前進性表明良類型狀態可以過渡。特別地，在空程序改變標簽下，程序執行一步，良類型機器狀態可過渡到另一機器狀態。在顏色程序改變標簽下，程序執行一步，良類型機器狀態可以過渡到另一機器狀態或故障狀態。

定理1（前進性）

根據保持性，如果在程序改變標簽Ζ下，如果機器狀態是良類型的，程序無誤地執行一步，過渡到另一機器狀態，那么結果機器狀態在Ζ下是良類型的。此外，如果在空程序改變標簽下，機器狀態是良類型的，程序有誤執行一步，那么存在顏色c，使得結果機器狀態在c下是良類型的。

定理2（保持性）

前進性和保持性定義了一般的類型安全的概念。此外，從前進性定理和保持定理，可以推出下面的重要推論：在良類型程序執行過程中，如果沒有故障發生，那么硬件就不會發出故障信號。

推論1（非誤報性）

3.2 容錯性

當程序的所有有故障執行相似于程序的無故障執行時，程序就是具有容錯性的。更確切地說，有故障執行的輸出序列與無故障執行的輸出序列一致，或硬件檢測出故障。定義相似關系都和程序改變標簽Ζ相關。直觀地說，如果Ζ是空的，相應的對象必須是一致的。如果Ζ是一個顏色c，相應對象必須和具有顏色c的模值一致。在后一種情況中，具有顏色c的數值可能被損壞。

利用相似關系，我們可以準確地描述并證明良類型程序的容錯性定理。假設在空程序改變標簽下，機器狀態是Σ良類型的，程序無故障執行n步，程序狀態從Σ過渡到Σ′，輸出地址-值對s序列。如果在程序執行中的某一步發生故障，然后程序執行了n+1步驟，或在這段時間終止于故障狀態。如果程序有故障執行需要n+1步，并達到無故障狀態，那么Σ′相擬于，而且輸出的地址-值對序列與原來的一致；如果程序有故障執行達到故障狀態，那么輸出的地址-值對將是無故障輸出對的前面部分。

定理4（容錯性）

4 實驗結果

本文介紹的容錯方法對代碼進了全部復制，空間開銷增加了一倍，但時間開銷并沒有成倍的增加，因為好的指令調度和高效配置的資源可以減少執行時間。所采用的實驗平臺為主頻2.3 GHz的Intel賽揚處理器、1GB內存、內核版本為2.6的Linux的操作系統。我們對VELOCITY編譯器[6]進行相應修改以增加容錯TAL的可靠性。實驗結果如圖5所示，以沒有故障檢測能力的匯編程序為基線，無代碼執行順序約束版本的容錯TAL執行時間約增加了30%，有代碼執行順序約束限制版本的執行時間增加34%。

5 結束語

文中介紹了一種面向瞬時故障的軟硬結合的容錯技術，即容錯類型化匯編語言，以及對它的形式化方法。兩個主要的形式結果表明，影響良類型程序的瞬時故障，都能被檢測出；當沒有故障發生時，系統不會報告檢測到故障。在容錯程序的時間開銷上，盡管良類型程序本質上復制所有的計算，但仿真結果表明時間開銷為原來的1.34倍，對于實際的應用是可以接受的。本文介紹的容錯方法中還有一些需要改進的地方，如故障模型不全面，所涉及的指令還不完整等。這些也都是需要進一步做的研究工作。

圖5 時間開銷比較Fig.5 Time overhead comparison

[1]Oh N，Shirvani P，McCluskey E，et al.Control flowchecking by software signatures[J].IEEE Trans on Reliability，2002，51（2）:111-122.

[2]Reis G A，Chang J，Vachharajani N，et al.SWIFT:Software implemented fault tolerance[M].In Proceedings of the 3rd InternationalSymposiumonCodeGenerationandOptimization，2005.

[3]Necula G.Proof-carrying code[M].In Twenty-Fourth ACM Symposium on Principles of Programming Languages，1997：106119.

[4]Morrisett G，Walker D，Crary K，et al.From system to typed assembly language[M].In Twenty-Fifth ACM Symposium on Principles of ProgrammingLanguages，1998：85-97.

[5]McM， row D， Lotshaw William T， et al.Single-event upsetin flip-chip SRAM induced by through-wafer，twophotonabsorption[J].IEEE Trans on Nuclear Science，2005，52（6）:2421-2425.

[6]Triantafyllis S，BridgesM J，Raman E，et al.A frameworkfor unrestricted whole-program optimization [C]//In ACM SIGPLAN 2006 Conferenceon ProgrammingLanguage Design and Implementation，2006：61-71.