# [译]硬件内存模型

Russ Cox关于内存模型的系列文章之一。这是第一篇 Hardware Memory Models

## 简介: 童话之终局

“看情况”(It depends)并不是一个圆满的结局。程序员需要一个明确的答案来判断一个程序是否在新的硬件和新的编译器上能够正确运行。硬件设计人员和编译器开发人员也需要一个明确的答案，说明在执行给定的程序时，硬件和编译后的代码可以有多精确。因为这里的主要问题是对存储在内存中数据更改的可见性和一致性，所以这个契约被称为内存一致性模型（memory consistency model）或仅仅是内存模型(memory model)。

## 顺序一致性

Leslie Lamport 1979年的论文《How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs》引入了顺序一致性的概念:

The customary approach to designing and proving the correctness of multiprocess algorithms for such a computer assumes that the following condition is satisfied: the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program. A multiprocessor satisfying this condition will be called sequentially consistent.

If the execution of this litmus test is sequentially consistent, there are only six possible interleavings:

(本文中三个内存模型图摘自 Maranget et al. “A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”)

## x86-TSO 之路

x86-TSO模型看起来相当整洁，但是这条道路充满了路障和错误的弯道。在20世纪90年代，第一批x86多处理器可用的手册几乎没有提到硬件提供的内存模型。

Loosely speaking, this means the ordering of events originating from any one processor in the system, as observed by other processors, is always the same. However, different observers are allowed to disagree on the interleaving of events from two or more processors.
Future Intel processors will implement the same memory ordering model.

Plan 9的讨论不是一个孤立的事件。从11月下旬开始，Linux内核开发人员在他们的邮件列表上讨论了100多条消息

2008年晚些时候对英特尔和AMD规范的修订保证了IRIW case的“不”，并加强了内存屏障，但仍允许不可预期的行为，这些行为似乎不会出现在任何合理的硬件上。例如:

## ARM/POWER Relaxed Memory Model

ARM和POWER系统的概念模型是，每个处理器从其自己的完整内存副本中读取和向其写入，每个写入独立地传播到其他处理器，随着写入的传播，允许重新排序。

## 弱排序和无数据竞争的顺序一致性

Sarita Adve and Mark Hill proposed exactly this approach in their 1990 paper “Weak Ordering – A New Definition”. They defined “weakly ordered” as follows.

Sarita Adve和Mark Hill在他们1990年的论文“Weak Ordering – A New Definition”中正是提出了这种方法。他们把“弱有序”定义为如下。

Let a synchronization model be a set of constraints on memory accesses that specify how and when synchronization needs to be done.