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

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

• 批准号: 1955852
• 负责人: Stephen Siegel
• 金额: $ 44.85万
• 依托单位: University of Delaware
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-08-01 至 2025-07-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1955852&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高级Cyber​​infradstructure的办公室。该奖项反映了NSF的法规任务，并认为通过基金会的知识优点和广泛的critia critia criter criter criter criter criter criter criter critia criter critia criter critia criter critia criteria criter critia criteria criteria cripitia均可表现出宝贵的支持。

项目成果

Verifying Fortran Programs with CIVL

使用 CIVL 验证 Fortran 程序

• DOI: 10.1007/978-3-030-99524-9_6
• 发表时间: 2022
• 期刊: TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems
• 作者: Wu, Wenhao;Hückelheim, Jan;Hovland, Paul D.;Siegel, Stephen F.
• 通讯作者: Siegel, Stephen F.