Static Verification for Fearless GPU programming

对图形处理单元(GPU)编程目前是一门为少数专家保留的艺术，因为释放这些设备的全部潜力需要掌握复杂的硬件体系结构和执行模型。科学家和领域专家需要调整他们的算法以适应编程模型，在这种模型中，简单地更改数据访问顺序可能会产生10倍的性能开销，而一个接一个的错误可能会悄悄地破坏他们的数据。这个项目的目的是开发一个补充代码分析技术的基础设施，包括错误预防、性能分析和错误配对。该项目的创新之处在于对性能和安全漏洞的全面理解，它考虑了不同类别漏洞之间的相互作用。该项目的影响是通过向所有程序员提供工具来简化对并行编程和硬件架构的理解，从而使算法正确性和更深入的性能分析，从而使GPU编程更容易获得。该项目的一个结果是提高了开发人员的生产力和软件的可持续性，因为该项目能够在不牺牲这两个目标的情况下编写正确和高效的GPU程序。工业界(例如，自主移动性、人工智能应用)以及学术界和国家实验室都希望对此感兴趣。该研究降低了GPU编程的进入门槛，有望将GPU的适用性扩大到更多的领域。从这个项目中产生的工具可以使学生自主地理解他们代码中的错误，从而在教师和学生之间产生更有针对性的教学体验。该项目在正确性和性能分析方面促进了对GPU和其他加速器架构的静态验证的艺术水平。静态验证的目的是在不执行程序的情况下评估软件的需求。现有的解决方案存在警报频率高、不能处理大代码或声音不佳的问题。最重要的是，现有的方法要么解决性能问题，要么解决安全问题，但不能同时解决这两个问题。该项目的一个关键方面是基础静态验证基础设施，这是由理论结果支持的分析集合，使新的高效工具能够更好地了解现有软件。这种验证基础设施是围绕一种基于行为类型理论的新颖而通用的中间表示来构建的，该表示对并行程序的含义进行了编码、构造和实施。该项目扩展了我们对GPU编程模型的正式理解，引入了安全属性、语义保留转换和行为等价，所有这些都使用了证明助手。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Programming Graphics Processing Units (GPUs) is an art currently reserved to aselect few experts, as unlocking the full potential of these devices requiresmastering an intricate hardware architecture and execution model. Scientists anddomain experts need to adapt their algorithms to a programming model wheresimply changing the order in which data is accessed can have a 10× performanceoverhead, and off-by-one errors can silently corrupt their data. The intent ofthis project is to develop an infrastructure of complementary code analysistechniques that include bug prevention, performance profiling, and bugrepairing. The project's novelties are in developing a holistic understanding ofperformance and safety bugs, which considers the interactions between variousclasses of bugs. The project's impacts are on making GPU programming moreaccessible, by providing tools to all programmers that simplify understandingparallel programming and hardware architectures, thus enabling algorithmcorrectness and more in depth performance analysis. An outcome of this projectis improved developer productivity and software sustainability, as the projectaids in writing correct and highly efficient GPU programs without sacrificingeither objectives. There is an expectation of interest from industry (e.g., autonomousmobility, artificial intelligence applications) as well as from academia andnational laboratories. The research lowers the barrier to entry of GPUprogramming, so it is expected to widen the suitability of GPUs to more fields. Thetools that result from this project can empower students to understand bugs intheir code autonomously, leading to a more focused pedagogical experiencebetween the instructor and the student.This project advances the state of the art of static verification for GPUs andother accelerator architectures, both in terms of correctness and performanceanalysis. Static verification aims to assess the requirements of softwarewithout executing the program. Existing solutions suffer from a high rate offalse alarms, cannot handle large codes, or are unsound. Most importantly,existing approaches either address performance or safety, but not both at once.A key aspect of this project is an underlying static verificationinfrastructure, a collection of analysis backed by theoretical results, thatenables novel and efficient tools that better our understanding of existingsoftware. Such verification infrastructure is built around a novel and generalintermediate representation based on behavioral type theory, which codifies,structures, and enforces the meaning of parallel programs. The project expandsour formal understanding of GPU programming models, by introducing safetyproperties, semantics preserving transformations, and behavioral equivalences,all fully mechanized using a proof assistant.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.