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.

翻译：内存一致性模型定义了并发系统中共享内存访问可被观测到的发生顺序。由于微架构特性或编译器转换，程序顺序并非执行顺序的可靠指示，因此此类模型不可或缺。并发编程本已极具挑战性，在必须处理弱内存效应时变得更为困难。因此，对弱内存模型进行严格规范对于开发安全关键、安全攸关的低层软件至关重要。本文系统综述弱内存模型形式化领域，涵盖其规范定义、对执行的影响，以及用于代码推理的工具与推断系统。为辅助讨论，我们还对文献中常见的两种形式化表示风格进行导论性介绍（以高度简化的英特尔x86架构为例）：基于系统执行轨迹逐步构建的方法（操作语义学）；以及基于内存事件间关系的方法（公理语义学）。本综述涵盖导致可观测弱行为的若干长期存在的硬件特性，描述实践与理论中的历史发展脉络，概述可计算性与复杂性研究成果，并展望该领域的当前趋势与未来方向。