Postdoc: Refinement and Modularity in Parallel Programs

这项工作是一项为期两年的工作，旨在开发和应用基于形式方法的技术来编写可靠的程序，以在高性能并行计算机上解决科学问题。以前的工作已经证明了一种并行应用开发方法的实用价值，该方法基于(1)形式指定的编程模型和基于语义保持转换的开发方法，以及(2)抽象(“原型”)，其捕获具有相似结构的程序类的共性并封装并行代码的细节。这项工作的一个重要方面是，虽然它为并行程序的开发和推理提供了一个完善的理论框架，但它不需要应用程序开发人员开发形式证明；一旦声明和证明了转换规则，它在程序开发中的应用就可以非正式地进行。PI以前的工作为解决并行程序中的模块化和程序组合问题提供了一个简单而灵活的理论框架。在这两个方面工作的基础上，提出了一个关于并行程序模块化和组合推理的理论框架。PI将使用这个框架来开发技术，帮助应用程序开发人员编写可靠的并行程序，并将通过将这些技术应用于计算科学和工程中选定的现实世界应用程序来验证这些技术的有用性。

This work is a two-year effort to develop and apply techniques based on formal methods to the writing of reliable programs for solving scientific problems on high-performance parallel computers. Previous work has demonstrated the practical value of an approach to parallel application development based on (1) a formally-specified programming model and a development methodology based on semantics-preserving transformations, and (2) abstractions ("archetypes") that capture the commonality of classes of programs with similar structure and encapsulate the details of the parallel code. An important aspect of this work is that, while it provides a sound theoretical framework for developing and reasoning about parallel programs, it need not require application developers to develop formal proofs; once a transformation rule is stated and proved, its application during program development can be carried out informally. Previous work by the PI has provided a simple and flexible theoretical framework for addressing questions of modularity and program composition in parallel programs. Building on these two areas of work, a theoretical framework is proposed for reasoning about modularity and composition in parallel programs. The PI will use this framework to develop techniques that will assist application developers in writing reliable parallel programs, and will validate the usefulness of these techniques by applying them to selected real-world applications in computational science and engineering.