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

点击翻译按钮获取中文摘要

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.