CAREER: Type-Driven Heterogeneous Programming

计算机硬件正变得更加异构化：从智能手表到数据中心的系统使用图形处理单元(GPU)、现场可编程门阵列(FGA)和单应用程序加速器来增强传统CPU，以提高效率。然而，这些异类系统的编程工具却落后了。每一种新的计算技术都伴随着一种新的专用编程模型，或者是尽最大努力编译像“C”这样的遗留编程语言。该项目设计的系统能够弥合应用程序语义和硬件约束之间的语义鸿沟。该项目的新颖性是类型驱动的方法，以平衡生产率和对低级别性能细节的控制。该项目的影响是针对异类系统的新编程语言，它们避免了尽力而为的C语言编译的可用性陷阱，暴露了决定性能的系统级问题，并支持跨设备编译器优化。该项目还力求通过针对不同架构的编程的互动式在线课程，扩大获得教育和研究的机会；创建一系列研讨会，以增加对本科生研究的参与；并在计算机架构会议上举办讲习班，以扩大本科生和研究生的参与和指导。这个项目的重点是两个主要方法。第一种方法将针对异类体系结构后端的一次性编译器中的潜在约束提升到可理解的类型系统中。它针对的是高级综合(HLS)编译器，它试图将C或C语言的松散定义的子集转换成硬件。该项目旨在保证类型良好的程序具有可实现的硬件实现。第二种方法将较高级别的抽象嵌入到用于低级计算的类型系统中，以防止错误并启用新的编译器优化。它专注于在GPU上进行线性代数计算。这种计算将抽象的代数属性与低级代码纠缠在一起。一种新的类型系统结合了描述线性代数行为的抽象类型和描述GPU执行的具体类型。组合类型系统避免了细微的错误，并允许编译器自动生成对线性代数结构(如向量空间)的逐个构造的正确操作。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Computer hardware is becoming more heterogeneous: systems from smartwatches to datacenters augment traditional CPUs with Graphics Processing Units (GPUs), Field Programmable Gate Arrays (FPGAs), and single-application accelerators for efficiency. The programming tools for these heterogeneous systems, however, are lagging behind. Each new computing technology comes with a new special-purpose programming model or a best-effort attempt to compile legacy programming languages like 'C'. This project designs systems that bridge the semantic gap between application semantics and hardware constraints. The project's novelties are type-driven approaches to balancing productivity with control over low-level performance details. The project's impacts are new programming languages for heterogeneous systems that avoid the usability pitfalls of best-effort C-language compilation, expose system-level concerns that dictate performance, and enable cross-device compiler optimizations. The project further seeks to include broadening access to education and research through interactive online lessons that target programming for heterogeneous architectures; creating a series of seminars aimed at increasing engagement in undergraduate research; and running workshops at computer architecture conferences for broadening participation of and mentoring of undergraduate and graduate students. This project focuses on two main approaches. The first approach lifts the latent constraints in one-off compilers for heterogeneous architectural backends into an intelligible type system. It addresses high-level synthesis (HLS) compilers for FPGAs, which attempt to translate a loosely-defined subset of C or C++ to hardware. The project aims to guarantee that well-typed programs have a realizable hardware implementation. The second approach embeds a higher level of abstraction into the type system for low-level computations to prevent bugs and enable new compiler optimizations. It focuses on linear algebra computations on GPUs. Such computations entangle abstract algebraic properties with low-level code. A new type system combines abstract types describing the linear algebra behavior with concrete types describing the GPU execution. The combined type system avoids subtle bugs and lets the compiler automatically generate correct-by-construction manipulations of linear algebra structures such as vector spaces.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.