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.