第 10 章 内存模型：难点

本章描述了 OCaml 松弛内存模型的细节。松弛内存模型描述了 OCaml 程序在读取内存位置时允许观察到的值。如果您对 OCaml 中的高级并行编程感兴趣，请查看并行编程章节 9。

本章面向希望从实践者的角度了解 OCaml 内存模型细节的专家。有关 OCaml 内存模型的正式定义、其保证以及编译到硬件内存模型，请查看 2018 年 PLDI 论文 Bounding Data Races in Space and Time。本章中介绍的内存模型是 PLDI 2018 论文中提出的模型的扩展。本章还涵盖了一些论文中未涉及的内存模型的实用方面。

1 为什么弱一致性内存？

我们可以为程序提供的最简单的内存模型是顺序一致性。在顺序一致性下，程序观察到的值可以通过程序中不同域的操作的某种交错来解释。例如，考虑以下具有两个并行执行的域 d1 和 d2 的程序

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = !a * 2 in (r1, r2, r3) let d2 b = b := 0 let main () = let a = ref 1 in let b = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 a b in Printf.printf "r1 = %d, r2 = %d, r3 = %d\n" r1 r2 r3) in d2 b; Domain.join h

引用单元 a 和 b 最初为 1。如果 d2 中对 b 的写入发生在 d1 中对 b 的读取之前，用户可能会观察到 r1 = 2, r2 = 0, r3 = 2。在这里，观察到的行为可以用不同域的操作的交错来解释。

现在让我们假设 a 和 b 是彼此的别名。

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = !a * 2 in (r1, r2, r3) let d2 b = b := 0 let main () = let ab = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 ab ab in assert (not (r1 = 2 && r2 = 0 && r3 = 2))) in d2 ab; Domain.join h

在上面的程序中，变量 ab、a 和 b 指向同一个引用单元。人们期望主函数中的断言永远不会失败。推理是，如果 r2 为 0，则 d2 中的写入发生在 d1 中对 b 的读取之前。鉴于 a 和 b 是别名，d1 中对 a 的第二次读取也应该返回 0。

1.1 编译器优化

令人惊讶的是，由于编译器优化，此断言可能在 OCaml 中失败。OCaml 编译器观察到 d1 中的公共子表达式 !a * 2 并将程序优化为

let d1 a b = let r1 = !a * 2 in let r2 = !b in let r3 = r1 in (* CSE: !a * 2 ==> r1 *) (r1, r2, r3) let d2 b = b := 0 let main () = let ab = ref 1 in let h = Domain.spawn (fun _ -> let r1, r2, r3 = d1 ab ab in assert (not (r1 = 2 && r2 = 0 && r3 = 2))) in d2 ab; Domain.join h

这种优化称为公共子表达式消除 (CSE)。此类优化对于良好的性能是有效且必要的，并且不会更改程序的顺序含义。但是，CSE 破坏了顺序推理。

在上面的优化程序中，即使 d2 中对 b 的写入发生在 d1 中的第一次和第二次读取之间，程序也会为 r3 观察到值 2，导致断言失败。观察到的行为无法通过源程序中不同域的操作的交错来解释。因此，CSE 优化在顺序一致性下被认为是无效的。

解释观察到的行为的一种方法是，好像对域执行的操作被重新排序了。例如，如果 d1 中的第二次和第三次读取被重新排序，

let d1 a b = let r1 = !a * 2 in let r3 = !a * 2 in let r2 = !b in (r1, r2, r3)

那么我们可以解释 d1 返回的观察到的行为 (2,0,2)。

1.2 硬件优化

另一个重新排序的来源是硬件。现代硬件架构具有复杂的多级缓存层次结构。虽然缓存一致性确保对单个内存位置的读写尊重顺序一致性，但对操作不同内存位置的程序的保证要弱得多。考虑以下程序

let a = ref 0 and b = ref 0 let d1 () = a := 1; !b let d2 () = b := 1; !a let main () = let h = Domain.spawn d2 in let r1 = d1 () in let r2 = Domain.join h in assert (not (r1 = 0 && r2 = 0))

在顺序一致性下，我们永远不会期望断言失败。但是，即使在提供比 ARM 更强保证的 x86 上，在 CPU 内核上执行的写入也不会立即发布到所有其他内核。由于 a 和 b 是不同的内存位置，因此对 a 和 b 的读取都可能观察到初始值，从而导致断言失败。

如果允许加载在先前的对不同内存位置的存储之前重新排序，则可以解释此行为。由于现代处理器上的内核存储缓冲区的存在，可能会发生这种重新排序。每个内核实际上都有一个挂起的写入的 FIFO 缓冲区，以避免在写入完成时阻塞的需要。对 a 和 b 的写入可能分别位于运行域 d1 和 d2 的内核 c1 和 c2 的存储缓冲区中。如果写入尚未从缓冲区传播到主内存，则分别在内核 c1 和 c2 上运行的对 b 和 a 的读取将看不到这些写入。

2 数据竞争自由蕴含顺序一致性

OCaml 松弛内存模型的目标是精确描述 OCaml 程序中哪些顺序会被保留。编译器和硬件可以自由地优化程序，只要它们遵守内存模型的顺序保证即可。虽然直接在松弛内存模型下编程很困难，但内存模型也描述了程序仅表现出顺序一致行为的条件。此保证称为数据竞争自由蕴含顺序一致性 (DRF-SC)。在本节中，我们将描述此保证。为此，我们首先需要一些定义。

2.1 内存位置

OCaml 将内存位置分类为原子和非原子位置。引用单元、数组字段和可变记录字段是非原子内存位置。不可变对象是非原子位置，具有初始化写入但没有进一步更新。原子内存位置是使用Atomic模块创建的那些位置。

2.2 发生前关系

让我们假设 OCaml 程序由一个抽象机器执行，该机器一次执行一个动作，在每一步任意选择一个可用的域。我们将动作分为两类：域间和域内。域间动作是可以被其他域上的动作观察到并受其影响的动作。有几个域间动作

另一方面，域内动作既不能被观察到，也不能影响其他域的执行。例如，计算算术表达式、调用函数等。内存模型规范忽略此类域内动作。在后续内容中，我们使用术语“动作”来表示域间动作。

抽象机执行的动作的完全有序列表称为执行轨迹。由于不确定性，给定程序可能存在多个可能的执行轨迹。

对于给定的执行轨迹，我们定义了一个自反的、传递的发生前关系，它捕获 OCaml 程序中动作之间的因果关系。发生前关系定义为满足以下属性的最小传递关系

2.3 数据竞争

在给定的轨迹中，如果两个动作访问相同的非原子位置，至少一个是写入，并且都不是对该位置的初始化写入，则称这两个动作冲突。

如果程序存在一些执行轨迹，其中有两个冲突的动作，并且这两个冲突的访问之间不存在发生前关系，则称该程序存在数据竞争。没有数据竞争的程序称为正确同步的程序。

2.4 DRF-SC

DRF-SC 保证：没有数据竞争的程序只会表现出顺序一致的行为。

DRF-SC 对程序员来说是一个强大的保证。程序员可以使用顺序推理，即通过一个接一个地执行域间动作来推理，以识别他们的程序是否存在数据竞争。特别是，他们不需要考虑第 ‍10.1 节中描述的重新排序，以确定他们的程序是否存在数据竞争。一旦确定某个特定程序没有数据竞争，他们就不需要担心代码中的重新排序。

3 使用 DRF-SC 进行推理

在本节中，我们将查看使用 DRF-SC 进行程序推理的示例。在本节中，我们将使用名称dN的函数来表示与其他域并行执行的域。也就是说，我们假设存在一个main函数，它如下并行运行dN函数

let main () =
  let h1 = Domain.spawn d1 in
  let h2 = Domain.spawn d2 in
  ...
  ignore @@ Domain.join h1;
  ignore @@ Domain.join h2

这是一个存在数据竞争的简单示例

(* 存在数据竞争 *) let r = ref 0 let d1 () = r := 1 let d2 () = !r

r 是一个非原子引用。这两个域争夺访问该引用，而d1是一个写入。由于冲突访问之间不存在发生前关系，因此存在数据竞争。

我们在第 ‍10.1 节中看到的两个程序都存在数据竞争。它们表现出非顺序一致行为也就不足为奇了。

并行访问不相交的数组索引和记录的字段不是数据竞争。例如，

(* 没有数据竞争 *) let a = [| 0; 1 |] let d1 () = a.(0) <- 42 let d2 () = a.(1) <- 42
(* 没有数据竞争 *) type t = { mutable a : int; mutable b : int } let r = {a = 0; b = 1} let d1 () = r.a <- 42 let d2 () = r.b <- 42

不存在数据竞争。

原子位置上的竞争不会导致数据竞争。

(* 没有数据竞争 *) let r = Atomic.make 0 let d1 () = Atomic.set r 1 let d2 () = Atomic.get r

消息传递

原子变量可用于实现域之间的非阻塞通信。

(* 没有数据竞争 *) let msg = ref 0 let flag = Atomic.make false let d1 () = msg := 42; (* a *) Atomic.set flag true (* b *) let d2 () = if Atomic.get flag (* c *) then !msg (* d *) else 0

观察到动作a和d分别对相同的非原子位置msg进行写入和读取，因此它们是冲突的。我们需要确定a和d之间是否存在发生前关系，以证明该程序没有数据竞争。

动作a在程序顺序中先于b，因此，a发生前b。类似地，c发生前d。如果d2观察到原子变量flag为true，则b在发生前顺序中先于c。由于发生前是传递的，因此冲突的动作a和d处于发生前顺序中。如果d2观察到flag为false，则不会执行对msg的读取。因此，在此执行轨迹中不存在冲突访问。因此，该程序没有数据竞争。

消息传递程序的以下修改版本确实存在数据竞争。

(* 存在数据竞争 *) let msg = ref 0 let flag = Atomic.make false let d1 () = msg := 42; (* a *) Atomic.set flag true (* b *) let d2 () = ignore (Atomic.get flag); (* c *) !msg (* d *)

域d2现在无条件地读取非原子引用msg。考虑执行轨迹

Atomic.get flag; (* c *)
!msg; (* d *)
msg := 42; (* a *)
Atomic.set flag true (* b *)

在此轨迹中，d和a是冲突的操作。但它们之间不存在发生前关系。因此，该程序存在数据竞争。

4 局部数据竞争自由

OCaml 的内存模型即使对于存在数据竞争的程序也能提供强保障。它提供了所谓的 *局部数据竞争自由顺序一致性 (LDRF-SC)* 保证。本文档章节不涉及此属性的正式定义。感兴趣的读者可以阅读 2018 年 PLDI 论文 Bounding Data Races in Space and Time。

通俗地说，LDRF-SC 指的是程序中无数据竞争的部分仍然保持顺序一致性。也就是说，即使程序存在数据竞争，那些与存在数据竞争的部分互不相干的部分仍然适合进行顺序推理。

考虑以下代码片段

let snippet () = let c = ref 0 in c := 42; let a = !c in (a, c)

观察到 c 是一个新分配的引用。读取 c 的返回值是否可能不是 42？也就是说，a 是否可能不等于 42？令人惊讶的是，在 C++ 和 Java 内存模型中，答案是肯定的。在 C++ 内存模型中，如果程序存在数据竞争，即使在不相关的部分，语义也是未定义的。如果此代码片段与存在数据竞争的库链接，那么在 C++ 内存模型下，读取可能返回任何值。由于不相关位置上的数据竞争会影响程序行为，因此我们说 C++ 内存模型在空间上是不受限的。

与 C++ 不同，Java 内存模型在空间上是受限的。但 Java 内存模型在时间上是不受限的；未来的数据竞争会影响过去的行为。例如，考虑将此示例转换为 Java。我们假设事先定义了 Class c {int x;} 和一个共享的 *非易失性* 变量 C g。现在，此代码片段可能是包含并行线程的较大程序的一部分

(* Thread 1 *)
C c = new C();
c.x = 42;
a = c.x;
g = c;

(* Thread 2 *)
g.x = 7;

第一个线程中对 c.x 的读取和对 g 的写入是在不同的内存位置上进行的。因此，Java 内存模型允许它们被重新排序。结果，第二个线程中的写入可能发生在读取 c.x 之前，因此，c.x 返回 7。

上述 Java 代码的 OCaml 等价代码是

let g = ref None let snippet () = let c = ref 0 in c := 42; let a = !c in (a, c) let d1 () = let (a,c) = snippet () in g := Some c; a let d2 () = match !g with | None -> () | Some c -> c := 7

观察到 g 和 c 都存在数据竞争。仅考虑 snippet 中的前三条指令

let c = ref 0 in
c := 42;
let a = !c in
...

OCaml 内存模型在空间和时间上都是受限的。这里唯一的内存位置是 c。仅针对此代码片段进行推理，既不存在空间上的数据竞争（对 g 的竞争），也不存在时间上的数据竞争（对 c 的未来竞争）。因此，此代码片段将具有顺序一致的行为，并且 !c 返回的值将是 42。

OCaml 内存模型保证即使对于存在数据竞争的程序，内存安全也能得到保留。虽然存在数据竞争的程序可能会观察到非顺序一致的行为，但它们不会崩溃。

5 内存模型的操作视角

在本节中，我们将描述 OCaml 内存模型的语义。内存模型操作视角的正式定义在 2018 年 PLDI 论文 Bounding Data Races in Space and Time 的第 3 节中给出。本节将借助示例对内存模型进行非正式描述。

给定一个可能包含数据竞争的 OCaml 程序，操作语义会告诉您读取内存位置时可能观察到的值。为简单起见，我们将线程内操作限制为仅访问原子和非原子位置，忽略域生成和连接操作，以及对互斥量的操作。

我们以简单明了的小步操作方式描述 OCaml 内存模型的语义。也就是说，语义由一个抽象机器描述，该机器每次执行一个操作，并在每一步任意选择一个可用的域。这类似于我们之前在第 ‍10.2.2 节中用于描述先行关系的抽象机。

5.1 非原子位置

在语义中，我们将非原子位置建模为从时间戳 t 到值 v 的有限映射。我们将时间戳视为有理数。时间戳是完全有序但稠密的；任何两个时间戳之间都存在一个时间戳。

例如，

a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t8 -> 7]

表示三个非原子位置 a、b 和 c 及其历史。位置 a 在时间戳 t1 和 t2 处分别有两个写入，其值为 1 和 2。当我们写 a: [t1 -> 1; t2 -> 2] 时，我们假设 t1 < t2。我们假设位置初始化时具有一个历史记录，该历史记录在时间戳 0 处有一个条目，该条目映射到初始值。

5.2 域

每个域都配备了一个 *前沿*，它是非原子位置到时间戳的映射。直观地说，每个域的前沿记录了每个非原子位置的最新写入。可能发生过更新的写入，但不能保证可见。

例如，

d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t7]

表示两个域 d1 和 d2 及其前沿。

5.3 非原子访问

现在让我们定义非原子读写语义。假设域 d1 执行对 b 的读取。对于非原子读取，域可以读取该位置历史记录中的任意元素，只要它不早于域前沿中的时间戳即可。在本例中，由于 d1 在 b 处的前沿位于 t3，因此读取可能返回值 3、4 或 5。非原子读取不会更改当前域的前沿。

假设域 d2 将值 10 写入 c (c := 10)。我们为此次写入选择一个新的时间戳 t9，使其晚于 d2 在 c 处的前沿。请注意这里的一个细微差别：此新时间戳可能不晚于历史记录中的所有其他时间戳，而仅仅晚于写入域已知的任何其他写入。因此，t9 可以插入到 c 的历史记录中，方法是 (a) 在 t7 和 t8 之间或 (b) 在 t8 之后。为了讨论，我们选择第一个选项。由于新的写入出现在域 d2 已知对位置 c 的所有写入之后，因此 d2 在 c 处的前沿也会更新。抽象机的新的状态为

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7] (* new write at t9 *)

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9] (* frontier updated at c *)

5.4 原子访问

原子位置不仅包含值，还包含同步信息。我们将原子位置建模为该位置保存的值和前沿的配对。前沿对同步信息进行建模，该信息与对该位置进行操作的线程的前沿合并。这样，一个线程进行的非原子写入可以通过原子位置进行通信，从而为另一个线程所知。

例如，

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

显示了两个原子变量 A 和 B，它们的值分别为 10 和 5，以及它们自己的前沿。我们使用大写变量名来表示原子位置。

在原子读取期间，位置的前沿会合并到执行读取的域的前沿中。例如，假设 d1 读取 B。读取返回 5，并且通过将其与 B 的前沿合并来更新 d1 的前沿，为每个位置选择较晚的时间戳。原子读取之前的抽象机状态为

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t1; b -> t3; c -> t7]
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

原子读取的结果是，抽象机状态更新为

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7] (* frontier updated at a and b *)
d2: [a -> t1; b -> t4; c -> t9]

(* Atomic locations *)
A: 10, [a -> t1; b -> t5; c -> t7]
B: 5,  [a -> t2; b -> t4; c -> t6]

在原子写入期间，原子位置保存的值会被更新。写入域和正在写入的位置的前沿都更新为两个前沿的合并。例如，如果 d2 在当前机器状态下将 20 写入 A，则机器状态将更新为

(* Non-atomic locations *)
a: [t1 -> 1; t2 -> 2]
b: [t3 -> 3; t4 -> 4; t5 -> 5]
c: [t6 -> 5; t7 -> 6; t9 -> 10; t8 -> 7]

(* Domains *)
d1: [a -> t2; b -> t4; c -> t7]
d2: [a -> t1; b -> t5; c -> t9] (* frontier updated at b *)

(* Atomic locations *)
A: 20, [a -> t1; b -> t5; c -> t9] (* value updated. frontier updated at c. *)
B: 5,  [a -> t2; b -> t4; c -> t6]

5.5 使用语义进行推理

让我们回顾前面（第 10.1 节）的一个示例。

let a = ref 0 and b = ref 0 let d1 () = a := 1; !b let d2 () = b := 1; !a let main () = let h = Domain.spawn d2 in let r1 = d1 () in let r2 = Domain.join h in assert (not (r1 = 0 && r2 = 0))

此程序在 a 和 b 上存在数据竞争，因此程序可能会表现出非顺序一致的行为。让我们使用语义来证明程序可能会表现出 r1 = 0 && r2 = 0。

抽象机的初始状态为

(* Non-atomic locations *)
a: [t0 -> 0]
b: [t1 -> 0]

(* Domains *)
d1: [a -> t0; b -> t1]
d2: [a -> t0; b -> t1]

执行此程序有多种可能的调度。让我们考虑以下调度

1: a := 1 @ d1
2: b := 1 @ d2
3: !b     @ d1
4: !a     @ d2

在d1执行第一个动作a:=1后，机器状态为

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1] (* new write at t2 *)
b: [t1 -> 0]

(* Domains *)
d1: [a -> t2; b -> t1] (* frontier updated at a *)
d2: [a -> t0; b -> t1]

在d2执行第二个动作b:=1后，机器状态为

(* Non-atomic locations *)
a: [t0 -> 0; t2 -> 1]
b: [t1 -> 0; t3 -> 1] (* new write at t3 *)

(* Domains *)
d1: [a -> t2; b -> t1]
d2: [a -> t0; b -> t3] (* frontier updated at b *)

现在，对于d1执行的第三个动作!b，观察到d1在b处的边界在t1。因此，读取可能返回0或1。假设它返回0。机器状态不会因非原子读取而更新。

类似地，对于d2执行的第四个动作!a，d2在a处的边界在t0。因此，此读取也可能返回0或1。假设它返回0。因此，原始程序中的断言assert (not (r1 = 0 && r2 = 0))对于此特定执行将失败。

6 不符合规范的操作

某些操作不符合内存模型规范。

版权所有 © 2024 法国国家信息与自动化研究所