Collaborative Research: Finite-State Verification for High-Performance Computing

摘要0541035/0540948/0541263 PI（电极导线/UMass）：Stephen F. Siegelco-PI（马萨诸塞大学）：乔治AvruninPI（UNL）：Matthew DwyerPI（芝加哥大学）：Andrew Siegel合作研究：高性能计算（HPC）已经彻底改变了广泛的科学和工程工作，包括气候建模，计算流体动力学，分子工程，以及建筑物，飞机和汽车的设计。 并行计算机，其中一些包含超过10万个处理器，使这种计算成为可能。 不幸的是，对这些机器进行编程是出了名的困难：并行程序极其复杂，难以调试，并且可能以不可预测的方式运行。 随着科学应用的规模和复杂性的增加，开发它们所需的工作量正在以惊人的速度增长，并且正在形成一种共识，即需要新的开发方法。本项目的目标是开发一套有限状态验证（FSV）技术，使HPC开发人员能够根除错误并确认他们的程序满足指定的要求。 FSV技术涉及将算法方法应用于被分析程序的形式模型。 虽然这些技术已经成功地用于其他一些编程领域，但在成功地应用于HPC软件之前，必须克服许多挑战。 最终的结果将是提高HPC开发人员的生产力，并增加他们对程序正确性的信心。

ABSTRACT0541035/0540948/0541263PI (lead/UMass): Stephen F. Siegelco-PI (UMass): George AvruninPI (UNL): Matthew DwyerPI (UChicago): Andrew SiegelCollaborative Research: Finite-State Verification for High-Performance ComputingHigh performance computation (HPC) has revolutionized a wide range of scientific and engineering endeavors, including climate modeling, computational fluid dynamics, molecular engineering, and the design ofbuildings, airplanes, and cars. Parallel computers, some of which contain over one hundred thousand processors, make this computation possible. Unfortunately, programming these machines is notoriouslydifficult: parallel programs are extremely complex, difficult to debug, and can behave in unpredictable ways. As scientific applications increase in scale and complexity, the effort required to develop them is growing at an alarming rate, and there is an emerging consensus that new development methods are required.The goal of this project is to develop a body of finite-state verification (FSV) techniques that will allow HPC developers to root out bugs and confirm that their programs meet specified requirements. FSV techniques involve the application of algorithmic methods to a formal model of the program being analyzed. While these techniques have been used successfully in some other programming domains, a number of challenges must be overcome before they can be successfully applied to HPC software. The ultimate result will be an increase in productivity of HPC developers and an increased confidence in the correctness of their programs.