CAREER: Type-Driven Heterogeneous Programming

点击翻译按钮获取中文摘要

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.