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

点击翻译按钮获取中文摘要

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.