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.