面向软错误的故障恢复和验证技术研究

发布时间：2018-01-12 05:05

本文关键词：面向软错误的故障恢复和验证技术研究　出处：《国防科学技术大学》2013年博士论文　论文类型：学位论文

【摘要】：随着集成电路制造工艺的发展，现代微处理器的性能在大幅度提高的同时，面临软错误的威胁也越来越严重。软错误是由外部环境中的高能粒子辐照或电压扰动、地磁干扰等因素诱发的一种硬件瞬态故障现象。它不破坏电路的内部结构，但是却可以通过改变处理器状态或者存储单元值等方式影响程序的正常运行，从而对系统可靠性造成严重影响。为提高系统可靠性，，国内外纷纷开展了容错技术的研究。从实现方式来看，面向软错误的容错技术主要可以分为硬件实现的和软件实现的容错技术。与硬件实现的容错技术相比，软件实现的容错技术无需改造或重新设计硬件，具有实现成本低、开发周期短、可灵活配置等优势而备受关注。从软错误的处理过程来看，软件实现的容错技术主要包括这几个方面的研究内容：软错误的影响分析和评估、错误检测、错误恢复、容错优化配置和容错算法验证。由于目前的研究大都集中在软错误的影响分析和错误检测方面，本文主要针对错误恢复和容错算法验证展开研究。本文的主要贡献可分为以下四个方面： 1.本文提出一种基于格式化标签分析的控制流恢复技术，使得错误检测后程序状态能恢复至故障发生前的一个正确状态，确保程序继续执行且输出正确结果。该方法首先在汇编语言级上将程序代码划分为无存基本块，并为每个无存基本块分配格式化的静态标签；然后基于分配的静态标签添加控制流检测和恢复指令，其中检测指令主要负责控制流检测而恢复指令主要负责恢复由控制流错误导致的程序数据流错误；最后定义分层故障处理例程，即为每个过程单独定义一个过程错误处理例程和为整个程序定义一个全局错误处理例程。该方法首次解决了过程间的控制流错误检测和恢复问题，能检测和恢复所有的基本块间的控制流错误，并能检测和恢复绝大部分的基本块内部的控制流错误。与纯控制流检测算法相比，该方法在控制流错误检测的基础上以相对较少的性能开销实现了错误恢复。 2.本文提出一种源代码级的数据流错误容错处理机制，主要包括三个方面：(1)基于基本块的概念给出包含块的定义，该错误处理机制以包含块为基本单位对数据流错误进行检测和恢复，确保包含块内发生的数据流错误不会传播至块外。(2)提出一种基于差异转换和冗余复算的错误检测机制，其基本思想是基于一组差异转换规则，将原程序转换为功能完全一致的冗余程序，通过在特定位置插入比较检测语句来判断程序运行过程中是否发生软错误。(3)提出一种应用级检查点备份的数据流错误恢复机制，即通过求解数据流分析方程得出检查点包含的变量集合，以此为依据插入恢复代码。为自动生成容错程序，本文设计并实现一个源到源的转换工具。故障注入实验和性能开销实验结果表明：与其它源代码级数据流错误容错方法相比，该方法能以相对较少的性能开销达到较高的错误覆盖率。 3.本文根据模型检验原理，提出一种通用的针对基于标签分析的控制流检测算法的形式化验证方法。该方法首先对待验证目标——基于标签分析的控制流检测算法进行概述；在此基础上将容错程序建模为控制流状态机，并给出其语法和语义的定义；然后对控制流状态机进行进一步具体化，通过定义一个状态转换系统来描述控制流检测过程状态的转移；并基于状态转换系统和模型检验工具的对应关系，将状态转换系统转换为模型检验工具的输入程序，以进行自动验证；最后以代表性的控制流检测算法CFCSS算法和DSM算法为例，说明该方法的实用性。验证结果表明：该验证方法首次发现了DSM算法的检测盲点，以及与CFCSS算法中标签设计相关的一些检测盲点。 4.针对数据流容错算法的有效性验证，本文提出一种基于汇编语言类型系统的形式化验证方法。它的基本思想是给汇编语言加上静态类型属性，通过类型安全性来保证程序的容错属性。本文以典型的数据流恢复算法SWIFT_R为例，首先给出类型化的容错汇编语言TFAL的语法，通过将一条指令的执行建模为状态的一次转移，对TFAL的操作语义进行解释；在此基础上对TFAL的指令进行类型检查，得出了SWIFT_R算法的检测盲点；在假定排除这些检测盲点的前提下，首先证明了TFAL系统的类型安全性——前进和保持属性。然后在此基础上定义状态的相似关系，进一步证明了SWIFT_R算法的容错属性，即原程序在无错环境下运行的输出结果与容错程序在错误环境下运行的输出结果一致，且状态转移过程相似。
[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 .

【学位授予单位】：国防科学技术大学
【学位级别】：博士
【学位授予年份】：2013
【分类号】：TP302.8

【参考文献】