CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis

对高性能的追求推动了并行科学计算软件的设计。超过60%的高性能计算(HPC)社区使用MPI库编写程序；为了提高性能，众所周知，他们需要执行许多手动优化。即使是从高级描述生成MPI的组，由于其卓越的可移植性，最终似乎也会生成MPI代码。然而，由于性能不匹配，手动调整是不可避免的。这一点，再加上MPI标准的广泛性和不断发展的本质，以及并发编程固有的复杂性，带来了代价高昂的错误。正规方法正在爆炸性地增长，正是为了帮助消除这些类型的错误。他们已经在不同的领域找到了应用，从正式验证优化编译器转换，正式调试设备驱动程序代码，到巩固工业标准。该项目将研究和使用一些补充的形式化方法来进行HPC软件设计：为MPI建立正式的标准，以便设计者得到适当的教育；利用这些标准并编写全面的MPI平台测试；从MPI程序中提取有限状态模型并自动分析它们是否存在死锁和竞争条件；以及将使用可在运行时检查的正确性断言来检测基于MPI的程序。该项目将通过开发利用通信库的语义属性的算法，在形式化方法方面推进最先进的技术。它将通过鼓励使用正式断言，并鼓励使用正式分析代替暴力执行，帮助推动并行科学编程的最新水平。

The quest for high performance drives parallel scientific computing software design. Well over 60% of the high-performance computing (HPC) community writes programs using the MPI library; to gain performance, they are known to perform many manual optimizations. Even groups that generate MPI from high level descriptions ultimately seem to generate MPI code, due to its eminent portability. However, since performance does not port, manual tweaks are inevitable. This, together with the vastness and evolving nature of the MPI standard, and the innate complexity of concurrent programming introduces costly bugs.Formal methods are enjoying an explosive growth precisely to help eliminate these kinds of bugs. Already they find applications in diverse areas ranging from formally verifying optimizing compiler transformations, formally debugging device driver codes, and solidifying industrial standards. The project will investigate and employ a number of complementary formal approaches to HPC software design: erect formal standards for MPI so that designers are properly educated, take advantage of the standards and write comprehensive MPI platform tests, extract finite-state models from MPI programs and analyze them automatically for deadlocks and race conditions, and will instrument the MPI-based program with correctness assertions that can be checked at run-time.The project will advance the state of the art in formal methods by developing algorithms that take advantage of semantic properties of communication libraries. It will help advance the state of the art in parallel scientific programming by encouraging the use of formal assertions, and encouraging the use of formal analysis in lieu of brute-force execution.