0541035/0540948/0541263 PI (lead/UMass): Stephen F. Siegel co-PI (UMass): George Avrunin PI (UNL): Matthew Dwyer PI (UChicago): Andrew Siegel
Collaborative Research: Finite-State Verification for High-Performance Computing
High performance computation (HPC) has revolutionized a wide range of scientific and engineering endeavors, including climate modeling, computational fluid dynamics, molecular engineering, and the design of buildings, airplanes, and cars. Parallel computers, some of which contain over one hundred thousand processors, make this computation possible. Unfortunately, programming these machines is notoriously difficult: 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.
