Collaborative Research: Finite-State Verification for High-Performance

0541035/0540948/0541263PI(Lead/UMassas)：Stephen F.Siegelco-Pi(UMassas)：George Avrunin PI(UNL)：Matthew DwyerPI(UChicago)：Andrew Siegel协作研究：用于高性能计算的有限状态验证高性能计算(HPC)已经彻底改变了一系列科学和工程工作，包括气候建模、计算流体动力学、分子工程以及建筑、飞机和汽车的设计。并行计算机，其中一些包含超过十万个处理器，使这种计算成为可能。不幸的是，编程这些机器是出了名的困难：并行程序极其复杂，难以调试，并且可能以不可预测的方式运行。随着科学应用程序规模和复杂性的增加，开发它们所需的工作正以惊人的速度增长，需要新的开发方法的共识正在形成。该项目的目标是开发一套有限状态验证(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.