Collaborative Research: SHF: Medium: Practical and Rigorous Correctness Checking and Correctness Preservation for Irregular Parallel Programs

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

Many important — and in some cases, lifesaving — computations are performed on graph structures consisting of millions of vertices and edges. For example, such graphs might represent medical information, protein interactions, or taxonomies of diseases. Since these graphs tend to be large, they are processed in parallel to fully harness the speed offered by modern computers, which use multicore processors and often general-purpose Graphics Processing Units (GPUs). Unfortunately, parallelizing graph computations is difficult, especially for GPUs,and often leads to accidental uncoordinated accesses known as data races. Data races can be hard to track down as they only sometimes corrupt the result. The project's novelties are the development of scalable and mathematically sound methods for data-race and other bug detection on graph computations. The project's main impact is the elimination of many human programming errors to improve the trust in computations carried out on life-critical and other data.The project develops generic symbolic representations of allowed concurrent operations on primitive data operations. This provides theability to easily boil down new concurrency models into this semantic base to quickly create new analysis tools, thus counteracting verification tool obsolescence. It augments the power of small-scope symbolic-analysis methods with execution-based dynamic-analysis methods that scale to realistic code and data sizes. The project derives real-world case studies from high-performance CUDA and OpenMP implementations of important graph algorithms developed over a decade. The project plans to publicly release the new data-race checking tools as well as verification micro-benchmarks and rigorously verified parallel graph codes. It is also training students whose education is advanced by teaching them modern program analysis methods.This award is co-funded by the Software & Hardware Foundations Program in the Division of Computer & Computing Foundations, and the NSF Office of Advanced Cyberinfrastructure.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.