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.