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

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

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.