CCF: SHF: Medium: Collaborative: A Static and Dynamic Verification Framework for Parallel Programming

CCF：SHF：媒介：协作：并行编程的静态和动态验证框架

• 批准号: 1302570
• 负责人: Vivek Sarkar
• 金额: $ 40万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-04-15 至 2017-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1302570&HistoricalAwards=false
• 关键词: CCF; SHF; Medium; Collaborative; Static

Human society is faced with an increasing number of problems includingstubborn diseases and international security/climate threats. Thecomputer simulations and advanced data management methods necessary tosolving these societal problems can only be realized through increaseduse of parallel computing at all system scales, including desktops,servers and the cloud. Efficient large-scale parallel computinghowever requires advanced parallel programming methods. Such methods,unfortunately, have a greater proclivity for software bugs thatincrease cost through lost cycles on super-computers and these samebugs undermine confidence in simulation results. This researchaddresses the challenge of developing parallel computing software bycreating new scalable methods to support advanced parallel programmingmodels that provide rigorous guarantees on program correctness. Thesocietal impacts of this work stem from increasing reliability ofsoftware powering the national infrastructure, advanced educationalmethods to train future generations, and pedagogical material in theform of course notes and software for broad dissemination. It alsohelps maintain the United States in a leadership situation withrespect to the available talent pool in this area.Providing rigorous guarantees on correctness of existing parallelcomputing software requires that two classes of methods be developed,evaluated, and taught widely: scalable code-level (static) checkingmethods, and downstream detailed (dynamic) checking methods. Thisproject develops these novel and much-needed correctness checkingmethods around the Habanero Java programming and compilationsystem. The research is to augment the system with correctnessobligations emitted during compilation and checked at all later stagesof translation and deployment. A key highlight of the project'sapproach is that it allows some of the correctness obligations to bechecked statically in the context of safe subsets of Habanero Java.Obligations that are not able to be statically checked, especially forlarger subsets of the Habanero language, are marked for checkingdynamically through novel active-testing methods. An OperationalSemantics written in the Coq notation lends cohesion to the work byensuring that the division of correctness checking between static anddynamic techniques is sound. In summary, this research helps advancethe science of parallel programming in terms of rigorous correctnesschecking methods, while at the same time contributing to the broadpractice of programming at all scales from desktop to cloudcomputing and high-end scientific simulations.

人类社会面临着越来越多的顽疾、国际安全/气候威胁等问题。解决这些社会问题所需的计算机模拟和先进的数据管理方法只能通过在所有系统规模（包括桌面、服务器和云）上增加使用并行计算来实现。然而高效的大规模并行计算需要先进的并行编程方法。不幸的是，此类方法更容易出现软件错误，这些错误会因超级计算机上的周期丢失而增加成本，而这些相同的错误会破坏模拟结果的可信度。 这项研究通过创建新的可扩展方法来支持先进的并行编程模型，为程序的正确性提供严格的保证，从而解决了开发并行计算软件的挑战。这项工作的社会影响源于为国家基础设施提供动力的软件的可靠性不断提高、培训后代的先进教育方法以及以课程笔记和软件形式广泛传播的教学材料。 它还有助于保持美国在该领域可用人才库方面的领先地位。为现有并行计算软件的正确性提供严格的保证需要广泛开发、评估和教授两类方法：可扩展的代码级（静态） ）检查方法，以及下游详细（动态）检查方法。该项目围绕 Habanero Java 编程和编译系统开发了这些新颖且急需的正确性检查方法。该研究旨在通过编译期间发出的正确性义务来增强系统，并在翻译和部署的所有后期阶段进行检查。 该项目方法的一个关键亮点是它允许在 Habanero Java 安全子集的上下文中静态检查一些正确性义务。无法静态检查的义务，特别是对于 Habanero 语言的较大子集，会被标记通过新颖的主动测试方法进行动态检查。用 Coq 表示法编写的操作语义通过确保静态和动态技术之间正确性检查的划分是合理的，为工作提供了凝聚力。总之，这项研究有助于在严格的正确性检查方法方面推进并行编程科学，同时有助于从桌面到云计算和高端科学模拟的各种规模的编程的广泛实践。