Weak Memory Model Formalisms: Introduction and Survey

TL;DR

This survey paper reviews formal methods for specifying, analyzing, and reasoning about weak memory models in concurrent systems, highlighting their importance for safe low-level software development.

Contribution

It provides a comprehensive overview of formal representations, historical developments, and tools for weak memory models, including simplified examples and future research directions.

Findings

Survey of formal semantics for weak memory models

Comparison of operational and axiomatic approaches

Discussion of tools and future research in the field

Abstract

Memory consistency models define the order in which accesses to shared memory in a concurrent system may be observed to occur. Such models are a necessity since program order is not a reliable indicator of execution order, due to microarchitectural features or compiler transformations. Concurrent programming, already a challenging task, is thus made even harder when weak memory effects must be addressed. A rigorous specification of weak memory models is therefore essential to make this problem tractable for developers of safety- and security-critical, low-level software. In this paper we survey the field of formalisations of weak memory models, including their specification, their effects on execution, and tools and inference systems for reasoning about code. To assist the discussion we also provide an introduction to two styles of formal representation found commonly in the literature (using a much simplified version of Intel's x86 as the example): a step-by-step construction of traces of the system (operational semantics); and with respect to relations between memory events (axiomatic semantics). The survey covers some long-standing hardware features that lead to observable weak behaviours, a description of historical developments in practice and in theory, an overview of computability and complexity results, and outlines current and future directions in the field.