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

合作研究：SHF：Medium：不规则并行程序的实用且严格的正确性检查和正确性保持

• 批准号: 1956106
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 44.76万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-08-01 至 2024-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1956106&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Medium; Practical

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.

许多重要的-在某些情况下，救命-计算是在由数百万个顶点和边组成的图结构上执行的。 例如，这样的图可能表示医学信息、蛋白质相互作用或疾病分类。 由于这些图形往往很大，它们被并行处理，以充分利用现代计算机提供的速度，这些计算机使用多核处理器和通用图形处理单元（GPU）。不幸的是，并行化图计算是困难的，特别是对于GPU，并且经常导致被称为数据竞争的意外不协调访问。 数据竞争可能很难追踪，因为它们只是有时会破坏结果。 该项目的新颖之处在于开发了可扩展的、数学上合理的方法，用于图计算的数据竞争和其他错误检测。 该项目的主要影响是消除了许多人类编程错误，以提高对生命关键数据和其他数据进行计算的信任。该项目开发了允许对原始数据操作进行并发操作的通用符号表示。 这提供了将新的并发模型简化到这个语义基础中的能力，以快速创建新的分析工具，从而抵消验证工具的过时。 它通过基于执行的动态分析方法增强了小范围符号分析方法的功能，这些方法可以扩展到实际的代码和数据大小。 该项目从十多年来开发的重要图形算法的高性能CUDA和OpenMP实现中获得真实案例研究。该项目计划公开发布新的数据竞争检查工具以及验证微基准和严格验证的并行图形代码。 该奖项由计算机计算基础部门的软件硬件基础项目和NSF高级网络基础设施办公室共同资助。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。