EAGER: Formal Reliability Enhancement Methods for Million Core Computational Frameworks

University Of Utah, Salt Lake City UT

Investigators

Abstract

High Performance Computing is strategically important to national competitiveness. Advances in computational capabilities involve the use of unprecedented levels of parallelism: programming methods that involve billions of concurrent activities. Computational Frameworks allow these parallel programs to be organized in a modular fashion, achieving higher reliability, scalability, and better resource management capabilities. The project develops formally based reliability enhancement mechanisms when Computational Frameworks are developed or optimized in response to the arrival of newer hardware/software technologies. These mechanisms include a formal specification of the expected behavior of these frameworks, and ways to verify them before deployment and during live operation. Correctness issues addressed in this proactive manner will considerably reduce the time it takes to proceed from idea to science. This project will enable a scientific understanding of which formal methods are likely to work at the scale of millions of cores, and which formal methods are best recommended to capture intended behavior versus those that are best suitable for run-time use. The project will also result in broad impact in terms of: the incorporation of our verification tools and techniques within popular tool-integration frameworks; achieving large-scale case studies on the use of formal methods within a computational framework that is under development; and training of undergraduate and graduate students on advanced correctness verification methods. It will also help build talent pool vital to continued progress in high performance computing with applications to science and engineering, energy/sustainability, and homeland security.