SPX: Write Once, Run on Anything: Verified, Tuned Accelerator Kernels from High Level Specifications

计算中的两个趋势共同导致计算资源的有效利用变得困难。首先，领域专家对部署计算能力感兴趣的应用程序--计算基因组学、视频处理、数据分析--越来越不规律，计算和数据访问的模式很难推理。其次，领域专家想要开发的计算平台越来越异构化，围绕表现出截然不同的性能特征、编程模型和效率权衡的加速器构建。最令人担忧的是，这些加速器通常需要仔细映射计算和数据访问，以实现最高性能--这正是不规则计算中难以完成的任务。该项目的创新之处在于创建了新的领域特定语言(DSL)，允许程序员以高级、易于理解的方式表达复杂的计算，然后将这些DSL映射到新的中间表示法，从而允许不同域中的程序以通用的表示法进行优化。然后，将使用可证明安全的转换来转换该中间表示，以在不牺牲正确性保证的情况下提高性能。最后，转换后的程序将针对加速器自动调优，该调优取决于加速器的特定资源配置文件和应用程序的资源需求。该项目的影响将是向更广泛的程序员和科学家群体释放基于加速器的平台的能力，并为两个丰富的问题域(流视频处理和计算基因组学)和新的加速器提供DSL和相关的编译框架。虽然不同的问题域需要不同的抽象来有效地捕获它们的计算--计算基因组学的字符串处理内核、视频处理的过滤和转换内核--但这些抽象通常可以有效地映射到一个公共的中间表示，该表示仍然捕获程序执行的高级属性，如数据访问模式和并行性属性。这种中间表示形式形成了域不可知转换的基础，可以将计算重组为适合不同加速器范例的模板(例如，为图形处理单元(GPU)等加速器选择宽并行，或为多核中的矢量单元选择较窄的并行)。然后，该项目将使用机器学习来开发加速器模型，允许使用每个应用程序的加速器特定参数实例化这些模板(例如，调整GPU内核中的块大小)，从而最大限度地提高性能。最后，为了确保这个转换和调整管道是健全的，该项目将开发新的验证技术，以确保每个翻译都保持正确。这些工具将允许程序员编写加速器程序，而不必关心他们针对的加速器的正确性或性能的细节。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Two trends in computation have conspired to make efficient exploitation of computational resources difficult. First, the applications for which domain experts are interested in deploying computational power--computational genomics, video processing, data analytics--are increasingly irregular, with patterns of computation and data access that are difficult to reason about. Second, the computational platforms that domain experts want to exploit are increasingly heterogeneous, built around accelerators that present vastly different performance characteristics, programming models, and efficiency tradeoffs. Most worryingly, these accelerators often require careful mapping of computation and data access to achieve maximum performance--exactly the task that is difficult in irregular computations. This project's novelties are creating new domain-specific languages (DSLs) to allow programmers to express complex computations in a high-level, easy-to-understand way, then mapping those DSLs to novel intermediate representations that allow programs in different domains to be expressed in a common representation for optimization. This intermediate representation will then be transformed using provably safe transformations to improve performance without sacrificing correctness guarantees. Finally, the transformed programs will be automatically tuned for accelerators, with that tuning dependent on the specific resource profile of the accelerator and the resource demands of the application. This project's impacts will be unlocking the power of accelerator-based platforms to a broader group of programmers and scientists and providing a DSL and the associated compilation framework to two rich problem domains (streaming video processing and computational genomics) and to new accelerators.While different problem domains require different abstractions to effectively capture their computations--string-processing kernels for computational genomics, filtering and transformation kernels for video processing--these abstractions can often effectively be mapped to a common intermediate representation that nevertheless captures high-level properties of program execution such as data-access patterns and parallelism properties. This intermediate representation forms the basis for domain-agnostic transformations that can restructure computation to templates that fit different accelerator paradigms (for example, choosing wide parallelism for accelerators like Graphics Processing Units (GPUs), or narrower parallelism for vector units in multi-cores). This project will then use machine learning to develop accelerator models that allow these templates to be instantiated with accelerator-specific parameters for each application (e.g., tuning block size in a GPU kernel), and therefore maximize performance. Finally, to ensure that this transformation and tuning pipeline is sound, this project will develop novel verification techniques to ensure that each translation preserves correctness. These tools will allow programmers to write accelerator programs without concerning themselves with the details of the accelerators they are targeting for correctness or performance.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.