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

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

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.