一种面向瞬时故障的容错技术的形式化方法

朱丹丹，刘久富，陈 柯，梁娟娟

（南航航空航天大学 自动化学院，江苏 南京 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.