EAGER: Memory Models: Specification and Verification in a Concurrency Intermediate Verification Language (CIVL) Framework

美国的经济发展和国家安全严重依赖于计算机技术的稳定发展。这种进步主要依赖于使用并行编程语言编写的多个处理单元的使用。由于这些并行处理系统在国家安全基础设施、医疗设备、飞机和预测天气的计算装置等关键应用中得到了应用，因此它们必须高度可靠且节能。不幸的是，当今的多处理器很难可靠地使用，也很难使用当前的并行编程语言进行高效编程。除了普遍公认的编写并行程序的困难之外，一个尚未解决的核心困难是开发一个明确定义的共享内存语义，以允许足够的并行性。这种语义规定了计算元素如何交换数据，以及编译器如何安全地优化并行程序。这项工作主要集中在解决与并行程序中并发共享内存交互相关的关键问题。它通过开发一组数学模型来清楚地定义这些相互作用，从而帮助提高了当前的技术水平。这些数学模型将构成开发并行处理器和编译器的基础，这些编译器可以可靠地将用户意图转换为功能正确的计算系统。我们工作的中心重点是，通过建立基于并发中间验证语言的数学模型，它统一地解决了并行处理元素类型和计算机语言的多样性。这项工作的一个同样重要的特点是，这种对内存一致性模型的理解直接转化为严格的错误检查工具，以避免在部署的计算机软件中出现严重错误。该项目的一个关键方面是为并行程序开发这种错误检查工具，并在从国家实验室和工业合作伙伴获得的实际程序中展示这些工具的有效性。

The nation's economic progress and national security are critically dependent on maintaining a trajectory of steady advances in computing. Such advances are crucially dependent on the use of multiple processing units that are programmed using parallel programming languages. As these parallel processing systems find uses in critical applications such as national security infrastructures, medical devices, airplanes, and computing installations that predict our weather, they must be highly reliable as well as energy efficient. Unfortunately, today's multi-processors are extremely difficult to reliably employ and to efficiently program using current parallel programming languages. In addition to the generally recognized difficulty of writing parallel programs, one of the central unresolved difficulties is the development of a clearly defined shared memory semantics that allows sufficient parallelism. This semantics dictates how the computing elements exchange data, as well as how compilers can safely optimize parallel programs.This work primarily focuses on addressing critical problems relating to concurrent shared memory interactions in parallel programs. It helps advance the current state of the art by developing a collection of mathematical models for clearly defining these interactions. These mathematical models will form the bedrock for developing parallel processors as well as compilers that reliably translate user intentions into correctly functioning computing systems. A central emphasis of our work is that it uniformly addresses the multiplicity of parallel processing element types as well as computer languages by erecting these mathematical models based on a Concurrency Intermediate Verification Language. An equally important feature of this work is that this understanding of memory consistency models directly translates into rigorous error-checking tools to avoid egregious mistakes in deployed computer software. A key aspect of this project is the development of such error-checking tools for parallel programs and demonstrating the effectiveness of these tools on realistic programs acquired from national labs and industrial partners.