Static Verification for Fearless GPU programming

图形处理单元（GPU）编程目前是一门只有少数专家才能掌握的艺术，因为要充分发挥这些设备的潜力，需要掌握复杂的硬件架构和执行模型。科学家和领域专家需要使他们的算法适应一种编程模型，在这种模型中，简单地改变数据访问的顺序可能会带来10倍的性能开销，而逐个错误可能会悄悄地破坏他们的数据。这个项目的目的是开发一个补充代码分析技术的基础设施，包括错误预防，性能分析和错误配对。该项目的新颖之处在于对性能和安全漏洞的整体理解，它考虑了各种漏洞之间的相互作用。该项目的影响是通过向所有程序员提供简化并行编程和硬件架构理解的工具，使GPU编程更容易获得，从而实现算法正确性和更深入的性能分析。该项目的一个成果是提高了开发人员的生产力和软件的可持续性，因为该项目有助于编写正确和高效的GPU程序，而不会违背任何一个目标。有一个来自工业界的兴趣的期望（例如，以及来自学术界和国家实验室。该研究降低了GPU编程的门槛，因此有望将GPU的适用性扩展到更多的领域。该项目的工具可以让学生自主地理解代码中的错误，从而在教师和学生之间形成更专注的教学体验。该项目在正确性和性能分析方面都提升了GPU和其他加速器架构的静态验证技术水平。静态验证的目的是在不执行程序的情况下评估软件的需求。现有的解决方案存在高错误率警报、不能处理大代码或不可靠的问题。最重要的是，现有的方法要么解决性能问题，要么解决安全问题，但不能同时解决这两个问题。这个项目的一个关键方面是一个底层的静态验证基础设施，一个由理论结果支持的分析集合，它可以使我们更好地理解现有软件的新颖而有效的工具。这样的验证基础设施是建立在一个新的和generalintermediate表示的基础上的行为类型理论，编纂，结构，并强制执行的意义上的并行程序。该项目扩展了我们对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.