Memory Models

[CookiePieWw]

https://research.swtch.com/mm

[CookiePieWw]

内存模型指硬件和编程语言在多线程场景下对内存和共享数据取用顺序的保证。

硬件中由于缓存/乱序执行等，可能对共享数据有不同的保证。

Sequentially Consistent

Sequentially Consistent 内存模型保证在每个线程中指令执行的顺序和在程序中指定的顺序一致。SC 内存模型的机器可以视为下图表示的机器：

不同的内存模型可以用 Litmus Test 来区分：

// Litmus Test: Message Passing
// Can this program see r1 = 1, r2 = 0?
// Thread 1
x = 1
y = 1
// Thread 2
r1 = y
r2 = x
// On sequentially consistent hardware: no.

x86-TSO

x86-TSO 模型为每个线程加入了一个 local write buffer，但所有线程对共享变量写入到内存的顺序的意见是一致的：

// Litmus Test: Write Queue (also called Store Buffer)
// Can this program see r1 = 0, r2 = 0?
// Thread 1 
x = 1 
r1 = y
// Thread 2
y = 1
r2 = x
// On sequentially consistent hardware: no.
// On x86 (or other TSO): yes!

BTW，2007-08 年的 white paper/spec 所给出的 TSO-CC 和 revision 的版本与 x86 实际的硬件表现不一致 qaq，详见文中的 The Path to x86-TSO 章节。

ARM/POWER Relaxed Model

ARM/POWER 架构的内存模型是一个大型破坏魔法（大雾

Relaxed Model 对不相关的共享变量的写入顺序不提供任何保证，但对于同一个变量的写入顺序观测是一致的。（文中的 coherence 指对于同一个变量的写入顺序观测，而不是常识中多层级共享变量的一致性保证）

// 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
x = 1
// Thread 2
x = 2 
// Thread 3
r1 = x 
r2 = x 
// Thread 4
r3 = x
r4 = x
// On sequentially consistent hardware: no.
// On x86 (or other TSO): no.
// On ARM/POWER: no.

DRF-SC

不同的架构有不同的内存模型，但它们提供一个基本的保证，即 data-race-free sequential-consistency，或者 DRF-SC。

[CookiePieWw]

编译器可能对指令进行重排以进行优化，这将导致另一些变化。

// 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
x = 1
// Thread 2
x = 2 
// Thread 3
r1 = x 
r2 = x 
// Thread 4
r3 = 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!

例如在上述 Litmus Test 中，编译器可能对 Thread 4 的读写进行重排，从而获得不同的结果。

Original Java Memory Model (1996)

The first edition of the Java Language Specification, 1996

1996 年 Java 首先尝试规范多线程程序的执行：定义内存模型和发生 data race 时的行为、引入互斥锁和 volatile 变量。

但最初的 volatile 变量并不保证 sync，因此会出现：

// Litmus Test: Message Passing in Java
// Can this program print 0?
int x;
volatile int done;
// Thread 1
x = 1;
done = 1;
// Thread 2
while (done == 0) { /* loop */ }
print(x);
// On Java (1996): Yes!

这里 x 和 done 的写入和读取顺序可能发生重排。

同时 Java 的内存模型保证了变量的 coherence（同一变量在不同线程中对于写入顺序的观测一致），这将禁止基本的编译器优化。

New Java Memory Model (2004)

JSR-133 adopted in Java 5.0, 2004

2004 年的新 Java 内存模型遵循 DRF-SC。

相较于 1996 年不能 sync 的 volatile，新内存模型提供以下的 sync 操作：

• 线程的创建在执行第一条指令之前
• 互斥锁的解锁在之后的任意锁定之前
• volatile 变量的写在之后的任意读之前

Litmus Test: Store Buffering
Can this program see r1 = 0, r2 = 0?
// Thread 1
x = 1
r1 = y
// Thread 2
y = 1
r2 = x
On sequentially consistent hardware: no.
On x86 (or other TSO): yes!
On ARM/POWER: yes!
On Java using volatiles: no.

新的内存模型同样定义了 racy program 的行为，但使用的是 happens before 关系而不是 coherence：对于小变量（word-sized or smaller variables），读写之间不发生 race，读可以观察到 happens before 它的写和 race with 它的写。

但使用 happens before 定义 racy program 产生了一些问题。

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

这里内存模型允许观察到 r1 和 r2 有不一样的结果，也就是不保证 coherence。如果在两次读中间加入 x = r1，那么内存模型就不再允许 r1 和 r2 不一致。但这个写入显然是可以优化掉的。因此内存模型和编译器实现之间存在不一致。更多的例子见 On the Validity of Program Transformations in the Java Memory Model, Sevcik and Aspinall, ECOOP'08。

同时，内存模型会导致 Out Of Thin Air Values 的问题

// Litmus Test: Racy Out Of Thin Air Values
// Can this program see r1 = 42, r2 = 42?
// Thread 1
r1 = x
y = r1
// Thread 2
r2 = y
x = r2
// (Obviously not!)

虽然不可能发生这样的情况，但 r1=42 是一个可以自我实现的预言。Java 内存模型为了解决这个问题使用了大量篇幅。

C++11 Memory Model (2011)

C++ 11 的内存模型对 racy program 没有任何保证（引发 ub，被称作 DRF-SC or Catch Fire），它提供了 SC、aquire/release 和 relaxed 三种内存序。

SC 和 Java 的 volatile 是类似的，禁止重排并全局保序；acquire/release 则在 release 和之后的 acquire 之间建立 happens-before 关系；relaxed 只保证相关变量的 race 不是 ub。（ 这部分还是看 cppreference 好一些，见 https://en.cppreference.com/w/cpp/atomic/memory_order）

作者这里批评了 acquire/release 的用处不大，举了一个条件变量无锁实现只能用 SC 而不能用 aquire/release 的例子。

C, Rust and Swift Memory Models

和 C++11 没区别。

Hardware Digression: Efficient Sequentially Consistent Atomics

SC 只能使用 memory barrier 这样的实现，非常昂贵且没有必要。ARMv8 提供了 ldar 和 stlr 这样的硬件指令来加速 SC。

JavaScript Memory Model (2017)

作为单线程的程序，js 本没有必要关注内存模型。但 ECMAScript 2017 添加了 SharedArrayBuffer，允许 web workers 和 主线程共享一块内存区域。（在提案的第一个版本中，这是为了将多线程 cpp 代码编译到 js）