Formal Verification of Programs on Synchronous Parallel Machines

同步并行机上程序的形式化验证

• 批准号: 9123200
• 负责人: Philip Lewis
• 金额: $ 5.71万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-06-01 至 1995-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9123200&HistoricalAwards=false
• 关键词: Formal; Verification; Programs; Synchronous; Parallel

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.

同步电机是一类重要的高性能电机 电脑 这种类型的机器包括线性阵列和脉动阵列 例如WARP机器，二维阵列，例如Massively 并行计算机和具有更复杂互连的机器 比如连接机器。 这一类的重要性 机器在很大程度上是由于可扩展性的 架构 同步机可以建造包含数百个 成千上万的处理器。 然而，这种可伸缩性意味着 整个程序的复杂性相应增加 在机器上运行，因此，在推理的困难中， 无论是正式的还是非正式的，关于这个程序的正确性。 本研究的目的是开发方法， 验证在同步并行机上运行的程序 特别是由大量处理器组成的机器， 执行相同程序的副本并使用消息进行通信 通过。 基本的方法是证明关于一个 程序的副本，并从这个证明中推断程序的属性。 整个程序集。 我们的目标是开发一个完整的 基于这种方法的形式理论。 与所有用于程序推理的形式化方法一样， 定理，一般的方法可以预期有一个显着的 为这些机器的软件开发带来好处-即使 软件是非正式开发的。 软件设计师必须 当然，我也会考虑软件的正确性， 推理是非正式的。 形式化方法可以提供一个指导， 如何进行推理。