CAREER: Composable Memory Consistency Models for Heterogeneous Systems

当今的计算机系统是异质的，即由不同的处理单元(PU)组成。历史上，每个处理单元在很大程度上处理其自己的任务，例如，中央处理单元(CPU)运行网络浏览器，而图形处理单元(GPU)执行图形计算。然而，新兴的工作负载，例如在图像识别和粒子模拟中，具有复杂的结构，其可以从PU之间的密切协作中获得数量级的性能好处。这需要关于数据如何在PU之间流动的精确规则，例如，以便不会错过关键更新。这些规则称为内存一致性模型。虽然这些模型已经针对单个PU进行了研究，但对于非均质系统还没有广泛的研究。该项目的新奇之处在于为不同的内存一致性模型设计了一个逻辑框架，这将使系统设计人员能够为不同的PU如何协作提供准确的规则。该项目的影响将利用这个逻辑框架来指定流行的现实世界中各种系统(如移动电话)的行为，从而能够更有效地计算这些设备上的新兴工作负载。此外，该项目将通过专注于可移植抽象来为GPU编程开发公平的教育材料，该抽象可以部署在许多设备和价位上；相比之下，大多数现有材料都绑定到昂贵的供应商特定框架。该项目将利用关系逻辑设计一个模块化和可组合的框架，用于指定不同的内存模型。该框架将允许将现有的内存模型(例如用于CPU和GPU的内存模型)组合在一起来描述异类系统。为了组合不同的模型，调查者将提供一种新的关系，称为异类发生之前，它提供了系统中内存访问的偏序。该框架将在一个可执行的约束求解器中实现，它将允许：(1)在新的内存模型下分析小程序，以及(2)测试用例的自动生成，该测试用例可用于测试现有的异类系统以验证它们是否符合规范。调查员将分析现有的异类应用程序，以确定所需的协作(即同步)模式的特征，并确保逻辑规范可用于推断应用程序的正确性。这些任务结合在一起，为关于异类内存模型的推理提供了理论基础，并展示了如何使用组合技术对复杂的真实世界系统(和应用程序)进行推理。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.