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.