Theory of Program Checking and Fault-Tolerant Software

程序检查是一种新的软件容错方法。对于计算函数的程序，检查器测试程序的输出对于特定输入是否正确。即使当程序出错时，检查器也会使用程序本身来执行测试，方法是将程序应用于与原始输入相关的几个输入。检查器提供对执行程序的特定输入的正确性的概率保证，而正式的程序验证在执行之前建立对所有输入的正确性。在这个项目中，将传统的容错技术与程序检查相结合，产生了对实际规模的程序有效的新型程序检查器。特别是，程序检查与认证跟踪和基于算法的容错相结合，这是一种用于并发错误检测的技术。此外，程序检查被应用于操作系统算法，以确保诸如互斥、死锁避免和并发事务的可串行化等谓词的真实性。

Program checking is a new approach to software fault-tolerance. For a program that computes a function, a checker tests whether the program's output is correct for a specific input. Even when the program makes mistakes, the checker uses the program itself to perform the test by applying the program to several inputs related to the original one. The checker provides a probabilistic guarantee of correctness on a particular input on which the program is executed, whereas formal program verification establishes correctness on all inputs prior to execution. In this project, traditional fault-tolerance techniques are combined with program checking to produce new kinds of program checkers that are effective for programs of practical size. In particular, program checking is combined with certification trails and with algorithm-based fault-tolerance, a technique for concurrent error detection. Further, program checking is applied to operating system algorithms that ensure the truth of predicates such as mutual exclusion, deadlock avoidance, and serializability of concurrent transactions.