發(fā)布時間：2018-01-12 05:05

  本文關(guān)鍵詞：面向軟錯誤的故障恢復(fù)和驗(yàn)證技術(shù)研究　出處：《國防科學(xué)技術(shù)大學(xué)》2013年博士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 軟錯誤 軟件容錯 錯誤恢復(fù) 應(yīng)用級檢查點(diǎn) 容錯驗(yàn)證 模型檢驗(yàn) 類型化匯編

【摘要】：隨著集成電路制造工藝的發(fā)展，現(xiàn)代微處理器的性能在大幅度提高的同時，面臨軟錯誤的威脅也越來越嚴(yán)重。軟錯誤是由外部環(huán)境中的高能粒子輻照或電壓擾動、地磁干擾等因素誘發(fā)的一種硬件瞬態(tài)故障現(xiàn)象。它不破壞電路的內(nèi)部結(jié)構(gòu)，但是卻可以通過改變處理器狀態(tài)或者存儲單元值等方式影響程序的正常運(yùn)行，從而對系統(tǒng)可靠性造成嚴(yán)重影響。 為提高系統(tǒng)可靠性，，國內(nèi)外紛紛開展了容錯技術(shù)的研究。從實(shí)現(xiàn)方式來看，面向軟錯誤的容錯技術(shù)主要可以分為硬件實(shí)現(xiàn)的和軟件實(shí)現(xiàn)的容錯技術(shù)。與硬件實(shí)現(xiàn)的容錯技術(shù)相比，軟件實(shí)現(xiàn)的容錯技術(shù)無需改造或重新設(shè)計(jì)硬件，具有實(shí)現(xiàn)成本低、開發(fā)周期短、可靈活配置等優(yōu)勢而備受關(guān)注。從軟錯誤的處理過程來看，軟件實(shí)現(xiàn)的容錯技術(shù)主要包括這幾個方面的研究內(nèi)容：軟錯誤的影響分析和評估、錯誤檢測、錯誤恢復(fù)、容錯優(yōu)化配置和容錯算法驗(yàn)證。由于目前的研究大都集中在軟錯誤的影響分析和錯誤檢測方面，本文主要針對錯誤恢復(fù)和容錯算法驗(yàn)證展開研究。本文的主要貢獻(xiàn)可分為以下四個方面： 1.本文提出一種基于格式化標(biāo)簽分析的控制流恢復(fù)技術(shù)，使得錯誤檢測后程序狀態(tài)能恢復(fù)至故障發(fā)生前的一個正確狀態(tài)，確保程序繼續(xù)執(zhí)行且輸出正確結(jié)果。該方法首先在匯編語言級上將程序代碼劃分為無存基本塊，并為每個無存基本塊分配格式化的靜態(tài)標(biāo)簽；然后基于分配的靜態(tài)標(biāo)簽添加控制流檢測和恢復(fù)指令，其中檢測指令主要負(fù)責(zé)控制流檢測而恢復(fù)指令主要負(fù)責(zé)恢復(fù)由控制流錯誤導(dǎo)致的程序數(shù)據(jù)流錯誤；最后定義分層故障處理例程，即為每個過程單獨(dú)定義一個過程錯誤處理例程和為整個程序定義一個全局錯誤處理例程。該方法首次解決了過程間的控制流錯誤檢測和恢復(fù)問題，能檢測和恢復(fù)所有的基本塊間的控制流錯誤，并能檢測和恢復(fù)絕大部分的基本塊內(nèi)部的控制流錯誤。與純控制流檢測算法相比，該方法在控制流錯誤檢測的基礎(chǔ)上以相對較少的性能開銷實(shí)現(xiàn)了錯誤恢復(fù)。 2.本文提出一種源代碼級的數(shù)據(jù)流錯誤容錯處理機(jī)制，主要包括三個方面：(1)基于基本塊的概念給出包含塊的定義，該錯誤處理機(jī)制以包含塊為基本單位對數(shù)據(jù)流錯誤進(jìn)行檢測和恢復(fù)，確保包含塊內(nèi)發(fā)生的數(shù)據(jù)流錯誤不會傳播至塊外。(2)提出一種基于差異轉(zhuǎn)換和冗余復(fù)算的錯誤檢測機(jī)制，其基本思想是基于一組差異轉(zhuǎn)換規(guī)則，將原程序轉(zhuǎn)換為功能完全一致的冗余程序，通過在特定位置插入比較檢測語句來判斷程序運(yùn)行過程中是否發(fā)生軟錯誤。(3)提出一種應(yīng)用級檢查點(diǎn)備份的數(shù)據(jù)流錯誤恢復(fù)機(jī)制，即通過求解數(shù)據(jù)流分析方程得出檢查點(diǎn)包含的變量集合，以此為依據(jù)插入恢復(fù)代碼。為自動生成容錯程序，本文設(shè)計(jì)并實(shí)現(xiàn)一個源到源的轉(zhuǎn)換工具。故障注入實(shí)驗(yàn)和性能開銷實(shí)驗(yàn)結(jié)果表明：與其它源代碼級數(shù)據(jù)流錯誤容錯方法相比，該方法能以相對較少的性能開銷達(dá)到較高的錯誤覆蓋率。 3.本文根據(jù)模型檢驗(yàn)原理，提出一種通用的針對基于標(biāo)簽分析的控制流檢測算法的形式化驗(yàn)證方法。該方法首先對待驗(yàn)證目標(biāo)——基于標(biāo)簽分析的控制流檢測算法進(jìn)行概述；在此基礎(chǔ)上將容錯程序建模為控制流狀態(tài)機(jī)，并給出其語法和語義的定義；然后對控制流狀態(tài)機(jī)進(jìn)行進(jìn)一步具體化，通過定義一個狀態(tài)轉(zhuǎn)換系統(tǒng)來描述控制流檢測過程狀態(tài)的轉(zhuǎn)移；并基于狀態(tài)轉(zhuǎn)換系統(tǒng)和模型檢驗(yàn)工具的對應(yīng)關(guān)系，將狀態(tài)轉(zhuǎn)換系統(tǒng)轉(zhuǎn)換為模型檢驗(yàn)工具的輸入程序，以進(jìn)行自動驗(yàn)證；最后以代表性的控制流檢測算法CFCSS算法和DSM算法為例，說明該方法的實(shí)用性。驗(yàn)證結(jié)果表明：該驗(yàn)證方法首次發(fā)現(xiàn)了DSM算法的檢測盲點(diǎn)，以及與CFCSS算法中標(biāo)簽設(shè)計(jì)相關(guān)的一些檢測盲點(diǎn)。 4.針對數(shù)據(jù)流容錯算法的有效性驗(yàn)證，本文提出一種基于匯編語言類型系統(tǒng)的形式化驗(yàn)證方法。它的基本思想是給匯編語言加上靜態(tài)類型屬性，通過類型安全性來保證程序的容錯屬性。本文以典型的數(shù)據(jù)流恢復(fù)算法SWIFT_R為例，首先給出類型化的容錯匯編語言TFAL的語法，通過將一條指令的執(zhí)行建模為狀態(tài)的一次轉(zhuǎn)移，對TFAL的操作語義進(jìn)行解釋；在此基礎(chǔ)上對TFAL的指令進(jìn)行類型檢查，得出了SWIFT_R算法的檢測盲點(diǎn)；在假定排除這些檢測盲點(diǎn)的前提下，首先證明了TFAL系統(tǒng)的類型安全性——前進(jìn)和保持屬性。然后在此基礎(chǔ)上定義狀態(tài)的相似關(guān)系，進(jìn)一步證明了SWIFT_R算法的容錯屬性，即原程序在無錯環(huán)境下運(yùn)行的輸出結(jié)果與容錯程序在錯誤環(huán)境下運(yùn)行的輸出結(jié)果一致，且狀態(tài)轉(zhuǎn)移過程相似。
[Abstract]:With the development of integrated circuit manufacturing technology , the performance of modern microprocessor is greatly improved , and the threat of soft error is more and more serious . Soft error is a kind of hardware transient fault caused by high - energy particle irradiation or voltage perturbation and geomagnetic disturbance in the external environment . It does not destroy the internal structure of the circuit , but can influence the normal operation of the program by changing the state of the processor or the value of the storage unit , so that the reliability of the system is seriously affected . In order to improve the reliability of the system , the fault - tolerant technology has been studied at home and abroad . From the realization mode , the fault - tolerant technology facing the soft error can be divided into hardware implementation and software - implemented fault - tolerant technology . The fault - tolerant technique realized by software mainly includes the following aspects : impact analysis and evaluation of soft error , error detection , error recovery , fault - tolerant optimization configuration and fault - tolerant algorithm verification . The invention provides a control flow recovery technique based on a format label analysis , which enables the program state after the error detection to be restored to a correct state before the fault occurs , ensures that the program continues to execute and outputs the correct result . This paper presents a source code - level error - tolerant processing mechanism of data stream error , which mainly includes three aspects : ( 1 ) the definition of the inclusion block is given based on the concept of basic block . 3 . Based on the principle of model test , this paper presents a universal formal verification method for control flow detection algorithm based on label analysis . The method is firstly used to model the control flow detection algorithm based on label analysis . Then , the control flow state machine is modeled as the control flow state machine , and its syntax and semantics are defined . Finally , based on the corresponding relationship between the state transition system and the model inspection tool , the practicability of the method is explained . Finally , the method is used to detect the blind spot of the DSM algorithm and some detection blind spots related to the label design in the CFCSS algorithm . 4 . To verify the validity of data flow fault - tolerant algorithm , this paper presents a formal verification method based on assembler language type system . The basic idea is to add static type attribute to assembly language , and to guarantee the fault - tolerant property of the program by type security .

【學(xué)位授予單位】：國防科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2013
【分類號】：TP302.8

【參考文獻(xiàn)】

相關(guān)期刊論文 前8條

1 孫峻朝,王建瑩,楊孝宗;容錯機(jī)制測評中的故障注入模型及應(yīng)用算法[J];計(jì)算機(jī)研究與發(fā)展;1999年11期

2 徐建軍;譚慶平;李建立;李劍明;;一種基于格式化標(biāo)簽的可擴(kuò)展控制流檢測方法[J];計(jì)算機(jī)研究與發(fā)展;2011年04期

3 富弘毅;楊學(xué)軍;;大規(guī)模并行計(jì)算機(jī)系統(tǒng)硬件故障容錯技術(shù)綜述[J];計(jì)算機(jī)工程與科學(xué);2010年10期

4 李愛國;洪炳昒;王司;;基于錯誤傳播分析的軟件脆弱點(diǎn)識別方法研究[J];計(jì)算機(jī)學(xué)報(bào);2007年11期

5 郭亮,唐稚松;基于XYZ/E描述和驗(yàn)證容錯系統(tǒng)[J];軟件學(xué)報(bào);2002年05期

6 楊學(xué)軍;高瓏;;錯誤流模型:硬件故障的軟件傳播建模與分析[J];軟件學(xué)報(bào);2007年04期

7 彭俊杰;黃慶成;洪炳熔;李瑞;袁成軍;;一種用于星載系統(tǒng)可靠性評測的軟件故障注入工具[J];宇航學(xué)報(bào);2005年06期

8 李愛國;洪炳熔;王司;;一種軟件實(shí)現(xiàn)的程序控制流錯誤檢測方法[J];宇航學(xué)報(bào);2006年06期

相關(guān)博士學(xué)位論文 前1條

1 徐建軍;面向寄存器軟錯誤的容錯編譯技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2010年

本文編號：1412786