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

协作研究：高性能计算的有限状态验证

• 批准号: 0541263
• 负责人: Matthew Dwyer
• 金额: $ 30万
• 依托单位: University of Nebraska-Lincoln
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-04-15 至 2010-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0541263&HistoricalAwards=false
• 关键词: Collaborative; Research; Finite; State; Verification

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.

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广泛的科学和工程努力，包括气候建模，计算流体动力学，分子工程以及建筑，飞机和汽车的设计。 并行计算机（其中一些包含十万个处理器）使此计算成为可能。 不幸的是，对这些机器进行编程是众所周知的：平行程序非常复杂，难以调试，并且可以以不可预测的方式行事。 随着科学应用的规模和复杂性的提高，开发它们所需的努力正在以惊人的速度增长，并且有一个新的共识，即需要新的开发方法。该项目的目的是开发有限状态验证（FSV）技术的技术，该技术将允许HPC开发人员脱离错误并确认其程序满足指定要求。 FSV技术涉及将算法方法应用于被分析的程序的正式模型。 尽管这些技术已成功地用于其他一些编程域中，但在将它们成功应用于HPC软件之前，必须克服许多挑战。 最终结果将是HPC开发人员的生产率提高，并提高对计划的正确性的信心。