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

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

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

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

1 機器模型

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

圖1 指令語法和機器狀態(tài)Fig.1 Syntax of instructions and machine states

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

一個抽象的機器狀態(tài)（∑）也可能具有錯誤的形式fault，這表明硬件發(fā)現(xiàn)了一個瞬時故障；或者具有普通狀態(tài)（R，C，M，Q，ir）形式。為了便于某些定理的證明，根據(jù)所屬計算，我們?yōu)槊考拇嫫髦蹈缴舷鄳念伾珮撕灒ňG色或藍色）。但這些標簽對運行時程序的行為沒有影響。

1.1 故障模型

1.2 指令操作語義

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

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

2 類型系統(tǒng)

2.1 類型定義

TAL類型系統(tǒng)的首要目標是確保在瞬時故障出現(xiàn)時程序是良類型程序的。類型系統(tǒng)的語法如圖3所示。

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

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

2.2 定型規(guī)則

TAL類型系統(tǒng)定型規(guī)則包括：數(shù)值定型規(guī)則、類型化斷言之間的子定型規(guī)則、指令定型規(guī)則和機器狀態(tài)定型規(guī)則。圖4只給出了存儲指令定型規(guī)則，其他規(guī)則類似。

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

3 類型安全和容錯性

3.1 類型安全

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

定理1（前進性）

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

定理2（保持性）

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

推論1（非誤報性）

3.2 容錯性

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

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

定理4（容錯性）

4 實驗結果

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

5 結束語

文中介紹了一種面向瞬時故障的軟硬結合的容錯技術，即容錯類型化匯編語言，以及對它的形式化方法。兩個主要的形式結果表明，影響良類型程序的瞬時故障，都能被檢測出；當沒有故障發(fā)生時，系統(tǒng)不會報告檢測到故障。在容錯程序的時間開銷上，盡管良類型程序本質上復制所有的計算，但仿真結果表明時間開銷為原來的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.