Specifying, Verifying, and Translating Between Memory Consistency Models

Abstract

In modern hardware, inter-core communication takes place through shared virtual memory and according to the memory consistency model---the set of rules and guarantees about the ordering and visibility of memory accesses. Unfortunately, consistency models frequently suffer from a lack of formalism, precision, and/or completeness, resulting in situations in which the legal behavior(s) for a given program may be left underspecified and/or undefined.

First, this thesis proposes Memory Ordering Specification Tables (MOSTs), a model-independent method for specifying memory ordering requirements, and it also proposes the ArMOR framework for systematically comparing and manipulating MOSTs. The architecture-independent approach used by MOSTs and ArMOR allows for direct comparison of preserved program order, fences, and other ordering enforcement mechanisms from different models. This thesis demonstrates the power of ArMOR by using it to produce optimized, self-contained translation engines called shims that automatically and dynamically translate code compiled under the assumptions of one memory model into code which can be executed by a (micro)architecture implementing a different model.

Second, this thesis proposes PipeCheck, a framework for verifying the correctness of particular implementations of a given memory model. PipeCheck's domain-specific language allows it to explicitly specify and verify the behavior of common microarchitectural optimizations such as speculative load reordering, even though such optimizations are intentionally abstracted away by higher-level models. PipeCheck's fast constraint solver software quantifies in just minutes whether an implementation is stronger than, weaker than, or equal in strength to its memory model requirements. The PipeCheck approach reduces the problem of verifying memory model implementation correctness into the more tractable task of verifying a set of more localized, self-contained axioms about behaviors of the given implementation.

In summary, this thesis presents architects with new techniques for reducing the complexity of defining memory consistency models and building systems that correctly implement them. As hardware and software complexity continues to grow, the techniques developed in this thesis will help designers avoid the memory model bugs that continue to appear in hardware even today, and they will present programmers, compiler writers, and runtime systems with usable, precise descriptions of the memory ordering behaviors of any computing system.