Formal Verification of Programs on Synchronous Parallel Machines

同步机是一类重要的高性能计算机。这种类型的机器包括线性和收缩阵列，如WARP机器，二维阵列，如大规模并行计算机，以及具有更复杂互连的机器，如连接机。这类机器的重要性在很大程度上归因于体系结构的可伸缩性。同步机器可以包含数十万个处理器。然而，这种可扩展性意味着在机器上运行的整个程序的复杂性相应增加，因此，在正式或非正式的情况下，对该程序的正确性进行推理的难度也相应增加。本研究的目的是开发在同步并行机器上运行的程序的正式验证方法-特别是由大量处理器组成的机器，这些处理器执行相同程序的副本并使用消息传递进行通信。基本方法是证明关于程序的单个副本的断言，并从这个证明中推断整个程序集合的属性。我们的目标是在这种方法的基础上建立一个完整的形式化理论。与所有用于程序推理的正式方法一样，这些概念、定理和一般方法可以期望对此类机器的软件开发有重大的好处——即使该软件是非正式开发的。软件设计师当然必须对软件的正确性进行推理，即使这种推理是非正式的。形式化方法可以为如何执行推理提供指导。

Synchronous machines are an important class of high performance computers. Machines of this type include linear and systolic arrays such as the WARP machine, two dimensional arrays such as the Massively Parallel Computer, and machines with more complex interconnections such as the Connection Machine. The importance of this class of machines is due in large measure to the scalability of the architecture. Synchronous machines can be built containing hundreds of thousands of processors. This scalability, however, implies a corresponding increase in the complexity of the overall program running on the machine and, hence, in the difficulty of reasoning, either formally or informally, about the correctness of that program. The objective of this research is to develop methods for the formal verification of programs running on synchronous parallel machines-- specifically machines consisting of a large number of processors that execute copies of the same program and communicate using message passing. The basic approach is to prove assertions about a single copy of the program and, from this proof, infer properties of the entire assembly of programs. The goal is to develop a complete formal theory based on this approach. As with all formal methods for reasoning about programs, the concepts, theorems, and general approach can be expected to have a significant benefit on software development for such machines--even when that software is developed informally. The software designer must certainly reason about the correctness of the software even if that reasoning is done informally. Formal methods can provide a guide to how to perform that reasoning.