Formal Verification of Programs on Synchronous Parallel Machines

点击翻译按钮获取中文摘要

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.