CAREER: Composable Memory Consistency Models for Heterogeneous Systems

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

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.