CAREER: Composable Memory Consistency Models for Heterogeneous Systems

Today’s computer systems are heterogeneous, i.e., composed of different processing units (PUs). Historically, each processing unit has largely worked on its own task, e.g., central processing units (CPUs) run web browsers, while graphics processing units (GPUs) perform graphics computations. However, emerging workloads, e.g., in image recognition and particle simulation, have a complex structure that can achieve an order-of-magnitude performance benefit from close collaboration between PUs. This requires precise rules for how data flows between PUs, e.g., so that critical updates are not missed. These rules are called the memory consistency model. While these models have been studied for individual PUs, they have not been widely studied for heterogeneous systems. The project’s novelty is to design a logical framework for heterogeneous memory consistency models, which will enable system designers to provide precise rules for how different PUs can collaborate. The project’s impact will utilize this logical framework to specify the behavior of prevalent real-world heterogeneous systems, such as mobile phones, and thus enable more efficient computation of emerging workloads on these devices. Additionally, this project will develop equitable educational material for GPU programming by focusing on portable abstractions, which can be deployed across many devices and price points; in contrast, most existing material is tied to expensive vendor-specific frameworks. This project will utilize relational logic to design a modular and composable framework for specifying heterogeneous memory models. The framework will allow existing memory models, e.g., for CPUs and GPUs, to be composed together to describe a heterogeneous system. In order to compose different models, the investigator will provide a new relation, called the heterogeneous happens-before, which provides a partial order across memory accesses in the system. The framework will be implemented in an executable constraint solver, which will allow: (1) small programs to be analyzed under the new memory models, and (2) the automatic generation of test cases, which can be used to test existing heterogeneous systems to validate that they conform to a specification. The investigator will analyze existing heterogeneous applications to characterize the required collaboration (i.e., synchronization) patterns and ensure that the logical specifications can be used to reason about the correctness of the applications. Combined, these tasks provide a theoretical foundation for reasoning about heterogeneous memory models and show how complex real-world systems (and applications) can be reasoned about using compositional techniques. 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.