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

对高性能的追求推动了并行科学计算软件的设计。超过60%的高性能计算（HPC）社区使用MPI库编写程序;为了获得性能，他们执行许多手动优化。即使是从高级描述生成MPI的团队，由于其出色的可移植性，最终似乎也会生成MPI代码。然而，由于性能不端口，手动调整是不可避免的。这一点，加上MPI标准的广泛性和不断发展的性质，以及并发编程的固有复杂性，引入了代价高昂的bug。形式化方法正享受着爆炸性的增长，以帮助消除这些bug。它们已经在不同的领域找到了应用，从形式验证优化编译器转换，形式调试设备驱动程序代码，到巩固工业标准。 该项目将调查并采用一些互补的正式方法来进行HPC软件设计：建立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.