EAGER: Formal Reliability Enhancement Methods for Million Core Computational Frameworks

高性能计算对国家竞争力具有重要的战略意义。 计算能力的进步涉及到前所未有的并行性水平的使用：涉及数十亿并发活动的编程方法。 计算框架允许这些并行程序以模块化的方式组织，实现更高的可靠性，可扩展性和更好的资源管理能力。该项目在开发或优化计算框架以响应新硬件/软件技术的到来时，开发基于形式的可靠性增强机制。这些机制包括这些框架的预期行为的正式规范，以及在部署之前和实时操作期间验证它们的方法。以这种积极主动的方式解决正确性问题将大大减少从想法到科学的时间。该项目将使科学的理解，正式的方法可能在数百万个核心的规模，以及哪些正式的方法是最好的建议，以捕捉预期的行为与那些最适合运行时使用。 该项目还将产生广泛的影响：将我们的验证工具和技术纳入流行的工具集成框架;在正在开发的计算框架内使用正式方法进行大规模案例研究;以及对本科生和研究生进行高级正确性验证方法的培训。它还将帮助建立人才库，这对高性能计算在科学和工程、能源/可持续性和国土安全方面的应用的持续进展至关重要。

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.