EAGER: Formal Reliability Enhancement Methods for Million Core Computational Frameworks

EAGER：百万核心计算框架的正式可靠性增强方法

• 批准号: 1241849
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 20万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-06-01 至 2014-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1241849&HistoricalAwards=false
• 关键词: EAGER; Formal; Reliability; Enhancement; Methods

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.

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