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.