【译】编程语言内存模型 Programming Language Memory Models

JuneBao

发布于 2022-10-26 15:27:37

1.6K0

发布于 2022-10-26 15:27:37

文章被收录于专栏：JuneBao

这是 RSC 关于 Go 内存模型系列文章的第二篇，介绍了 Java，C/C++，Rust，JavaScript 等高级语言的内存模型。对于高级语言来说，如何定义竞争，如何避免竞争，竞争发生时编程语言能提供什么保证都是内存模型需要考虑的问题。

编程语言内存模型

(Memory Models, Part 2)

Posted on Tuesday, July 6, 2021. PDF

编程语言的内存模型回答了并行的程序可以依赖哪些（硬件）行为以便在线程之间共享内存的问题。例如，考虑以下类 c 程序, 其中 x 和 done 都是从零开始的：

// Thread 1           // Thread 2
x = 1;                while(done == 0) { /* loop */ }
done = 1;             print(x);

程序尝试将变量 x 的值从线程 1 同步给线程 2，使用变量 done 作为准备好接收消息的信号，如果线程 1 和线程 2 都运行在自己专门的线程上，并且都执行结束，则该程序能保证按预期打印 1 吗？编程语言的内存模型回答了这个问题以及其他类似的问题。

尽管每个编程语言在细节上有所不同，但有一些通用的答案基本能始应现代的多线程程序，包括 C, C++, Go, Java, JavaScript, Rust 和 Swift :

首先，如果 x 和 done 是普通变量，那么线程 2 的循环可能永远不会停止。一个常见的编译器优化是在变量第一次使用时将其加载到寄存器中，然后在将来尽可能长时间地来使用该寄存器来访问该变量。如果线程 2 在线程 1 执行之前将 done 复制到寄存器中，它可能会在整个循环中一直使用该寄存器，而不会注意到线程 1 在稍后修改了 done.
其次，即便线程 2 地循环停止，即已经观察到 done == 1, 线程 2 任然可以输出 x = 0. 编译器经常根据优化启发式（optimization heuristics）甚至是生成代码时遍历哈希表或其他数据结构地形式对程序读写进行重排序。线程 1 编译后的代码可能在 done 赋值之后而不是之前写入 x，而且线程 2 编译后的代码也可可能在循环之前读取 x

考虑到这个程序的缺陷，显而易见的问题是如何修复它。

现代编程语言以原子变量或原子操作的形式提供了一些特殊的功能，以允许程序同步其线程，如果将 done 设置为原子变量（或者在支持原子操作的语言中使用原子操作操作它），那么我们的程序将保证正确结束并打印出 1 ，将 done 设置为 “原子的” 会产生很多效果：

线程 1 编译后的代码必须保证对 x 的写完成，并且在写 done 之前需要保证 x 的写入结果对其他线程可见。
线程 2 编译后的代码必须在每次循环时重新读取 done 的值。
线程 2 编译后的代码必须保证在读 x 之前先读 done
编译后的代码需要做一些必要的事情来组织可能重新导致这些问题的硬件优化。

使 done 原子化的最终结果就是程序将按我们预期的样子执行：成功将 x 的值从线程 1 传递到线程 2.

在原来的代码中，经过编译器的代码重排序后，线程 1 可能在线程 2 读取 x 的同时修改 x 的值，这就是数据竞争(data race) ，在修改后的程序中，原子变量 done 用于同步对 x 的访问: 现在，线程 1 在写 x 的同时线程 2 再读 x是不可能的了，该程序就是无数据竞争（data-race-free）的了。通常，现代语言保证无数据竞争的程序总是以顺序一致的方式执行，就像来自不同线程的操作都被安排到单一的处理器上交叉执行，但没进行重新排序一样。这是硬件内存模型的 DRF-SC 属性，被应用到了编程语言的上下文中。

顺便一提，这些原子变量或原子操作更恰当的应该被称之为 “同步原子（synchronizing atomic）”，在数据库的意义上，这些操作确实是原子的，允许同时读取和写入，就像按某种顺序顺序运行一样：在使用 atomic 时，普通变量的竞争不再是竞争。但更重要的是 atomic 同步程序的其余部分，这提供了一种消除非原子数据竞争的方法。不过它的标准术语就是普通的 "原子（atomic）" 故本文也这样使用，除非另外说明，你只需要记住，我们在说 “原子（atomic）” 时指的就是 “同步原子（synchronizing atomic）”。

编程语言的内存模型规定了程序员和编译器之间需要约定的确切细节。上述概括的一般特征基本上适用于所有现代编程语言，但这一点直到最近才趋于相同，在 20 世纪之初，有着更多明显的差异。即使在今天，不同编程语言在二阶逻辑（second-order）问题上依然存在诸多差异，包括：

原子变量本身的顺序保证是什么
变量是否既可以原子访问，又可以非原子访问
除了原子之外是否还有其他的同步机制
是否存在不同步的原子操作
有数据竞争的程序有什么保证吗

在做一些基本的准备操作后，本文剩余的部分将探讨不同编程语言如何回答这些问题，以及他们解决这些问题的办法。本文同样会介绍在探索路上的那些错误设计，来强调在很大程度上，我们仍然在学习什么是管用的，什么是不管用的。

硬件、Litmus Tests、Happens Before 和 DRF-SC

在我们详细了解特定语言的细节之前，让我们先对硬件内存模型做一个简要的总结。

不同的 CPU 架构允许对不同的指令进行重排序，因此在多核处理器上并行运行的代码根据体系结构到的不同可能会产生不同的执行结果。黄金法则是顺序一致性，他要求任何（并发的）执行其最终表现结果都表现为程序只是以某种顺序在单个处理器上交错执行。这个模型对开发人员来说更容易理解，但现在还没有主要的体系结构去支持它，因为较弱的保证往往能提供更好的性能。

其实很难对不同的内存模型进行全面的比较，但是 Litmus 测试可以帮助你只专注于特定的测试用例，如果两个内存模型针对给定的 Litmus 表现出不同的行为，那这证明他们是不同的，这至少能帮我们看到在这一个测试用例中，一个内存模型是否比另一个更强或更弱。例如这是我们之前检查程序的一条 Litmus 测试：

Litmus Test: Message Passing
Can this program see r1 = 1, r2 = 0?

// Thread 1           // Thread 2
x = 1                 r1 = y
y = 1                 r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: yes!
In any modern compiled language using ordinary variables: yes!

如在前一篇文章中一样，我们假设每个实例中共享变量的初始值都是零，rn 表示私有存储，比如寄存器或函数局部变量, 其他名称如 x 和 y 是不同的共享(全局)变量。我们询问在执行结束后，寄存器是否可以是特定的值。在回答硬件的 Litmus 测试时，我们假设没有编译器对线程中的代码进行重排序：列表中的指令将直接翻译成汇编指令在处理器上执行。

结果 r1 = 1, r2 = 0 代表原始程序（上面第一个程序）的线程 2 结束了 “循环” （这里 done 变成了 y）然后输出 0，程序在任何顺序一致的机器上交错执行都无法重复该结果，对于汇编语言版本，尽管由于处理器本身的指令重排，在 x86 上打印出 0 也是不可能的；但在 ARM 和 POWER 等更宽松的的架构上打印出 0 就是可能的。在现代编程语言中，由于编译器的指令重排，使得无论底层硬件是什么，这个结果都有可能出现。

正如我们前面说到的，当今的处理器并不能支持顺序一致性，它们只能保证 “无数据竞争的顺序一致性 DRF-SC” 保证 DRF-SC 的系统必须提供 原子指令 以协调不同处理器上的操作。程序通过这些指令使得在运行在不同的处理器上的代码之间可以建立起 “happens before” 关系。

例如，下图简单描述了两个线程上发生的操作，与之前一样，我们设定每个线程运行在自己的处理器上：

其实我们在上一章中已经看见过这张图了，线程 1 和线程 2 之间执行了一个同步操作 S(a) 在这个程序中，两个 S(A) 操作建立起了线程 1 和线程 2 之间的 “happens before” 关系，因此线程 1 的 W(x) 操作是在线程 2 的 R(x) 操作之前发生的。

在不同进程中的两个事件没有按照 “happened-before” 的顺序发生，它们有可能是同时发生的，总之顺序不能确定，我们就说它们是并行执行的。数据竞争就是对一个变量的读写操作并行执行导致的。提供了 DRF-SC 保证的处理器（当今的所有处理器）可以保证在运行没有数据竞争的程序时就像其运行在顺序一致的架构上一样。这是在现代处理器上编写多线程程序最基本的保障。

正如我们之前所看到的，DRF-SC 也是现代编程语言所采用的最基本的保证，它使得使用高级编程语言编写多线程程序成为可能。

编译器和优化

我们上次已经多次提到过，在编译器生成最终代码的过程中，它可能会对输入的程序中的指令进行重排序，接下来让我们仔细研究一下这件事以及它可能引起的其他问题。

通常，我们认为只要对读写操作的重排序不会影响其在单线程中的执行，那么编译器就可以任意地对这些操作进行重排序。例如下面这个程序：

w = 1
x = 2
r1 = y
r2 = z

因为 w,x,y,z 都是不同的变量，所以这四条语句可以任意的编译器认为更优的顺序执行。

如上，允许如此自由地对读写操作进行重排序使得大部分遍以后程序的一致性保证起码与 ARM/POWER 宽松内存模型一样（弱），因为她们无法通过一系列的 Limit 测试。事实上，编译后程序的保证本来就比较弱。

在硬件那一章中，我们把相干性（coherence）作为 ARM/POWER 模型也可以保证一些事情的一个依据：

Litmus Test: Coherence
Can this program see r1 = 1, r2 = 2, r3 = 2, r4 = 1?
(Can Thread 3 see x = 1 before x = 2 while Thread 4 sees the reverse?)

// Thread 1    // Thread 2    // Thread 3    // Thread 4
x = 1          x = 2          r1 = x         r3 = x
                              r2 = x         r4 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): no.
On ARM/POWER: no.
In any modern compiled language using ordinary variables: yes!

现代所有硬件都保证了相干性，这里也可以看作是对内存上某个位置的内存一致性，在这个程序中，一定是一个内存的写入覆盖了另一个的写入。并且整个系统必须就哪个覆盖了哪个达成一致。但是事实证明，由于编译过程中的指令重排序，现代编程语言甚至没有提供相干性保证。

译者注：关于相干性的问题可以看 RSC 的上一篇硬件内存模型的文章，ARM/POWER 模型每个核心都有自己的内存副本，每个核心上的读写操作都是独立地传播到其他核心上的，并且它允许延迟读操作，这其实就相当于是硬件层面的读写重排序了，但不管怎样，硬件都会保证在谁覆盖谁这件事上是确定的，不存在薛定谔的覆盖。

假设编译器对线程 4 中的两条指令进行重排，然后程序向下面这样执行时：

// Thread 1    // Thread 2    // Thread 3    // Thread 4
                                             // (reordered)
(1) x = 1                     (2) r1 = x     (3) r4 = x
               (4) x = 2      (5) r2 = x     (6) r3 = x

其结果就是 r1 = 1, r2 = 2, r3 = 2, r4 = 1 这在汇编语言中是不存在的，但在高级语言中确是可能存在的，从这个意义上来说，编程语言的内存模型要比最弱的硬件内存模型还弱。

但同样它也还是有一些保证的。所有人都同意编程语言需要提供 DRF-SC 它不允许引入新的读写优化，即使它们在单线程程序中是有效的。

例如，考虑下面这个程序：

if(c) {
    x++;
} else {
    ... lots of code ...
}

if 块中只有一条简单的 x++ 语句，但 else 块中有大量代码，去除掉分支并且消除 if 块可能会更加高效。我们可以在 if 之前运行 x++，如果我们错了, 就在 else 主体中调整 x 。也就是说，编译器可能会考虑将该代码重写为：

x++;
if(!c) {
    x--;
    ... lots of code ...
}

这是一个安全的编译器优化吗? 在单线程程序中，确实是的。但在一个多线程程序中，如果 c 为 false 且 x 与另一个线程共享时，就不是了: 优化将引入在原始程序中不存在的对 x 的竞争。

这个例子来自 Hans Boehm 在 2004 年的论文《Threads Cannot Be Implemented As a Library》，这使得语言不能对多线程执行的语义保持沉默。

编程语言内存模型试图精确地回答哪些优化是允许的，哪些是不允许的。通过研究过去几十年来编写这些模型的尝试历史，我们可以了解哪些是有效的，哪些是无效的，并对事情的发展方向有一种感觉。

原始 Java 内存模型(1996)

Java 时第一个尝试对多线程进行保护的主流编程语言，它包含互斥锁，并且定义了它们所隐含的内存顺序的要求。他还包含 volatile 原子变量，所有对 volatile 变量的读写操作都必须按程序定义的顺序直接在主存上执行，这使得对 volatile 变量的操作得以以顺序一致的方式运行。最后，Java 还定义(或至少试图定义)具有数据竞争的程序的行为。这其中的一部分是强制要求普通变量的一种相干性，我们将在下面更多地研究这一点。不幸的是，在 Java语言规范的第一版(1996) 中，这种尝试至少有两个严重的缺陷。作为事后诸葛亮，在今天，它们很容易解释，但是在当时，它们远没有那么明显。

原子需要同步（Atomics need to synchronize）

第一个缺陷是 volatile 原子变量不是同步的，因此它们不能帮助消除程序其余部分中的竞争。例如这个版本的 Java 的一个例子：

int x;
volatile int done;

// Thread 1           // Thread 2
x = 1;                while(done == 0) { /* loop */ }
done = 1;             print(x);

因为 done 被定义为 volatile，所以这个循环一定会结束：编译器无法将其缓存到寄存器中，从而导致无限循环。但是线程 2 并不一定能打印出 1，没有禁止编译器对 x 和 done 的访问进行重新排序，也没有要求禁止硬件做同样的事情。

因为Java volatile 是非同步原子，所以不能使用它们来构建新的同步原语。从这个意义上说，原始的Java内存模型太弱了。

相干性与编译器优化是不兼容的

原始的 Java 内存模型有时也太严格了，它保证了强相干性，一旦一个线程读取了线程某一位置的一个变量，他将不允许在这之后再读到旧值，也就是禁止了编译器优化。之前我们讲过指令重排序会破坏相干性，您可能会想：好吧，我不重排序了。但下面这种优化也会以一种微妙的方式破坏相干性——公共子表达式消除。

考虑下面这个 Java 程序：

// p and q may or may not point at the same object.
int i = p.x;
// ... maybe another thread writes p.x at this point ...
int j = q.x;
int k = p.x;

在此程序中，常见的子表达消除会注意到 P.X 计算了两次，并最终将其优化为 k = i。但是，如果 p 和 q 指向同一个对象，并且在读取 i 和 j 的过程中，另一个线程写入了 p.x，那么在 k 中重用原来的值 i 就违反了相干性：读到 i 看到了一个旧值，读到 j 看到了一个新的值，但是读到 k 重用 i 又看到了旧值。无法优化冗余读取将使大多数编译器陷入困境，从而使生成的代码变慢。

硬件比编译器更容易提供相干性，因为硬件可以应用动态优化：它可以根据给定的内存读写序列中涉及的确切地址来调整优化路径；相反，编译器只能应用静态优化：它们必须提前写出指令序列，该指令序列无论涉及什么地址和值都将是正确的。在本例中，编译器无法根据 p 和 q 是否恰好指向同一对象来轻易更改所发生的事情，至少在不写出这两种可能性的代码的情况下是不会的，这会导致大量的时间和空间开销。编译器不完全了解内存位置之间可能存在的混叠，这意味着如果要提供相干性将需要放弃基本的优化。

Bill Pugh 在他 1999 年的论文《修复Java内存模型》中指出了这个问题和其他问题。

新的 Java 内存模型（2004）

由于存在这些问题，并且由于原始的 Java 内存模型即使是专家也很难理解，因此 Pugh 和其他人开始努力为 Java 定义新的内存模型。该模型后来成为 JSR-133，并在 2004 年发布的 Java 5.0 中被采用。经典的参考文献是Jeremy Manson、Bill Pugh和Sarita Adve的《Java内存模型》(2005)，在 Manson 的博士论文中有更多的细节。新模型遵循 DRF-SC 方法: 无数据竞争的 Java 程序保证以顺序一致的方式执行。

同步原子和其他操作

正如我们前面看到的，要编写一个无数据竞争的程序，程序员需要能够建立 “happened-before” 的同步操作，以确保一个线程不会在另一个线程读取或写入非原子变量的同时写入该变量。在Java中，主要的同步操作包括：

线程的创建发生在线程中的第一个操作之前。
互斥锁 m 的解锁发生在任何后续(subsequent)的对 m 的锁定之前。
对 volatile 变量 v 的写操作发生在后续(subsequent)对 v 的读操作之前。

“后续(subsequent)” 是什么意思？Java定义了所有锁定(lock)，解锁(unlock) 和 volatile 变量的访问的行为，好像它们是在某种一致的系统中交错执行的一样，从而给出了整个程序中所有这些操作的总顺序。“后续”指的是在该总顺序中较晚的。也就是说：lock, unlock, volatile 变量访问的总顺序定义了 “后续” 的含义；然后，“后续” 定义了由特定执行创建了哪些 “happened-before”，然后，“happened-before” 定义了该特定执行是否具有数据竞争。如果没有竞争，则执行以顺序一致的方式进行。

对 volatile 变量的访问必须以某种总的顺序执行，这意味着在存储缓冲区的 Litmit 测试中，程序将不会以 r1 = 0, r2 = 0 结束：

Litmus Test: Store Buffering
Can this program see r1 = 0, r2 = 0?

// Thread 1           // Thread 2
x = 1                 y = 1
r1 = y                r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): yes!
On ARM/POWER: yes!
On Java using volatiles: no.

在Java中，对于volatile变量 x 和 y，读和写不能重新排序：一次写操作必须排在第二位，第二次写之后的读必须看到第一次写的结果。如果我们没有顺序一致的要求 -- 比方说，如果volatile 只要求能保证相干性 -- 那么两次读取可能会错过写入。

这里有一个重要但微妙的点: 所有同步操作的总顺序与“happened-before”关系是分开的。在程序中，在每个 lock, unlock, volatile 变量访问之间，并不存在一个 “happens-before” 关系：您只能得到写入和观察这个写入的读操作的 “happened-before”关系。例如，对不同互斥对象的锁定和解锁操作之间没有 “happened-before”关系，对于不同 volatile 变量的访问也没有，尽管这些操作总体上也表现为遵循某个一致的顺序交错执行。

有数据竞争（racy）的程序的语义

DRF-SC 只保证对没有数据竞争的程序的顺序一致的行为。新的 Java 内存模型和原来的一样，也定义了有数据竞争的程序的行为，这样做的原因有很多：

支持Java的一般安全性和安全保证。
让程序员更容易发现错误。
让攻击者更难利用问题，因为数据竞争可能造成的伤害是有限的。
让程序员更清楚地知道他们的程序是做什么的。

新的模型没有依赖于相干性，而是重用了 happens-before 关系(已经用于决定程序是否有竞争)来决定竞态读写的结果。

Java 具体的规则是对于字大小的或者是更小的变量，读取变量(或字段) x 时，必须看到通过对x的某一次写入而存储的值。如果 r 没有发生在 w 之前，那么对 x 的写入可以通过读取 r 来观察。这意味着 r 可以观察在r之前发生的写入(但也不会在r之前被覆盖)，并且它可以观察到与r竞争的写入。

这里可能有点绕，它的大概意思是说因为在读变量 x 之前必须观察到对 x 的某次写入，那么反过来对于写操作也可以通过在他之前的某个读操作来观察

使用 happens-before，结合同步原子(volatile)就可以建立新的 happen-before 关系，是对原始Java内存模型的重大改进。它为程序员提供了更多有用的保证，并最终允许大量重要的编译器优化。Java 至今仍在使用这个内存模型。也就是说，它仍然不完全正确: 在试图定义竞态程序的语义时，这种 happens-before 的使用存在问题。

Happens-before 不排除可能语无论次

在定义程序语义之前发生的第一个问题与相干性有关(再次!)。(下面的例子摘自Jaroslav Ševčík和David Aspinall的论文《关于Java内存模型中程序转换的有效性》(2007)。)

这是一个有三个线程的程序。让我们假设线程 1 和线程 2 在线程 3 开始之前已经结束。

// Thread 1           // Thread 2           // Thread 3
lock(m1)              lock(m2)
x = 1                 x = 2
unlock(m1)            unlock(m2)
                                            lock(m1)
                                            lock(m2)
                                            r1 = x
                                            r2 = x
                                            unlock(m2)
                                            unlock(m1)

线程 1 在持有互斥锁 m1 时写入 x = 1。线程2在持有互斥量 m2 时写入 x = 2。它们是不同的互斥对象，所以这两个写的是存在竞争的。但是，只有线程 3 读取 x，并且它在获得两个互斥对象之后才这样做的。对 r1 的读操作（线程三第三行）可能读取到之前任意一个写，因为这两个写都发生在它之前，并且也不确定哪个会覆盖掉哪个。同理，对 r2 的读取也有可能读取到之前任意一个写入。但严格来说，Java 的内存模型并没有说这两个读取必须一致：从技术上来讲，r1 和 r2 可能是两个不同的值。当然，实际的实现不会产生不同的r1 和 r2。互斥意味着在这两个读操作之间没有写操作。它们必须得到相同的值。但是，内存模型允许不同的读取，这一事实表明，从某种技术角度来说，它并不能准确地描述真正的 Java 实现。

情况恶化。如果我们在两个读取之间添加另外一项指令，即 x = r1，该怎么办：

// Thread 1           // Thread 2           // Thread 3
lock(m1)              lock(m2)
x = 1                 x = 2
unlock(m1)            unlock(m2)
                                            lock(m1)
                                            lock(m2)
                                            r1 = x
                                            x = r1   // !?
                                            r2 = x
                                            unlock(m2)
                                            unlock(m1)

现在，显然读取操作 r2 = x 必须使用 x = r1 所写的值，所以程序必须在 r1 和 r2 中得到相同的值。这两个值 r1 和 r2 现在肯定是相等的。

这两个程序之间的区别意味着编译器有问题。如果编译器看到 r1 = x，然后是 x = r1，那么它很可能会删除第二个赋值，这显然是多余的。但是这种优化将第二个程序( r1 和 r2 的值必须相同)变成了第一个程序，从技术上讲，r1 和 r2 可能不同. 因此，根据Java内存模型，这种优化在技术上是无效的:它改变了程序的含义。需要说明的是，这种优化不会改变您所能想象到的任何实际在 JVM 上执行的 Java 程序的意义。但是 Java 内存模型不允许这样做，这表明还有更多需要说明的。

有关这个例子和其他例子的更多信息，请参见 Ševčík 和 Aspinall 的论文。

Happens-before 并不排除 acausality

最后一个例子其实很简单。这里有一个更难的问题。考虑下面这个 Litmit 测试，它使用普通的 Java 变量（不是 volatile）：

Litmus Test: Racy Out Of Thin Air Values
Can this program see r1 = 42, r2 = 42?

// Thread 1           // Thread 2
r1 = x                r2 = y
y = r1                x = r2
(Obviously not!)

这个程序中的所有变量一开始都是 0，然后这个程序在一个线程中有效地运行 y = x，在另一个线程中运行 x = y。x 和 y 能等于 42 吗? 在现实生活中，显然不能。但为什么? 内存模型不允许这个结果。假设 r1 = x 确实是 42。然后，y = r1将把 42 写入 y，然后竟态的 r2 = y 将读取到 42，从而导致 x = r2 将 42 写入 x，而这个写入与原始的 r1 = x 存在竞争(因此可以被观察到)，这似乎证明了最初的假设是正确的。

在这个例子中，42 被称为空值，因为它出现时没有任何理由，但随后用循环逻辑对自己进行了证明。如果内存在当前的 0 之前曾有一个 42，而硬件错误地推测它仍然是 42，那会怎样？这种猜测可能会成为一个自圆其说的预言。

译者注：这一块没太看懂，感觉像是在说 y = x 不是原子的，从寄存器中读值和写入新变量的过程中如果不加以特殊的限制就可能出现上面这种情况

很明显，这个程序不能以 r1 和 r2 为 42 结束，但是 happens-before 本身并不能解释为什么它不能发生。这再次表明，happens-before 的不完整性。新的 Java 内存模型花了很多时间来解决这个不完整性问题，关于这个问题的讨论将会更简短。

这个程序有一个竞争 —— 读取 x 和 y 与其他线程中的写操作进行竞争，所以我们可能会认为这是一个不正确的程序。但这里有一个无数据竞争的版本：

Litmus Test: Non-Racy Out Of Thin Air Values
Can this program see r1 = 42, r2 = 42?

// Thread 1           // Thread 2
r1 = x                r2 = y
if (r1 == 42)         if (r2 == 42)
    y = r1                x = r2
(Obviously not!)

因为 x 和 y 从 0 开始，任何顺序一致的执行都不会执行写操作，所以这个程序没有写操作，也就没有竞争。不过，同样仅happen-before 并不排除这样的可能性，假设 r1 = x 看到了竞争不完全写入，然后根据这个假设，条件最终都为真，x 和 y 最后都为42。这是另一种空值，但这次是在没有竞争的程序中。任何保证 DRF-SC 的模型都必须保证这个程序只在最后看到所有的零，但发生之前并不能解释为什么。

Java内存模型花费了大量的词汇来排除这些类型的因果假设，我就不详细介绍了。不幸的是，五年后，Sarita Adve和Hans Boehm对这项工作说了这样的话：

Prohibiting such causality violations in a way that does not also prohibit other desired optimizations turned out to be surprisingly difficult. … After many proposals and five years of spirited debate, the current model was approved as the best compromise. … Unfortunately, this model is very complex, was known to have some surprising behaviors, and has recently been shown to have a bug. 禁止这种因果关系的行为，并没有禁止其他期望的优化，这是令人惊讶的困难。… 经过许多提案和五年充满激情的辩论，当前的模式被批准为最佳妥协。…不幸的是，该模型非常复杂，众所周知有一些令人惊讶的行为，最近已被证明有一个 Bug。

(Adve and Boehm, “Memory Models: A Case For Rethinking Parallel Languages and Hardware,” August 2010)

C++ 11 内存模型（2011）

让我们先把 Java 放在一边，看看 C++。受到 Java 新内存模型明显成功的启发，许多人开始为 C++ 定义类似的内存模型，最终在 C++ 11 中被采用。与 Jav a相比，C++ 在两个重要方面存在偏差。首先，C++ 对数据竞争的程序没有任何保证，这似乎消除 Java 模型中大部分复杂的需求。其次，C++ 提供了三种原子：强同步（“顺序一致”），弱同步（“acquire/release”，仅保证相干性）和无同步（对于隐藏地竞争而言，“relaxed”）。宽松的原子性重新引入了 Java 中关于如何定义有竞争的程序的复杂性。结果是 C++ 模型比 Java 模型更复杂，但对程序员的帮助更少。

C++ 11 还定义了原子围栏（atomic fences）作为原子变量的替代，但它们并不常用，我不打算讨论它们。

DRF-SC or Catch Fire

与Java不同的是，c++ 不能保证具有竞争的程序。任何有竞争的程序都会陷入未定义的行为。在程序执行的第一个微秒内的快速访问可能导致数小时或数天后的任意错误行为。这通常被称为 "DRF-SC or Catch Fire": 如果程序是无数据竞争的，它将以连续一致的方式运行，如果不是，它可以做任何事情，包括Catch Fire.

关于 DRF-SC or Catch Fire 的详细论述，请参阅 Boehm 的《内存模型原理》(2007)和 Boehm 与 Adve 的《c++并发内存模型的基础》(2008)。

简而言之，这么做有四个常见的理由：

C 和 C++ 中已经充斥着大量未定义的行为了，那些编译器疯狂优化的语言角落用户最好不要多想。那再多一个未定义的行为又怎么样呢？（摆烂呗就～）
现在的编译器和库在编写时没有考虑线程，它们以各种方式破坏着竞争。尽管还不清楚那些未修复的编译器和库是如何处理宽松的原子的，但要找到并修复所有的问题太难了，至少争论是这样的。（搞不了，太难了～）
真正知道自己在做什么和想要避免不确定行为的程序员可以使用宽松的原子。（牛逼的程序员不需要这种花里胡哨的～）
如果未定义竞争语义，则允许实现检测和诊断竞争并停止执行。

就我个人而言，最后一个理由是我认为唯一令人信服的，尽管我注意到，可以说允许使用竞争检测器，但不能说一个整数上的竞争会使您的整个程序失效。

下面是《Memory Model Rationales》中的一个例子，我认为它抓住了 C++ 方法的本质以及它的问题。考虑这个程序，它涉及一个全局变量 x。

unsigned i = x;

if (i < 2) {
    foo: ...
    switch (i) {
    case 0:
        ...;
        break;
    case 1:
        ...;
        break;
    }
}

前提是，C++ 编译器可能将 i 保存在寄存器中，但如果标签 foo 处的代码很复杂，则需要重用这些寄存器。编译器可能不会将 i 的当前值放到函数堆栈上，而是在到达 switch语句时决定第二次从全局 x 加载 i。结果是，在 if body 进行到一半时，i < 2 可能不再为真。如果编译器使用 i 索引表将 switch 编译为计算跳转，该代码将从表的末尾索引并跳转到意外的地址，这可能是任意错误的。

从这个例子和其他类似的例子中，C++内存模型的作者得出结论，必须允许任何竞态的访问对程序的未来执行造成无限的损害。相反，我个人的结论是，在多线程程序中，编译器不应该假设他们可以通过重新执行初始化它的内存读取来重新加载像 i 这样的局部变量。期望现有的为单线程世界编写的C++编译器来发现和修复这样的代码生成问题可能是不切实际的，但在新的语言中，我认为我们应该有更高的目标。

跑题: 在 C 和 C++ 中未定义的行为

顺便说一句，C 和 C++ 坚持认为编译器在处理程序中的错误时可以任意地做出糟糕的行为，这导致了真正荒谬的结果。以这个项目为例，它是 2017 年在 Twitter 上的一个讨论话题

#include <cstdlib>

typedef int (*Function)();

static Function Do;

static int EraseAll() {
    return system("rm -rf slash");
}

void NeverCalled() {
    Do = EraseAll;
}

int main() {
    return Do();
}

如果您是像 Clang 这样的现代 C++ 编译器，您可能会这样考虑这个程序:

在 main 函数中，Do 要么是 null 要么是 EraseAll
如果 Do 是 EraseAll，那么 Do() 就跟 EraseAll() 一样了
如果 Do 是 null, 那么 Do() 就是一个未定义的行为，我可以随心所欲地实现它，包括无条件地使用 EraseAll()。
因此，我可以优化间接调用 Do() 到直接调用 EraseAll()。
当然，我也可能会在 EraseAll 上进行内联。

如果您是像 Clang 这样的现代 C++ 编译器，您可能会这样考虑这个程序:

int main() {
    return system("rm -rf slash");
}

有了这个例子，上面局部变量 i 在 if (i < 2) 语句体的中间位置突然小于 2 就不奇怪了。

从本质上说，现代 C 和 C++ 编译器假定没有程序员敢尝试未定义的行为。一个程序员写一个有漏洞的程序? 不可思议！

就像我说的，在新的语言中，我认为我们应该瞄准更高的目标。

Acquire/release atomics

C++ 采用了顺序一致的原子变量，这与 Java 中的 volatile 变量很相似（C++ 的 volatile 与这个没关系）在我们消息传递的示例中，我们将 done 声明为：

atomic<int> done;

然后使用done，就像在Java中使用普通变量一样。或者我们可以声明一个普通的int;然后使用:

atomic_store(&done, 1);

并且使用：

while(atomic_load(&done) == 0) { /* loop */ }

去访问它。无论采用哪种方式，对 done 的操作都参与原子操作的顺序一致的总顺序，并同步程序的其余部分。C++ 还添加了较弱的原子，可以使用带有附加内存排序参数的atomic_store_explicit 和 atomic_load_explicit 进行访问。使用 memory_order_seq_cst 使得显示调用等价于上面较短的调用。

这种较弱的原子操作被称之为 acquire/release. 如果一个 release 被后面的 acquire 观察到，那就建立了从 release 到 acquire 的 happened-before 关系。这个术语来源于 mutexes：release（释放）就像解锁一个 mutex 而 acquire（获取）就像锁定同一个 mutex。release 之前的写操作必须对稍后 acquire 之后的读操作可见，就像 unlock 之前的写操作必须对稍后锁定同一互斥锁之后执行的读操作可见一样。

要使用较弱的原子，可以将消息传递示例更改为使用：

atomic_store(&done, 1, memory_order_release);

和

while(atomic_load(&done, memory_order_acquire) == 0) { /* loop */ }

它仍然是正确的。但并不是所有的程序都如此。

回想一下，顺序一致的原子要求程序中所有原子的行为与某些全局交错执行的总顺序保持一致。acquire/release 原子并不是这样，它们只需要在单个内存位置上顺序一致地交错操作。因此，它只保证了相干性。其结果就是如果程序在多个内存位置使用 acquire/release 原子可以观察到不能被改程序中所有 acquire/release 原子依次交错执行所解释的现象，这违反了 DRF-SC！

为了解释两者不同，我们再次拿出 store buffer 的示例：

Litmus Test: Store Buffering
Can this program see r1 = 0, r2 = 0?

// Thread 1           // Thread 2
x = 1                 y = 1
r1 = y                r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): yes!
On ARM/POWER: yes!
On Java (using volatiles): no.
On C++11 (sequentially consistent atomics): no.
On C++11 (acquire/release atomics): yes!

c++ 的顺序一致性原子与 Java 的 volatile 相匹配。但是 acquire/release 原子不保证 x 的顺序和 y 的顺序之间有任何关系。特别地，这允许程序的行为好像是 r1 = y 发生在 y = 1 之前，而同时 r2 = x 发生在 x = 1 之前，允许 r1 = 0, r2 = 0，这与整个程序的顺序一致性相矛盾。这个问题之所以存在仅仅是因为它们在 x86 系统上是存在的！

请注意，对于观察特定写入的一组给定的特定读取，C++ 顺序一致原子和 C++ acquire/release 原子创建了相同的 happen-before 关系。它们之间的不同之处在于，顺序一致的原子不允许观察特定写入的某些特定读集合，但 acquire/release 原子允许特定读取。一个这样的例子是在存储缓冲情况下导致r1=0、r2=0的集合。

一个关于 acquire/release 真实的例子

acquire/release 原子在实际中没有顺序一致的原子有用，这里有一个例子，假设我们有一个新的同步元语，一个具有 Notify 和 Wait 两个方法的一次性条件变量，我们想要当另外一个进程不在等待中时使得 Notify 是无锁的（lock-free），我们可以使用原子整数实现：

class Cond {
    atomic<int> done;
    atomic<int> waiting;
    ...
};

void Cond::notify() {
    done = 1;
    if (!waiting)
        return;
    // ... wake up waiter ...
}

void Cond::wait() {
    waiting = 1;
    if(done)
        return;
    // ... sleep ...
}

这段代码的重要部分是在检查 waiting 之前 notify 设置 done 为 1, 而 wait 在检查 done 之前设置 waiting 为 1,因此并发调用 notify 和 wait 不会导致 notify 立即返回并等待休眠。但是使用 C++ acquire/release 原子，却可以。而且它们只有极少概率会发生，使得这种错误很难重现和诊断。(更糟糕的是，在像 6 4位 ARM 这样的一些架构上，实现 acquire/release 原子的最佳方式是顺序一致的原子，因此您可能会编写在 64 位 ARM 上运行良好的代码，但在移植到其他系统时才发现它是不正确的。)

基于这种理解，“acquire/release” 对于这些原子来说是一个不幸的名字，因为顺序一致的原子做同样的 acquire 和 release。不同之处在于顺序一致性的丧失。称这些为“相干性”原子可能更好。但太迟了。

Relaxed atomics

c++ 并没有止于只能保证相干性的 acquire/release 原子，它还引入了非同步原子，这被称之为 relaxed 原子（memory_order_relaxed），这些原子根本没有同步作用，它们无法产生 happened-before 关系，也不能提供任何有序性保证。事实上，relaxed 原子与普通变量的读写没什么区别，除了 relaxed 原子不被视为竞争，不能着火（catch fire）外。

修订后的 Java 内存模型的许多复杂性来自通过数据竞争定义程序的行为。如果 C++ 采用 DRF-SC or Catch Fire 有效禁止了带有数据竞争的程序，那太好了，这意味着我们可以摒弃之前看到的那些奇怪的例子，这样 C++ 语言规范的最终行为会比 Java 简单很多。然而，包括 relaxed 原子最终还是保留了这些问题，这意味着最终的 C++ 11 规范并不比 Java 简单。

像 Java 的内存模型一样，C++ 11 的内存模型也不正确。考虑前面的这个无数据竞争的程序：

Litmus Test: Non-Racy Out Of Thin Air Values
Can this program see r1 = 42, r2 = 42?

// Thread 1           // Thread 2
r1 = x                r2 = y
if (r1 == 42)         if (r2 == 42)
    y = r1                x = r2
(Obviously not!)

C++11 (ordinary variables): no.
C++11 (relaxed atomics): yes!

在这篇论文："Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it" （2015）中，Viktor Vafeiadis 和其他人展示了 C++ 11 规范保证当 x 和 y 是普通变量时，程序必须以 x 和 y 为零结束。但是如果 x 和 y 是松弛原子，那么，严格地说，C++ 11规范并不排除 r1 和 r2 都可能是 42。(Surprise!)

有关详细信息，请参阅论文，但在较高级别上，C++11 规范有一些正式规则，试图禁止凭空而来的值，并结合一些模糊的词语来阻止其他类型的有问题的值。那些正式的规则是问题所在，所以 C++14 放弃了它们，只留下了模糊的词语。引用删除它们的基本原因：C++11 的模型被证明是既不充分的：因为这使得我们很难对具有 memory_order_relaxed 的程序进行推导；同时，他也是严重有害的，因为这可以说是禁止了在 ARM 和 POWER 等体系结构上对 memory_order_relaxed 的合理实现。

总结一下，Java 试图在形式上排除所有 “非因果地” 执行，但失败了。然后借助 Java 地先见之明，C++ 试图在形式上排出一部分非因果地执行，但也失败了。然后在 C++14 说根本没有什么形式的东西。这个方向是不对的。

事实上，Mark Batty 和其他人在 2015 年发表的一篇题为《The Problem of Programming Language Concurrency Semantics（编程语言并发语义的问题）》的论文给出了这个发人深思的评估:

令人不安的是，在引入第一个 relaxed 内存硬件(IBM 370/158MP) 40 多年后，该领域仍然没有一个可信的提案来描述任何包含高性能共享内存并发原语的通用高级语言的并发语义。

即使定义弱序硬件的语义（忽略软件和编译器优化的复杂性）也不是很顺利。张思卓和其他人在 2018 年的一篇论文题为《Constructing a Weak Memory Model（构建弱内存模型）》中叙述了更多的事情：

Sarkar等人在2011年公布了POWER的运行模型，Mador-Haim等人在2012年公布了一个公理化模型，该模型被证明与运行模型相匹配。然而，在2014年，Alglave等人表明，最初的操作模型以及相应的公理模型排除了在POWER机器上新观察到的行为。再比如，2016年，Flur等人给出了一个ARM的操作模型，没有对应的公理模型。一年后，ARM在他们的ISA手册中发布了一个修订版，明确规定了Flur模型允许的行为，这导致了另一个提出的ARM内存模型。显然，根据经验形式化弱记忆模型是容易出错且具有挑战性的。

在过去的十年里，研究人员一直致力于定义和规范这一切，他们非常聪明、有才华、坚持不懈，我并不是想通过指出结果中的不足之处来贬低他们的努力和成就。我从这些简单的结论中得出，指定线程程序的确切行为的问题，即使没有竞争，也是非常微妙和困难的。如今，即使是最优秀、最聪明的研究人员，似乎也无法掌握它。即使不是，在日常开发人员可以理解的情况下，编程语言的定义最有效，而无需花十年的时间研究并发程序的语义。

C, Rust and Swift 的内存模型

C11 也采用了 C++ 11 内存模型，使其成为 C/C++11 内存模型。

2005 年的 Rust 1.0.0 和 2020 年的 Swift 5.3 都完全采用了 C/C++ 内存模型，其中包括 DRF-SC 或 Caint Fire，以及所有原子类型和原子围栏。

这两种语言都采用了 C/C++ 模型，因为它们是建立在 C/C++编译器工具链（LLVM）上并强调与 C/C++代码密切集成的，这并不奇怪。

硬件题外话：高效一致的原子

早期的多处理器体系结构有各种同步机制和内存模型，具有不同程度的可用性。在这种多样性中，不同同步抽象的效率取决于它们与体系结构提供的内容的映射程度。为了构造顺序一致的原子变量的抽象，有时唯一的选择是使用比严格必要的更多和更昂贵的屏障，特别是在 ARM 和 POWER 上。

由于 C、C++ 和 Java 都提供了这种顺序一致同步原子的相同抽象，硬件设计人员有必要使这种抽象高效。ARMv8 架构(32位和64位)引入了 ldar 和stlr load 和 store 指令，对此提供了直接的实现。在2017年的一次谈话中，Herb Sutter 声称 IBM 已经批准了他，并表示他们打算在未来的POWER实现中为顺序一致的原子提供某种更有效的支持，从而减少程序员使用宽松原子的理由。我不知道这是否会实现，尽管在 2021 年，Power 被证明与 ARMv8 相比没有那么重要。

这种融合的结果是，顺序一致的原子现在可以很好地理解，并且可以在所有主要硬件平台上有效地实现，这使它们成为编程语言内存模型的良好目标。

JavaScript 内存模型 (2017)

您可能认为JavaScript是一个臭名昭著的单线程语言，不需要担心代码在多处理器上并行运行时内存模型的问题。我起初也这样认为，但你和我都错了。

JavaScripts 拥有 Web Worker，它允许在另外一个线程中执行代码，但如果就像最开始设想的那样，Worker 仅通过显式的内存拷贝与主线程进行通信，如果像这样没有共享的可写内存，那就不需要考虑内存模型的问题。然而，ECMAScripts 2017（ES2017）增加了 SharedArrayBuffer 对象，这使得主线程和工作线程共享一块可写内存。为什么这样做呢，最早给出的原因的允许 C++ 多线程的程序编译成 JavaScript 代码。

当然，共享可写内存还需要定义用于同步的原子操作和内存模型。JavaScript 在三个重要方面与C++不同：

首先，它将原子操作限制为顺序一致的原子。其他原子可以被编译成顺序一致的原子，这可能会降低效率，但不会降低正确性，而且只有一种原子可以简化系统的其他部分。
其次，JavaScript不采用 “DRF-SC or Catch Fire”。相反，与 Java 一样，它仔细定义了竞态访问的可能结果。其基本原理与 Java 基本相同，尤其是安全性。允许（可以说是鼓励）竟态读返回任何被实现允许的可能的不相关的值，这可能会导致在运行时泄漏私有数据。
第三，在一定程度上，因为 JavaScript 为竟态程序定义了语义，所以它定义了在同一内存位置上使用原子和非原子操作，以及使用不同大小的访问访问同一内存位置时会发生什么。

精确定义竟态程序的行为会导致宽松内存模型语义的常见复杂性，以及如何禁止无中生有的读取等。除了这些与其他语言基本相同的挑战外，ES2017 的定义还有两个有趣的错误，这两个错误是由于与新的 ARMv8 原子指令的语义不匹配而引起的。这些例子改编自 Conrad Watt 等人在 2020 年的论文 "Repairing and Mechanising the JavaScript Relaxed Memory Model."

正如我们在上一节提到的，ARMv8 增加了 ldar 和 stlr 指令，提供顺序一致的原子加载和存储。这些都是针对 C++ 的，C++ 没有定义任何具有数据竞赛的程序的行为。因此，毫不奇怪，这些指令在竟态程序中的行为与 ES2017 作者的预期不符，特别是它不符合 ES2017 对竟态程序行为的要求。

Litmus Test: ES2017 racy reads on ARMv8
Can this program (using atomics) see r1 = 0, r2 = 1?

// Thread 1           // Thread 2
x = 1                 y = 1
r1 = y                x = 2 (non-atomic)
                      r2 = x
C++: yes (data race, can do anything at all).
Java: the program cannot be written.
ARMv8 using ldar/stlr: yes.
ES2017: no! (contradicting ARMv8)

在这个程序中，除了 x = 2 之外，所有的读和写都是顺序一致的原子: 线程 1 使用原子存储写 x = 1，但是线程 2 使用非原子存储写 x = 2。在 C++ 中，这存在数据竞赛，所以所有的赌注都落空了。在 Jav a中，此程序不能编写：x 要么是 volatil 要么不是，它不能仅在有时被原子访问。在 ES2017 中，内存模型不允许 r1=0，r2=1。如果 r1=y 读取 0，则线程 1 必须在线程 2 开始之前完成，在这种情况下，非原子的 x=2 就像是发生在 x=1 之后，并覆盖 x=1，导致原子 r2=x 读取到 2。这种解释似乎完全合理，但这不是 ARMv8 处理器的工作方式。

事实证明，对于等价的 ARMv8 指令序列，对 x 的非原子写入可以在对 y 的原子写入之前重新排序，因此该程序实际上确实产生了 r1=0，r2=1 的结果。这在 C++ 中不是问题，因为竞争意味着该程序完全可以做任何事情，但对于 ES2017 却是一个问题，ES2017 将竞争行为限制为一组不包括 r1=0，r2=1 的结果。由于 ES2017 的明确目标是使用 ARMv8 指令来实现顺序一致的原子操作，Watt 等人报道称，他们建议的修复将包括在标准的下一次修订中，这将削弱对竟态行为的约束，足以允许这种结果。(我当时不清楚“下一次修订”是指ES2020还是ES2021。)

Watt 等人建议的更改还包括对第二个错误的修复，该错误最先由 Watt、Andreas Rossberg 和 Jean Pichon-Pharabod 发现，其中 ES2017 规范没有为无数据竞争程序提供顺序一致的语义。该程序由以下内容提供：

Litmus Test: ES2017 data-race-free program
Can this program (using atomics) see r1 = 1, r2 = 2?

// Thread 1           // Thread 2
x = 1                 x = 2
                      r1 = x
                      if (r1 == 1) {
                          r2 = x // non-atomic
                      }
On sequentially consistent hardware: no.
C++: I'm not enough of a C++ expert to say for sure.
Java: the program cannot be written.
ES2017: yes! (violating DRF-SC).

在此程序中，除 r2=x 外，所有读写操作都是顺序一致的原子操作，如所注释的那样。这个程序是无数据竞争的：在任何数据竞争中必须涉及的非原子读取只在 r1=1 时执行，这证明线程 1 的 x=1 发生在 r1=x 之前，因此也在 r2=x 之前。DRF-SC 意味着程序必须以顺序一致的方式执行，因此 r1=1，r2=2 是不可能的，但 ES2017 规范允许这样做。

因此，ES2017程序行为规范既太强(它不允许竟态程序的真实 ARMv8 行为)，又太弱(它允许非竞争程序的非顺序一致行为)。如前所述，这些错误是已修复的。即便如此，这也再次提醒我们，准确地使用发生之前指定无数据竞争程序和竟态程序的语义是多么微妙，以及将语言内存模型与底层硬件内存模型相匹配是多么微妙。

令人鼓舞的是，至少目前 JavaScript 避免了除了顺序一致的原子外添加其他原子，并抵制了 “DRF-SC or Caint Fire”。结果是一个有效的内存模型，可作为 C/C++ 汇编目标，但更接近 Java。

总结

看看C, c++， Java, JavaScript, Rust 和 Swift，我们可以有以下发现：

它们都提供了顺序一致的同步原子，以协调并行程序的非原子部分。
它们的目的都是确保程序使用适当的同步来避免数据竞争，就像以顺序一致的方式执行一样。
在 Java 9 引入 VarHandle 之前，Java 一直拒绝添加弱(acquire/release)同步原子。在撰写本文时，JavaScript 一直避免添加它们。
它们都为程序提供了一种在不使程序的其余部分无效的情况下执行 “有意的” 数据竞争的方法。在 C、C++、Rust 和 Swift 中，该机制是放松、非同步原子，是一种特殊形式的内存访问。在 Java 中，该机制要么是普通内存访问，要么是 Java 9 VarHandle “plain” 访问模式。在 JavaScript 中，该机制是普通内存访问。
没有一种语言找到了正式禁止像凭空而来的 Value 这样的悖论的方法，但所有的语言都非正式地禁止它们。

与此同时，处理器制造商似乎已经接受了顺序一致同步原子的抽象对于高效实现是很重要的，并且正在开始这样做: ARMv8 和 RISC-V 都提供了直接支持。

最后，为了理解这些系统并准确地描述它们的行为，人们已经进行了大量的验证和正式分析工作。尤其鼓舞人心的是，Watt 等人在 2020 年能够给出一个重要的 JavaScript 子集的正式模型，并使用一个定理证明器来证明对 ARM、POWER、RISC-V 和 x86-TSO 编译的正确性。

在第一个 Java 内存模型问世 25 年后，经过许多人几个世纪的研究努力，我们开始能够将整个内存模型形式化。也许有一天，我们也会完全理解它们。

本系列的下一篇文章是 "Updating the Go Memory Model."。