ARM 与 POWER 宽松内存模型入门

标题：A Tutorial Introduction to the ARM and POWER Relaxed Memory Models

日期：2012/10/10

作者：Luc Maranget, Susmit Sarkar, Peter Sewell

链接：https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf

注意：此为 AI 翻译生成 的中文转录稿，详细说明请参阅仓库中的 README 文件。

备注一：图非常多，必须要看原文，这里只是方便阅读。文中的生成代码不用管。

备注二：这是我能找到的最入门的资料了……（perfbook 那种简化概念的不算）

1 导论

ARM 和 IBM POWER 多处理器拥有高度松弛的内存模型：它们利用了一系列硬件优化，这些优化不影响顺序代码的可观察行为，但会暴露给并发程序员。除非存在足够的同步（以屏障、依赖和加载-保留/存储-条件对的形式），否则并发代码可能不会按预期方式执行。在本教程中，我们通过示例解释程序员应了解的一些主要问题。这些材料基于广泛的实验测试、与一些设计者的讨论，以及旨在捕捉架构意图的形式化模型（尽管我们不代表供应商发言）。为使本教程尽可能易于理解，我们引用了我们之前的工作来获取这些细节。

我们强调，我们的重点是低级并发代码：同步库的实现、并发数据结构等。对于遵循正确锁定规范并且除了锁实现之外无数据竞争的简单高级代码，我们所描述的大部分内容都不应成为问题。即使对于低级代码，虽然我们的一些示例出现在实际编程范式中，但有些（据我们所知）则不然，它们仅仅是为了提供一个关于机器可能行为的相当完整的图景。

1.1 范围

ARM 和 IBM POWER 架构在许多方面有所不同，但它们有相似（尽管不完全相同）的松弛内存模型。在这里，我们的目标是涵盖在用户或操作系统内核代码中可能出现的、用于主存中典型低级并发算法所需的指令集片段的内存模型。我们包括内存读写、寄存器到寄存器的操作、分支以及指令之间的各种依赖关系。

这两种架构各自有多种强制特定排序属性的特殊指令。首先，有内存屏障。对于 POWER，我们涵盖 sync（也称为 hwsync 或 sync 0）、lwsync 和 eieio 屏障，而对于 ARM，我们涵盖 DMB 屏障，它类似于 POWER 的 sync。其次，有 POWER 的 isync 指令和类似的 ARM ISB 指令。第三，有 POWER 的加载-保留/存储-条件对 larx/stcx 和 ARM 的加载-独占/存储-独占对 LDREX/STREX。我们不处理混合大小的访问或对页表、缓存提示、自修改代码或中断的显式操作。对于 ARM，我们假设所有观察者都在“相同的所需共享域”内。

1.2 组织结构

我们围绕一系列示例（通常称为石蕊测试）来组织解释：这些非常小的并发程序，仅访问少数共享变量，它们阐释了人们应该了解的主要松弛内存现象。大多数示例取自对有趣的小型示例的系统研究，涵盖了达到一定规模的所有可能的通信和同步模式，我们将这些示例汇总到第9节的“周期表”中。为了让读者尽可能清晰地看到通信和同步模式，这些示例是抽象的，而不是取自生产代码，但我们会简要讨论每种模式可能出现的用例（以及对其行为的可能的微架构解释）。阅读本教程后，读者应该能够审视一些生产并发代码，并根据其使用的通信和同步模式进行分析。第10-12节阐释了各种更微妙的现象，然后第13节讨论了加载-独占/存储-独占（ARM）和加载-保留/存储-条件（POWER）指令。第14节用石蕊测试模式分析了一个示例算法——Peterson互斥算法的简化版本。第15节将我们使用的石蕊测试与文献中出现的一些测试联系起来，第16节回顾了一些相关工作。

最后，第17节描述了可在线获取的支持材料。多篇论文描述了一个用于 POWER 的操作性抽象机模型，用该模型解释了一些石蕊测试的行为，为在 POWER 处理器上实现 C11 和 C++11 修订标准的 C/C++ 并发模型 [BA08, BOS+11, Bec11, ISO11] 提供了正确性证明，并给出了一个 POWER 的公理化模型。我们的 ppcmem 工具，通过一个 Web 界面提供，让用户可以交互式地探索 POWER 或 ARM 石蕊测试在我们操作模型下的行为；我们的 litmus 工具接受一个石蕊测试并构建一个测试工具（作为一个带有嵌入式汇编的 C 程序）来实验性地测试其可观察行为；我们的 diy 工具从简洁的规范中生成石蕊测试。还有一个在线的测试和实验结果摘要。

2 从顺序一致性到松弛内存模型

人们可能期望多处理器具有顺序一致性 (sequentially consistent, SC) 的共享内存，正如 Lamport [Lam79] 所阐述的：

“任何执行的结果都与所有处理器的操作以某种顺序执行的结果相同，并且每个独立处理器的操作在该序列中出现的顺序与程序指定的顺序一致。”

一个 SC 机器可以建模为下图所示：

[说明：此处原文为一张图示，展示了多个线程通过读(R)写(W)操作访问同一个共享内存。]

这里有多个硬件线程，每个线程都按照程序指定的代码执行，它们访问一个单一的共享内存（通过写入和读取其在每个地址保存的值）。这样的机器有两个关键属性：

  1. 没有局部重排序：每个硬件线程都按照程序指定的顺序执行指令，在开始下一条指令之前完成每条指令（包括对共享内存的任何读或写）。

  2. 每个写操作同时对所有线程（包括执行写的线程）可见。

然而，大多数多处理器并非顺序一致的，包括当前的 ARM、POWER、x86、Itanium 和 SPARC 架构，以及其他至少可以追溯到 1972 年 IBM System 370/158MP 的架构。相反，它们有各种松弛或弱内存模型：它们只保证较弱的属性，以允许处理器实现中一系列微架构优化，从而提供更好的性能、更低的能耗或更简单的硬件。这些优化通常对于单线程代码或遵循传统锁定规范且（锁实现之外）无竞争的程序是不可观察的，但一般的并发代码可以观察到非 SC 行为。

细节因架构而异，甚至在同一架构的不同处理器实现之间也有所不同。从广义上讲，x86 和 SPARC 是相似的，具有基于完全存储定序 (Total Store Ordering, TSO) 模型 [Spa92, OSS09, SSO+10] 的相对较强的模型，我们将在下面回顾。ARM 和 POWER 比 TSO 弱得多（尽管它们彼此大致相似），我们将在本教程中描述。Itanium [Int02] 也比 TSO 弱得多，但方式与 ARM 和 POWER 有很大不同；我们在此不作介绍。

TSO 一台 x86-TSO 或 SPARC TSO 机器可以用下图来描述 [SSO+10, OSS09, SSZN+09, Spa92]。这里每个硬件线程都有一个待处理内存写的 FIFO 写缓冲（从而避免了在写操作完成时阻塞线程）。此外，TSO 中的读操作需要从本地存储缓冲中最新的写（如果存在相同地址的写）中读取。

[说明：此处原文为一张图示，展示了每个线程都有一个本地的写缓冲，线程的写操作先进入写缓冲，读操作可以从自己的写缓冲或共享内存中读取。写缓冲通过一个锁机制写入共享内存。]

此外，许多 x86 指令涉及多次内存访问，例如 x86 的增量指令 INC。默认情况下，这些指令不保证是原子的（因此，对一个初始为0的位置进行两次并行的增量操作可能导致其值为1），但它们有原子变体：LOCK;INC 原子地执行一次读、一次写回增量值，并刷新本地写缓冲，有效地在操作期间锁定了内存。比较并交换指令 (CMPXCHG) 也是以同样的方式原子的，而内存栅栏 (MFENCE) 仅仅刷新本地写缓冲。SPARC 是相似的，但其原子指令的种类比通用的 LOCK 前缀要少。

回到上面的两个属性，在 TSO 中，一个线程可以在其自身的写操作对其他线程可见之前看到它们（通过从其写缓冲中读取），但任何写操作都会同时对所有其他线程可见：TSO 是一个多副本原子 (multiple-copy atomic) 模型，用 Collier [Col92] 的术语来说。人们也可以将从本地写缓冲读取的可能性看作是一种特定的局部重排序。一个先写位置x然后读另一位置y的程序，可能会通过将对x的写添加到线程的缓冲中，然后从内存中读取y，最后通过刷新缓冲将对x的写对其他线程可见来执行。在这种情况下，该线程读取的y值是新x值写入内存之前的y值。

ARM 和 POWER ARM 和 IBM POWER 采用了更为松弛的内存模型。出于多种原因（包括性能、功耗效率、硬件复杂性和历史选择），它们允许更广泛的硬件优化对程序员可见。这默认允许了广泛的松弛行为，因此这些架构也提供了机制，以各种内存屏障和依赖保证的形式，让程序员仅在需要时强制更强的排序（并为此付出代价）。在没有这些机制的情况下：

  1. 硬件线程可以乱序地执行读写，甚至可以推测性地执行（在前面的条件分支被解决之前）。与 TSO 不同（TSO 中除了对不同地址的写后读之外没有局部重排序），在这里，除非另有规定，任何局部重排序都是允许的。

  2. 内存系统（可能涉及一个缓冲层次和一个复杂的互连）不保证一个写操作在同一时间点对所有其他硬件线程可见；这些架构不是多副本原子的。

实现与架构 为了更详细地解释 ARM 和 POWER 允许的行为，我们必须清晰地区分多处理器的几种视图。一个特定的处理器实现，如 IBM POWER 7 或 NVIDIA Tegra 2（一个包含双核 ARM Cortex-A9 CPU 的 SoC），将有一个特定的微架构和详细设计，其中包含许多优化。我们在此不关心这些设计的内部结构，因为它们过于复杂，无法提供一个好的编程模型，并且通常是商业机密。

相反，我们关心的是实现的程序员可观察行为：程序员通过在某个特定实现上执行多线程程序并检查结果可能看到的所有行为集合（此外，我们这里只关心正确性属性，而不是性能行为）。

即使这样，通常也过于具体：每个处理器家族都包含许多实现，这些实现（正如我们将看到的）可以有显著不同的程序员可观察行为，而人们通常希望软件能在所有这些实现上正确工作，而不仅仅是在某个特定的处理器实现上。一个架构指定了一个程序员可以依赖的行为范围，适用于任何符合该架构的处理器实现。一个架构的规范可能比特定处理器实现的程序员可观察行为要松散得多，以适应当前、过去和未来实现之间的差异。（当然，这种松散性给软件开发带来了挑战：原则上，人们可能认为应该“面向架构编程”，但正常的软件开发依赖于在特定处理器实现上测试软件，这些实现可能不会展现其他实现会或将会展现的某些架构上允许的行为。）

处理器供应商会发布架构规范，例如 Power ISA 2.06 版 [Pow09] 和 ARM 架构参考手册（ARMv7-A 和 ARMv7-R 版）[ARM08a]。它们使用散文和伪代码来描述一系列可观察行为，并且通常对顺序行为相当精确，但在涉及并发行为和松弛内存现象时，清晰度就不如人们所希望的了——用散文来明确无误且完整地捕捉这些微妙之处是非常困难的。

相反，我们和其他人提倡使用数学上严谨的架构定义。这些定义通常以操作模型的形式呈现，最为易懂，例如上面展示的 TSO 机器模型。这带有一种“抽象微架构”的风格：它是一个抽象机器，拥有一些机器状态（包括共享内存、FIFO 写缓冲和线程的状态）以及机器可以进行的转换的定义。它隐含地指定了一个并发程序的可观察行为范围，即该抽象机器在运行该程序时可能展现的所有行为；通过声称一个抽象机器是一系列处理器实现的可靠架构模型，我们的意思是，对于任何程序，抽象机器运行该程序的可观察行为集合包含了任何这些实现运行该程序可能展现的任何行为。另一方面，抽象机器的内部结构可能与处理器实现的微架构和详细设计非常不同。实际上，现代 x86 处理器通常会有复杂的缓存层次结构、乱序执行等等，与抽象机器的简单 FIFO 写缓冲结构大相径庭。抽象机器模型的意义在于，那些内部结构对程序员是不可观察的（除了通过性能属性）。

在进行中的工作中，我们正在为 ARM 和 POWER 开发数学上严谨的操作模型架构规范 [SSA+11, SMO+12]。在本教程中，我们专注于通过示例解释 ARM 和 POWER 允许哪些可观察行为，所以我们不会详细给出那些模型，但为了建立一些关于并发程序如何行为的直觉，首先介绍模型中使用的一些基本概念是很有用的。我们再次强调，这些概念不应与当前实现的实际微架构相混淆。

ARM 和 POWER 抽象机概念 为了解释一个非多副本原子机器的行为，有时将每个线程想象成有效地拥有自己的内存副本是很有帮助的，如下图所示，它抽象地指定了该线程在正常情况下会为任何地址读取什么值。一个线程的写操作可以以任何顺序传播到其他线程，不同地址的写操作的传播可以任意交错，除非它们受到屏障或相干性的约束。正如我们稍后将看到的，人们也可以将屏障（ARM DMB 和 POWER sync 及 lwsync）想象成从执行它们的硬件线程传播到每个其他线程。

[说明：此处原文为一张图示，展示了五个线程，每个线程都有自己独立的内存视图（Memory 1 到 Memory 5）。这些内存视图之间通过双向箭头连接，表示写操作的传播。]

我们将所有内存及其互连（即除了线程之外的一切）的集合称为存储子系统。

对于线程局部的乱序（和推测性）执行，通常我们可以将每个线程在任何时间点看作拥有一棵已提交和执行中的指令实例树。新获取的指令成为执行中的，稍后，在满足适当的先决条件后，可以被提交。例如，下面我们展示了一组指令实例 {i1, ..., i13}，它们之间有程序顺序后继关系。其中三个（{i1, i3, i4}，用方框标出）已经被提交；其余的正在执行中。

[说明：此处原文为一张指令流水线的树状图示，展示了已提交和未提交（执行中）的指令。]

指令实例 i5 和 i9 是分支，线程已经为它们获取了多个可能的后继；这里只有两个，但一个具有计算地址的分支原则上可以获取许多可能的后继。一个典型的实现很可能每次只探索一个推测路径。注意，已提交的实例不一定是连续的：这里 i3 和 i4 已经提交，即使 i2 还没有，这只有在它们足够独立时才会发生。当一个分支被提交时，任何未被采纳的替代路径都会被丢弃，跟随（在程序顺序中）一个未提交分支的指令直到该分支被提交后才能被提交，所以树在任何已提交（方框）指令之前必须是线性的。

对于一个读指令，一旦读的地址已知，该读就可能被满足 (satisfied)，将其值绑定到从本地内存接收到的一个值（或者在某些情况下，从线程中更早的指令前递而来）。该值可以立即被线程中依赖它的后续指令使用，但它和这些后续指令都可能被重启或（如果这是一个推测路径）中止，直到读被提交 (committed)。

对于一个写指令，关键点是其地址和值何时被确定。之后（受其他条件约束），该写可以被提交，发送到本地内存；这不会被重启或中止。之后，该写可能会传播 (propagate) 到其他线程，变得可被它们读取。

屏障是相似的，它们在线程处被提交并发送到存储子系统的本地部分，然后可能传播到其他线程。正如我们将看到的，写和屏障如何传播的约束是相互交织的。

旁注：原子性的其他概念 我们上面介绍了多副本原子性，但需要注意，因为“原子”有许多不同的含义。另外两个重要的原子性概念如下。

一个指令的内存读或写是访问原子的 (access-atomic)（或用 Collier [Col92] 的术语是单副本原子的 (single-copy atomic)——但注意单副本原子不是多副本原子的反义词），如果它引起对内存的单次访问。通常，一个架构会指定某些大小的读写，在满足某些对齐约束的情况下（例如1、2、4、8和16字节的访问以及它们的对齐），是访问原子的，而其他大小和未对齐的访问可能会被拆分成几个不同的子访问。例如，对同一地址的两个相同大小的写是访问原子的，当且仅当结果保证是其中一个值，而不是它们比特的组合。当然，在一个非多副本原子的机器中，即使一个写指令是访问原子的，该写也可能在不同时间对不同线程可见（如果一个写不是访问原子的，各个子访问也可能在不同时间、可能以不同顺序对不同线程可见）。

一个涉及多于一次内存访问的指令，例如对同一位置进行读和写的增量操作，或读取多个字的加载多指令，是指令原子的 (instruction-atomic)，如果其访问在时间上是不可分割的，没有其他线程对这些位置的干预访问。例如，增量操作是指令原子的，当且仅当对一个初始为0的同一位置的两个并发增量操作保证导致该位置包含2，而不是1。在x86上，INC 不是指令原子的，而 LOCK;INC 是。在POWER上，lmw 加载多指令不是指令原子的。

另一个用法是 C11 和 C++11 的原子类型和操作。它们具有各种属性，包括访问原子性和指令原子性的类似物，我们在此不讨论；详见 [BA08, BOS+11, Bec11, ISO11]。

3 引入石蕊测试和简单消息传递 (MP)

3.1 无屏障或依赖的消息传递尝试

3.1.1 消息传递 (MP) 示例

一个简单的例子说明了 ARM 和 POWER 在哪些方面是松弛的，这就是经典的消息传递 (MP) 示例，它有两个线程（线程0和线程1）和两个共享变量（x和y）。这是一个简单的低级并发编程范式，其中一个线程（线程0）写入一些数据 x，然后设置一个标志 y 来表明数据已准备好被读取，而另一个线程（线程1）则忙等待读取标志 y 直到看到它被设置，然后读取数据 x 到一个局部变量或处理器寄存器 r2。期望的行为是，在读取线程看到标志被设置后，它随后对数据 x 的读取将看到写入线程的值，而不是初始状态（或其他一些先前的值）。伪代码如下：

MP-loop (循环)

伪代码

线程 0

x=1 // 写数据

y=1 // 写标志

线程 1

while (y==0) {} // 忙等待标志

r2=x // 读数据

初始状态: x=0 ∧ y=0

禁止?: 线程1寄存器 r2 = 0

该测试指定了寄存器和内存的初始状态（x=0 和 y=0；此后若未明确给出，我们假设它们为零）以及对最终状态的约束，例如线程1的寄存器 r2 为0。这里 x（或在汇编测试中的 [x]）是内存位置 x 的值；稍后我们用 1:r2 表示硬件线程1上寄存器 r2 的值。如果达到了 r2=0 的最终状态，那么线程1对 x 的读取必须是在线程1的 while 循环成功退出（因读取到线程0写入的 y=1）之后，却读取到了来自初始状态的 x=0，而线程0对 y=1 的写入是在程序顺序上晚于其对 x=1 的写入。

我们可以通过只关注标志的一次测试来简化这个例子，而不会真正影响正在发生的事情：与其查看 MP-loop 忙等待循环的所有执行，我们可以将注意力限制在 MP 程序（如下）的执行上，其中线程1对 y 的读取看到了由线程0写入的值1（我们实际上只考虑 MP-loop 中 while 循环测试第一次就成功的执行）。换句话说，期望的行为是，如果对 y 的读取看到了1，那么对 x 的读取就一定不能看到0。或者等价地说，r1=1 且 r2=0 的最终结果应该被禁止。

MP

伪代码

线程 0

x=1

y=1

线程 1

r1=y

r2=x

初始状态: x=0 ∧ y=0

禁止?: 1:r1=1 ∧ 1:r2=0

像这样的石蕊测试包含一个小的多线程程序，具有定义的初始状态和对它们最终状态的约束，从而挑选出感兴趣的潜在执行。鉴于此，对于任何架构，我们可以问这样的执行是被允许还是禁止；我们也可以在特定的处理器实现上运行测试（在一个测试工具 [AMSS11a] 中），看看它是被观察到还是未观察到。

在本文档中，我们使用术语“线程”来指代 SMT 机器上的硬件线程和非 SMT 机器上的处理器。假设有一个正确实现的调度器（在上下文切换时有适当的屏障），将软件线程以同样的方式看待应该是可靠的。

3.1.2 可观察行为

在一个顺序一致的模型中，r1=1 ∧ r2=0 的最终结果确实是被禁止的，因为不存在允许它的读写交错（其中每个读都读取到相同地址的最近的写）。为了检查这一点，可以枚举尊重每个线程程序顺序的六种可能的交错：

[说明：此处原文为一张表格，列出了六种指令交错及其最终的寄存器状态，表明在顺序一致性模型下，不可能出现 r1=1 且 r2=0 的情况。该表格已忽略。]

在 x86-TSO 或 SPARC TSO 上，r1=1 ∧ r2=0 的最终结果也是被禁止的，因为两个写操作通过一个 FIFO 缓冲流入共享内存，然后才对读取线程可见。但是在 ARM 和 POWER 上，这个最终结果在架构上是允许的，并且在当前的处理器实现上是普遍可观察到的。 线程1可以看到标志 y 被设置为1，然后按程序顺序随后看到数据 x 仍然是0。下表给出了一些样本实验数据，使用我们的 litmus 工具 [AMSS11a] 在各种处理器实现上运行此测试。每个条目给出一个比率 m/n，其中 m 是在 n 次试验中观察到 r1=1 ∧ r2=0 最终结果的次数。

[说明：此处原文为一张表格，展示了MP测试在多种POWER和ARM处理器上的实验结果，表明 r1=1 ∧ r2=0 的结果是允许(Allow)且可以被观察到的。该表格已忽略。]

当然，在解释这类结果时需要谨慎：具体的数字可能高度依赖于测试工具；这种对高度不确定性系统的测试不保证能产生一个实现可能产生的所有执行；并且架构在某些方面有意地比当前实现更松散，所以（正如我们稍后将看到的）某些行为可能在架构上是允许的，即使它在当前的处理器上从未被观察到。此外，我们的架构模型、供应商的架构意图以及供应商的架构手册（ARM ARM [ARM08a] 和 POWER ISA [Pow09]）之间可能存在差异。当然，虽然我们的模型部分基于与 ARM 和 IBM 架构师和设计师的广泛讨论，但我们不代表任何一方供应商。尽管如此，我们对我们的模型有合理的信心，并且我们发现我们的测试过程具有合理的区分度。凡是我们标记为允许或禁止的测试执行，我们相信这与架构意图相符，并且，除非另有说明，所有标记为允许的都在某个实现上是可观察到的，而（除了处理器勘误，我们在此不讨论）所有标记为禁止的都未被观察到。我们在每个部分给出一些总结性的测试数据来说明这一点。

3.1.3 行为解释

要解释为什么某个特定的松弛行为被一个架构所允许，或者为什么它可能在一个处理器实现上是可观察的，人们可以参考处理器供应商的架构文本，或者实现的微架构细节，或者一个试图捕捉其中之一的形式化模型，或者对这样一个模型的直观描述。所有这些都有其用途和缺点。参考供应商的架构文本具有通用性（因为它们旨在适用于该架构的所有处理器实现）和权威性。但当涉及到松弛内存行为时，它们往往不如人们希望的那么清晰。一个完整的微架构解释原则上是完全精确的，但需要处理器实现的详细知识，而这通常是商业机密，并且它也只适用于那个实现。对于第三个选项，我们的形式化模型 [OSS09, SSO+10, SSA+11, SMO+12] 旨在捕捉供应商的架构意图，并与观察到的行为一致，适用于 x86 和 POWER。它们用严谨的数学表达，因此是完全精确的，而且这种数学也可以用来自动生成测试和探索工具，就像我们的 ppcmem 工具一样。但这种数学细节可能使它们对广大读者来说不易理解。因此，在本教程中，我们利用了那些形式化模型是“抽象微架构”风格的特点：为了建立对形式化架构模型（并因此对处理器实现和供应商架构）可观察行为的直觉，我们使用第2节中介绍的抽象机的风格和术语来解释测试的行为。为避免过于繁琐的细节，我们不完全描述形式化模型；为此，读者应参考引用的论文。

为了解释 MP 在 ARM 和 POWER 上的观察行为，有三种不同的可能性：线程0上的写操作针对不同的地址，因此可以在线程0上乱序提交；和/或它们也可能以任一顺序传播到线程1；和/或线程1上的读操作（同样针对不同地址）可以乱序满足，以与程序顺序相反的顺序绑定它们读取的值（读操作也可能按顺序或乱序提交，但这对结果没有影响）。这些微架构特性中的任何一个单独存在都足以解释上述的非顺序一致性行为。

3.1.4 测试执行图

在我们将使用的大多数示例中，最终状态约束唯一地确定了一个候选执行，隐含地指定了任何读操作从哪个写操作中读取，任何控制流选择如何解决，以及对于每个位置，该位置的写操作如何相互排序（它们的相干性顺序，我们将在第8节中讨论）。用图表形式来思考这个执行，从代码中抽象出来，是很有帮助的。例如，我们可以用下面的执行图来描述上面的 MP 测试。

该图为每个内存访问都有一个节点。节点被标记（a, b, c, d），以便我们可以引用它们，并且每个节点都指定了它是写（W）还是读（R），它的位置（这里是 x 或 y），以及在此执行中读取或写入的值（这里是0或1）。事件按每个线程一列的方式排列，每个线程的两个事件之间有一个程序顺序 (program order, po) 边（这里恰好与源代码中两条指令的句法顺序相同，但通常它代表了该线程的一条控制流路径的选择，展开了任何分支）。从 b 到 c 的读自 (reads-from, rf) 边表示读 c 从写 b 中读取了值，而从一个红点到读 d 的读自边表示后者从初始状态读取。我们将根据需要引入其他类型的节点和边。有时我们会在图上标记以指示该执行是允许的还是禁止的（根据我们的模型和我们对供应商架构意图的最佳理解）。

3.1.5 伪代码 vs 真实代码

通常，松弛内存行为可以由硬件（来自微架构优化）和编译器（来自编译器优化）引入。例如，编译器很可能进行公共子表达式消除（CSE），从而对每个线程代码内对不同位置的访问进行重排序。在本教程中，我们只讨论硬件如何执行机器码汇编指令，我们给出的伪代码必须被理解为对实际执行的汇编指令的描述，而不是 C、Java 或其他高级语言中的程序。因此，我们将测试的最终版本视为 POWER 和 ARM 汇编代码，如下右侧所示，而不是上面和左侧的伪代码。对于不熟悉它的人来说，汇编代码可能更难阅读，但由于我们通常使用如上的执行图，这通常不是问题。

[说明：此处原文为一张表格，并列展示了MP测试的伪代码版本、ARM汇编版本和POWER汇编版本。该表格已忽略。]

3.1.6 未定义行为和数据竞争

通过专注于机器码的执行，我们也可以回避这样一个事实，即在某些高级语言中，某些程序具有未定义的行为。例如，在 C11/C++11 中，除非 y 被声明为 atomic，否则上面的代码会引起数据竞争，使得任何执行它的程序都是未定义的，如果它被声明为 atomic，编译器可能会引入各种汇编语言的栅栏（取决于原子访问的内存顺序参数）。在机器码级别，所有程序都有明确定义的（尽管通常是不确定的）行为，即使它们有竞争。

3.1.7 MP 范式的实际用法

在上面展示的 MP 测试中，数据 x 只是一个单一的内存位置，但在实际使用中，人们可能会有多字数据。对于我们稍后探讨的大多数或所有 MP 变体，这应该没有区别。

3.1.8 在 ppcmem 中运行示例

要使用我们的 ppcmem 工具交互式地探索此示例的行为，请访问 http://www.cl.cam.ac.uk/~pes20/ppcmem，如果需要，点击 Change to ARM model，点击 Select POWER/ARM Test 并从菜单中选择 MP，然后点击 Interactive。屏幕将显示我们模型（我们不在此处给出所有细节，但它们在我们的 PLDI 2011 和 PLDI 2012 论文 [SSA+11, SMO+12] 中有描述）运行该测试的状态，带有绿色下划线的选项是可能的模型转换；可以点击这些选项来探索特定的可能行为。另外，通过 http://www.cl.cam.ac.uk/~pes20/ppc-supplemental 的 Tests and Test Results 链接，可以直接链接到在 ppcmem 上运行每个 POWER 测试。

3.2 使用强 (dmb/sync) 屏障强制顺序

为了恢复顺序，程序员必须防御所有上述的乱序可能性。在线程0的两个写操作之间，以及线程1的两个读操作之间插入一个强内存屏障（或栅栏）指令就足够了。在 POWER 上，这将是 sync 指令（也写作 hwsync），在 ARM 上，它将是 DMB。得到的石蕊测试如下所示。

[说明：此处原文为一张表格，并列展示了MP+dmb/syncs测试的伪代码版本、ARM汇编版本和POWER汇编版本，关键在于在指令之间加入了 dmb/sync 屏障。]

我们如下所示地说明感兴趣的执行，用绿色的 dmb/sync 箭头表示由 sync 或 DMB 指令分隔的内存访问。

在微架构上，以及在我们的模型中，线程0上的 sync 或 DMB 保持了两个写操作的顺序，无论是在本地还是在它们传播到系统中其他线程的顺序上。同时，线程1上的 dmb/sync 通过阻止第二个读在第一个读被满足之前被满足，强制两个读按程序顺序被满足并绑定它们的值。请注意，正如我们下面将看到的，这比必要的强度要大得多，使用各种依赖或更轻量级的屏障就足够了。

dmb/sync 屏障可能开销很大，但它们满足这样一个属性：如果在每对内存访问之间都插入它们，它们会恢复顺序一致的行为。更详细地看，一对读或写操作前后屏障的四种情况，我们有：

  • RR 对于由 dmb/sync 分隔的两个读，屏障将确保它们按程序顺序被满足，并且也确保它们按程序顺序被提交。

  • RW 对于由 dmb/sync 分隔的一个读后跟一个写，屏障将确保在写可以被提交之前，读被满足（并且也被提交），因此在写可以传播并对任何其他线程可见之前。

  • WW 对于由 dmb/sync 分隔的两个写，屏障将确保在第二个写被提交之前，第一个写被提交并已传播到所有其他线程，因此在第二个写可以传播到任何其他线程之前。

  • WR 对于由 dmb/sync 分隔的一个写后跟一个读，屏障将确保在读被满足之前，写被提交并已传播到所有其他线程。

我们强调，这些描述都是从程序员模型的角度来看的。一个实际的硬件实现可能会更激进，例如，对跟随屏障的指令进行一些推测性执行，或者一个允许更多写传播的微架构结构，只要程序员无法检测到它。

3.3 使用 POWER lwsync 屏障强制顺序

在 POWER 上，有一个“轻量级同步” lwsync 指令，它比“重量级同步” sync 指令更弱且可能更快，对于这个消息传递示例，在写入方和读取方两边使用 lwsync 就足够了。再次看上面的四种情况：

  • RR 对于由 lwsync 分隔的两个读，就像 sync 一样，屏障将确保它们按程序顺序被满足，并且也确保它们按程序顺序被提交。

  • RW 对于由 lwsync 分隔的一个读后跟一个写，就像 sync 一样，屏障将确保在写可以被提交之前，读被满足（并且也被提交），因此在写可以传播并对任何其他线程可见之前。

  • WW 对于由 lwsync 分隔的两个写，屏障将确保对于任何特定的其他线程，第一个写¹ 在第二个写之前传播到该线程。

  • WR 对于由 lwsync 分隔的一个写后跟一个读，屏障将确保在读被满足之前写被提交，但允许在写传播到任何其他线程之前满足该读。

在这个消息传递示例中，我们只需要 WW 和 RR 的情况；写入线程上的一个 lwsync 保持了两个写操作的顺序（它们的提交和传播），就读取线程而言，而读取线程上的一个 lwsync 确保了读操作按程序顺序被满足。

¹ 或其相干性后继；见第8节。

[说明：此处原文为一张表格，展示了MP+lwsyncs测试的伪代码版本和POWER汇编版本。]

我们将在第6节的 SB+lwsyncs 测试中展示一个 lwsync 的弱点真正重要的情况。ARM 没有 lwsync 的类似物。

3.4 可观察行为

下面我们展示了这些测试的实验数据：对于 ARM 和 POWER 上的 MP+dmbs 和 MP+syncs，以及仅在 POWER 上的 MP+lwsyncs。

[说明：此处原文为一张表格，展示了MP、MP+dmbs/syncs和MP+lwsyncs测试在多种处理器上的实验结果。MP的非预期结果是可观察的，而带有屏障的变体则未观察到非预期结果。]

这里，MP 的允许结果在所有平台上都是可观察的，而带有屏障的变体的禁止结果在任何平台上都不可观察。

4 使用依赖强制顺序

实际上，在消息传递示例的读取端，上面使用的 sync、lwsync 和 DMB 内存屏障都强于必要：仅仅依靠代码中的各种依赖 (dependency) 就可以强制足够的排序来禁止不期望的结果。在本节中，我们解释这些依赖是什么以及它们的作用。在后面的章节中，我们在说明机器的其他一些松弛内存属性的示例中使用依赖。对于 POWER，在本节的所有示例中，人们都可以用 lwsync 替换写入线程上的 sync 而不影响结果。

4.1 地址依赖

最简单的一种依赖是地址依赖 (address dependency)。当第一个读指令读取的值被用来计算程序顺序上后面的读或写指令所使用的地址时，就存在从一个读指令到该读或写指令的地址依赖。在下面的 MP 变体中，写入方线程0不是写入一个标志值1，而是写入位置 x 的地址，读取方线程1则使用该地址进行其第二次读取。这个依赖足以保持线程1上的两个读操作按程序顺序被满足：第二个读在其地址（可能被推测性地）知道之前无法开始，因此在第一个读被满足之前，第二个读无法被满足（换句话说，ARM 和 POWER 架构不允许对地址进行值推测）。将其与线程0上的 dmb/sync（它保持了对x的写和对y的写，就任何其他线程而言，是有序的）结合起来，就足以防止线程1在读取了 &x 之后从y中读取到x的0值。

[说明：此处原文为一张表格，展示了 MP+dmb/sync+addr' 测试的伪代码版本。]

请注意，我们的伪代码的类C语法（其中 x 是一个C变量，&x 是其地址）与我们的汇编示例的表示法（其中 x 是一个位置）之间存在轻微的不匹配。

4.1.1 复合数据

为了看到这种带依赖的消息传递范式在数据（存储在 x 处的值）是多字的情况下仍然能正确工作，请注意，所有对数据部分的写入都会在线程0的 dmb/sync 之前，而所有对数据部分的读取都应该通过某种偏移计算，地址依赖于从 y 读取的值。

4.1.2 C11 Consume

这种被保留的地址依赖正是 C/C++11 内存模型通过它们的 read-consume 原子操作提供的：如果在 C/C++ 级别上对 y 的读取被标记为 read-consume，那么编译器必须尊重到线程1第二次读取的依赖（或者实现更强的机制，例如在它们之间放置一个 lwsync/sync/dmb 屏障）。

4.1.3 从读到写的地址依赖

从读到写的地址依赖具有与从读到读的地址依赖相似的效果，防止写操作在读被满足并知道其值之前开始；我们将在第4.4节的测试S中说明这一点。

4.1.4 人为依赖

上面我们说过“当第一个读指令读取的值被用来计算程序顺序上后面的读或写指令所使用的地址时，就存在从一个读指令到该读或写指令的地址依赖”，并且该计算可以通过寄存器和算术或逻辑运算的任何数据流路径（尽管不是通过内存）——即使使用的地址值不受读取值的影响。在下面的 MP+dmb/sync+addr 变体中，读取的值与自身进行异或运算，然后加到 x 的（常量）地址上，以计算线程1第二次读取要使用的地址。异或的结果将永远是零，因此第二次读取使用的地址将永远等于 x 的地址，但这两个读取仍然保持有序。添加这样一个人为的依赖（有时这些被称为，可能会令人困惑地，假依赖或伪依赖）可以是一种有用的编程范式，以低运行时成本强制从一个读到后续读（或写）的某种排序。

[说明：此处原文为一张表格，并列展示了 MP+dmb/sync+addr 测试的伪代码、ARM汇编和POWER汇编版本。]

由于人为地址依赖的行为与自然地址依赖完全相同，我们用同样的方式绘制它们，用 addr 边，从地址计算的具体细节中抽象出来。

4.2 控制依赖

一种相当不同的依赖是控制依赖 (control dependency)，从一个读到程序顺序上后面的读或写指令，其中第一个读读取的值被用来计算一个条件分支的条件，而该分支在程序顺序上位于第二个读或写之前。

从读到读的控制依赖几乎没有强制力，正如我们在下面的 MP+dmb+ctrl 和 MP+sync+ctrl 示例中看到的：ARM 和 POWER 处理器可以推测性地执行过条件分支（可能基于分支预测遵循一条路径，或者原则上同时遵循两条路径），因此在满足第一个读之前满足第二个读。第一个读、分支和第二个读随后都可能（以这些值）按程序顺序被提交。

[说明：此处原文为一张表格，并列展示了 MP+dmb/sync+ctrl 测试的伪代码、ARM汇编和POWER汇编版本。]

为简洁起见，我们展示的示例中分支只是跳转到下一条指令，无论分支是否被采纳，该指令都会被执行。这没有区别：如果分支跳转到不同的位置并且第二次读取只在一种情况下执行，行为将完全相同。

示例中分支条件的值也不受读取值的影响，因为它只是基于一个寄存器与自身的相等比较。就像上面描述的人为地址依赖一样，这也没有区别：控制依赖的存在仅仅依赖于读取的值被用于条件计算的事实，而不管如果读取了不同的值，条件的值是否会改变。因此，有许多方式可以编写一个与上述伪代码示例本质上等效的例子，例如，将 r2=x 放在条件内部，或者对于一个没有 x 上竞争的例子，将对 y 的读取放在一个循环中，如 do {r1=y;} while (r1 == 0)。

4.3 Control-isb/isync 依赖

要给读到读的控制依赖一些强制力，可以在条件分支和第二次读取之间添加一个 ISB (ARM) 或 isync (POWER) 指令，如下面的示例所示。这可以防止第二次读取在条件分支被提交之前被满足，而条件分支在第一个读的值被固定（即，直到该读被满足并提交）之前无法被提交；因此，两个读取被保持有序，测试的指定结果现在被禁止。

[说明：此处原文为一张表格，并列展示了 MP+dmb/sync+ctrlisb/ctrlisync 测试的伪代码、ARM汇编和POWER汇编版本。]

4.4 从读到写的控制依赖

与从读到读的控制依赖（没有 isb/isync）相反，从读到写的控制依赖确实有一些强制力：在分支被提交之前，该写不能被任何其他线程看到，因此在第一个读的值被固定之前。为了说明这一点，我们使用了 MP 测试家族的一个变体，被称为 S（出于历史原因），其中线程1上的第二次读取（对 x）被替换为对 x 的写入。我们不再问线程1对 x 的读取是否保证能看到线程0写入的值，而是问线程1对 x 的写入是否保证在相干性上晚于 (coherence-after) 线程0对 x 的写入（即，一个第三个线程两次读取 x 是否保证不会以相反的顺序看到这两个写；我们将在第8节回到相干性）。在线程1上没有控制依赖的情况下，这是不保证的；下面的执行是允许的。

[说明：此处原文为一张表格，并列展示了 S+dmb/sync+po 测试的伪代码、ARM汇编和POWER汇编版本。]

我们用一个 co 边来表示这种相干性条件，连接两个对同一地址的写。

如果我们对线程1添加一个从读到写的控制依赖，那么最终的结果就变得被禁止了：

[说明：此处原文为一张表格，并列展示了 S+dmb/sync+ctrl 测试的伪代码、ARM汇编和POWER汇编版本。]

4.5 从读到写的数据依赖

我们最后一种依赖是数据依赖 (data dependency)，从一个读到程序顺序上后面的写，其中读取的值被用来计算写入的值。这些依赖与从读到写的地址、控制或 control-isb/isync 依赖具有大致相似的效果：它们防止写在读的值被固定（当读被提交时）之前被提交（并因此传播和对其他线程可见）。因此，下面 S+dmb/sync+ctrl 测试的 S+dmb/sync+data 变体也是被禁止的。

[说明：此处原文为一张表格，并列展示了 S+dmb/sync+data 测试的伪代码、ARM汇编和POWER汇编版本。]

4.6 依赖总结

总结一下，我们有：

  • RR 和 RW address：从一个读到程序顺序上后面的读或写的地址依赖，其中第一个读读取的值被用来计算第二个读或写的地址。

  • RR 和 RW control：从一个读到程序顺序上后面的读或写的控制依赖，其中第一个读读取的值被用来计算一个条件分支的条件，该分支在程序顺序上位于第二个读或写之前。

  • RR 和 RW control-isb/isync：一个control-isb或control-isync依赖，从一个读到程序顺序上后面的读或写，其中第一个读读取的值被用来计算一个条件分支的条件，该分支在程序顺序上位于一个 isb/isync 指令之前，而该指令又在第二个读或写之前。

  • RW data：从一个读到程序顺序上后面的写的数据依赖，其中第一个读读取的值被用来计算写入的值。

没有从写（到读或写）的依赖。

在每种情况下，读取值的使用可以通过任何寄存器到寄存器操作的数据流链，并且无论它是否是人为的（或假/伪的）都无关紧要：即使读取的值不能影响实际用作地址、数据或条件的值，依赖仍然存在。

从一个读到另一个读，一个地址或 control-isb/isync 依赖将阻止第二个读在第一个读被满足之前被满足，而一个普通的控制依赖则不会。

从一个读到写，一个地址、控制（因此也包括 control-isb/isync）或数据依赖将阻止该写在读的值被固定之前对任何其他线程可见。

我们将在第10节回到依赖的一些更微妙的属性。

正如我们将看到的，依赖严格弱于 DMB、sync 和 lwsync 屏障：用其中一个屏障替换一个依赖将永远不会允许更多的行为（因此应该总是一个安全的程序转换），而反之则不成立。依赖只具有线程局部效果，而 DMB、sync 和 lwsync 具有我们将在下一节中介绍的更强的“累积”属性。

4.7 可观察行为

下面我们总结了关于依赖的硬件实验结果。

[说明：此处原文为一张表格，总结了本节中所有带依赖的MP和S变体测试在多种处理器上的实验结果，并标注了其中一些允许(Allow)的结果在特定处理器上未被观察到(Unseen)。]

实验数据显示，禁止的结果都是不可观察的。另一方面，一些允许的结果在某些实现上是不可观察的，如蓝色高亮并带有上标U（allowed-Unseen）所示：对于 MP+sync+po 和 MP+sync+ctrl，POWER 6 没有展现出允许的行为（在这个意义上，它的流水线比 POWER G5 或 POWER 7 更有序），而对于 S+sync+po，这些 POWER 实现都没有。看起来这些实现不会提交一个写操作，当有一个程序顺序上更早的、即使是到不同地址的未完成的读时；当然，其他和未来的实现可能会有所不同。

这些都是特定实现比架构意图更严格的情况，并且这一事实可以而且确实会从一代处理器到下一代处理器发生变化，这加强了这样一个事实，即旨在编写可移植代码的程序员必须关注架构规范，而不仅仅是他们当前的实现。

5 超过两个线程的迭代消息传递和累积性 (WRC 和 ISA2)

到目前为止，我们所有的示例都只用了两个线程。推广到三或四个线程揭示了一个新现象：在 POWER 和 ARM 上，两个线程可以以不同的顺序观察到对不同位置的写操作，即使没有任何线程局部的重排序。换句话说，这些架构不是多副本原子的 [Col92]。要看到这一点，首先考虑一个 MP 的三线程变体，其中第一个写被剥离到另一个线程，线程1在执行自己的写之前忙等待看到它：

WRC-loop

伪代码

线程 0

x=1

线程 1

while (x==0) {}

y=1

线程 2

while (y==0) {}

r3=x

初始状态: x=0 ∧ y=0

禁止?: 2:r3=0

这个测试被称为 WRC，即 Boehm 和 Adve [BA08] 中的“写到读因果性 (write-to-read causality)”。

和以前一样，我们通过移除循环来简化这个例子，用一个最终状态约束来替代它们，该约束将注意力限制在线程1读取到 x=1 并且线程2读取到 y=1 的执行上。问题是，这样的执行是否也可能看到 x=0（而不是从线程0对 x 的写中读取）。

WRC

[说明：此处原文为一张表格，展示了WRC测试的伪代码版本。]

没有任何依赖或屏障，这是微不足道地被允许的：线程1的读和写是针对不同地址的，可以相互重排序，同样线程2的读也可以乱序满足。添加人为依赖以防止这些重排序，我们得到了下面的 WRC+addrs 测试。

WRC+addrs

[说明：此处原文为一张表格，展示了WRC+addrs测试的伪代码版本。]

在一个多副本原子的架构上，这是被禁止的，但在 ARM 和 POWER 上是允许的。线程2必须按程序顺序进行其读取，但线程1在开始其对 y=1 的写入之前看到线程0对 x=1 的写入这一事实，并不妨碍这些写入以相反的顺序传播到线程2，从而允许它读取 y=1 然后读取 x=0。我们在 POWER 实现上观察到了这一点，并期望它在具有两个以上硬件线程的某些 ARM 处理器上是可观察的，但我们目前能接触到的唯一这样的机器（Tegra3）上尚未观察到。

5.1 WRC 的累积屏障

为了防止 WRC 的意外结果，可以加强上面线程1的地址依赖，用一个 DMB 或 sync 屏障替换它（在 POWER 上，较弱的 lwsync 屏障也足够）。

WRC+dmb/sync+addr

[说明：此处原文为一张表格，展示了WRC+dmb/sync+addr测试的伪代码版本。]

在 MP+syncs 中我们看到，一个 DMB 或 sync 屏障保持了同一线程在屏障前后的任何写操作的顺序，就任何其他线程而言。

这里，线程1的 DMB 或 sync 屏障也保持了线程1读自的任何写操作（在屏障前）与线程1在屏障后做的任何写操作的顺序，就任何其他线程（例如，线程2）而言。更一般地，屏障确保了在屏障前已传播到线程1的任何写操作，在线程1屏障后的写操作可以传播到该其他线程之前，也传播到任何其他线程。这个累积 (cumulative) 属性对于迭代消息传递示例至关重要。

作为微小的变体，人们也可以将线程1的屏障削弱为 POWER lwsync，得到 WRC+lwsync+addr 测试，或者将线程2的地址依赖加强为另一个 DMB 或 sync 屏障，得到 WRC+dmbs 或 WRC+syncs 测试；这些都与上面的测试有相同的可能结果。

5.2 ISA2 的累积屏障

WRC 测试扩展了左侧的消息传递（MP）示例，而 WRC+dmb/sync+addr 在那里展示了累积屏障的一个方面。下面的 ISA2 示例展示了累积性的另一个方面。该示例（[Pow09, §1.7.1, Example 2] 的简化版本，像往常一样用最终状态约束替换循环）扩展了右侧的 MP 示例，在最终读取 x 之前，插入了线程1对第三个共享变量 z 的写入和线程2的读取。可以认为这是线程0将一些可能复合的数据写入 x，然后设置一个标志 y；线程1等待该标志然后写入另一个标志 z，线程2等待该标志然后读取数据；像往常一样，人们希望防止读取到数据的初始状态值（或其一部分）的可能性。

ISA2

[说明：此处原文为一张表格，展示了ISA2测试的伪代码版本。]

要使这项工作成功（即，禁止所述的最终状态），在线程0上有一个 DMB 或 sync 屏障（或 POWER lwsync）并且在线程1和2上保留依赖（线程1读/写对之间的地址、数据或控制依赖，以及线程2读/读对之间的地址或 control-isb/isync 依赖）就足够了。这些依赖可以被 DMB/sync/lwsync 替换。

ISA2+dmb/sync+addr+addr

[说明：此处原文为一张表格，展示了ISA2+dmb/sync+addr+addr测试的伪代码版本。]

这里可以认为线程0的屏障确保了线程0对 x=1 的写在屏障之前传播到线程1，这又在线程0对 y=1 的写传播到线程1之前，这又在线程1执行其对 z=1 的写之前。累积性，应用于在屏障之前的 x=1 的写和 z=1 的写（所有传播到或由线程1完成的），然后保持了 x=1 和 z=1 的写，就所有其他线程而言，是有序的，特别是就线程2而言。像往常一样，依赖只是防止了否则会使不期望结果微不足道地可能的局部重排序。

5.3 可观察行为

下面我们总结了这些累积性测试的硬件实验结果。

[说明：此处原文为一张表格，展示了WRC、ISA2及其变体测试在多种POWER和ARM处理器上的实验结果。]

这些测试涉及三个硬件线程，而我们能接触到的 Tegra2、APQ8060 和 A5X 实现只支持两个硬件线程。因此，对于 ARM 我们只给出 Tegra3 的结果。像以前一样，lwsync 变体没有 ARM 的类似物。

结果证实，禁止的结果是不可观察的。对于 WRC+addrs，POWER G5 和 ARM Tegra3 没有展现出架构上允许的可能性，而 POWER 6 和 POWER 7 则展现了。

6 存储缓冲 (SB) 或 Dekker 示例

我们现在转向一个相当不同的双线程示例，这是一个出现在某些互斥算法核心的模式。它有时被称为存储缓冲 (store-buffering) 示例（SB），因为这或多或少是在 x86 或 Sparc 的 TSO 模型中，通过它们的 FIFO（和可前递）存储缓冲可观察到的唯一松弛内存行为，有时也称为 Dekker 示例，因为它出现在他的互斥算法中。

该示例的双线程版本有两个共享位置，就像 MP 一样，但现在每个线程写入一个位置然后从另一个位置读取。问题是它们是否能都（在同一次执行中）从初始状态读取。

SB

[说明：此处原文为一张表格，并列展示了SB测试的伪代码、ARM汇编和POWER汇编版本。]

没有任何屏障或依赖，该结果是允许的，而且由于没有来自写的依赖，代码唯一可能的加强是插入屏障。在两个线程上都添加一个 DMB 或 sync 就足以排除不期望的结果：

SB+dmbs/syncs

[说明：此处原文为一张表格，并列展示了SB+dmbs/syncs测试的伪代码、ARM汇编和POWER汇编版本。]

这里的 dmb 或 sync 屏障确保了程序顺序上更早的写必须在读被满足之前传播到所有线程，排除了给定的执行。在 POWER 上，这里使用 lwsync 屏障是不够的（或者一个 lwsync 和一个 sync 屏障）：POWER lwsync 不确保屏障前的写在后续动作之前已传播到任何其他线程，尽管它确实保持了 lwsync 前后的写操作，就所有线程而言，是有序的。

6.1 将 SB 扩展到更多线程：IRIW 和 RWC

就像我们通过将第一个写剥离到一个新线程来扩展 MP 示例得到 WRC 示例一样，我们可以通过将一个或两个写剥离到新线程来扩展 SB。将两个都剥离出来，就得到了下面的独立读独立写 (Independent Reads of Independent Writes, IRIW) 示例（由 Lea 如此命名）。线程0和2分别写入 x 和 y；线程1先读 x 后读 y；线程3先读 y 后读 x。

IRIW

[说明：此处原文为一张表格，展示了IRIW测试的伪代码版本。]

这给了我们一个引人注目的例证，即写操作可以以不同顺序传播到不同线程：在下面的 IRIW+addrs 中（我们向读取线程添加依赖以排除读操作被局部重排序的琐碎执行），线程1看到了对 x 的写但没有看到对 y 的写，而线程3看到了对 y 的写但没有看到对 x 的写。

IRIW+addrs

[说明：此处原文为一张表格，展示了IRIW+addrs测试的伪代码版本。]

要排除这种行为，需要在两个读取线程上都使用一个 DMB 或 sync（lwsyncs 在这里不充分），就像 SB 测试一样：

IRIW+dmbs/syncs [说明：此处原文为一张图示和一张表格，展示了IRIW+dmbs/syncs测试的执行图和伪代码，表示该结果是禁止的。]

我们不知道 IRIW 作为一种自然的编程范式出现在任何情况中（如果有人知道，我们会很高兴听到），但当人们在像 ARM 和 POWER 这样高度松弛的模型之上实现一个高级语言内存模型时，这会是一个问题，也许该模型对 volatiles 或 atomics 具有顺序一致的行为。

只将 SB 的一个写剥离到一个新线程，就得到了 Boehm 和 Adve [BA08] 的 RWC（“读到写因果性 (read-to-write causality)”）示例：

RWC [说明：此处原文为一张图示和一张表格，展示了RWC测试的执行图和伪代码，表示该结果是允许的。]

这也需要两个 DMBs 或 syncs。

6.2 SB 的写操作变体：R 和 2+2W

通过将一个或两个读替换为写，可以得到 SB 的两种不同变体，类似于我们早先从 MP 得到 S 的方式，用相干性边代替从初始状态的读取。我们分别称这些测试家族为 R 和 2+2W。就像 IRIW 一样，它们主要是在 ARM 或 POWER 之上实现一个高级语言模型（必须支持任意高级语言程序）时才值得关注；我们尚不知道它们在自然编程范式中出现的情况。

R [说明：此处原文为一张图示和一张表格，展示了R测试的执行图和伪代码，表示该结果是允许的。]

2+2W [说明：此处原文为一张图示和一张表格，展示了2+2W测试的执行图和伪代码，表示该结果是允许的。]

就像 SB 一样，R 需要两个 DMBs 或 syncs 来排除指定的行为。2+2W 在 ARM 上需要两个 DMBs，但在 POWER 上两个 lwsyncs 就足够了。

6.3 可观察行为

[说明：此处原文为一张大型表格，详细展示了SB、IRIW、RWC、S、R、2+2W及其各种加屏障/依赖的变体测试，在多种POWER和ARM处理器上的实验结果。]

Tegra3 是我们目前能接触到的唯一一个四硬件线程实现，所以我们只对它显示 IRIW 和 RWC 的结果，并且没有 lwsync 测试的 ARM 类似物。

正如人们所希望的，被禁止的行为都是不可观察的。在某些情况下，被允许的行为并未被特定实现所展现：就像 WRC+addrs 一样，IRIW+addrs 测试在 POWER G5 或 ARM Tegra3 上是不可观察的，而 IRIW+lwsyncs 在 POWER G5 上也是不可观察的（结合之前的数据，这表明 POWER G5 和 POWER 6 是不可比较的：没有一个严格弱于或强于另一个）。

R+lwsync+sync 测试在这些 POWER 实现上都不可观察，这对于实现像 C/C++11 这样的高级语言模型特别有趣。正如我们在别处 [BMO+12] 解释的，一个早期在 POWER 上实现 C/C++11 并发原语的提议，隐含地假设 R+lwsync+sync 是被禁止的，在实现的某个点使用了一个 lwsync，这个用法对于我们迄今测试过的 POWER 实现是可靠的，但对于架构意图来说并不可靠。该提议后来已经更新。

7 加载缓冲 (LB) 示例

与存储缓冲相反的是下面的加载缓冲 (load-buffering, LB) 示例，其中两个线程首先分别从两个共享位置读取，然后写入到其他位置。两个读取都读取到另一个线程的写入的结果在 ARM 和 POWER 上是架构允许的，并且在当前的 ARM 处理器上是可观察的；我们没有在 POWER G5、POWER 6 或 POWER 7 上观察到它。

LB [说明：此处原文为一张表格，并列展示了LB测试的伪代码、ARM汇编和POWER汇编版本，以及一个表示该结果是允许的执行图。]

要禁止该结果，只需在两个线程上添加任何从读到写的依赖，或者一个 DMB、sync 或 lwsync 屏障，如下面的 LB+addrs 变体所示：

LB+addrs [说明：此处原文为一张表格，并列展示了LB+addrs测试的伪代码、ARM汇编和POWER汇编版本，以及一个表示该结果是禁止的执行图。]

或在下面的 LB+datas 和 LB+ctrls 变体中：

[说明：此处原文为两张表格，分别展示了 LB+datas 和 LB+ctrls 测试的伪代码，都表示结果是禁止的。]

所有这些都确保了两个写操作都不能在其程序顺序上更早的读操作被满足并提交之前被提交（并因此传播和对其他线程可见）。

7.1 可观察行为

[说明：此处原文为一张表格，展示了LB及其变体测试在多种POWER和ARM处理器上的实验结果。]

这里我们看到另一个实现比架构意图更严格的情况：这些 POWER 实现不展现 LB，而 ARM 实现则展现。这表明这些 POWER 实现不会在程序顺序上更早的读操作绑定其值并提交之前提交一个写操作（正如我们在第4.7节中为 S+sync+po 所看到的那样），而在 ARM 的情况下，当一个写被提交时，一个程序顺序上更早的读请求可能仍然是未完成的。

令人欣慰的是，正如 LB+datas 所说明的，没有一个架构允许值被凭空合成出来；这一直是 Java 和 C/C++11 高级语言模型设计中的一个关键关注点。

[说明：从第8节开始到第17节结束，原文包含大量复杂的执行图（石蕊测试图）和图表（测试周期表）。根据您的指示，这些复杂的图表将用文字提示并忽略，只翻译相关的解释性文本。]

8 相干性 (CoRR1, CoWW, CoRW1, CoWR, CoRW)

正如我们所见，ARM 和 POWER 远非顺序一致：人们不能假设在一个多线程程序的任何执行中，存在所有线程读写操作的某个顺序序列，该序列与每个线程的程序顺序一致，并且其中每个读都读取最近写的值。然而，如果我们将注意力仅限于对单个位置的读写，那么所有线程必须共享对这些读写的一致视图。实际上，在任何执行中，对于每个位置，存在一个对该位置所有写的单一线性顺序，所有线程都必须遵守。这个属性被称为相干性 (coherence)；我们用下面的例子来探索并精确说明我们所说的‘被所有线程遵守’的含义。

我们的第一个测试，CoRR1，下面以三种形式展示：左边是可读的类C伪代码，使用线程局部变量r1和r2以及一个共享变量x（初始为1），右边是最终的ARM和POWER版本（我们测试的版本），使用汇编语言。如果达到了指定的最终状态，r1=2且r2=1，那么线程1的第二次对x的读取必须来自初始状态，尽管第一次对x的读取看到了来自线程0对x=2的写入的值。那个写必须在相干性上晚于初始状态，所以这将违反相干性，并且该执行在ARM和POWER中都是被禁止的。像往常一样，同样代码的其他几种执行是允许的：线程1的两个读都可以读到1，或者都读到2，或者第一个读到1第二个读到2。这些只是代码的顺序一致的交错，没有暴露架构的任何松弛方面。

[说明：此处原文为一张表格和一张图示，展示了CoRR1测试的伪代码、汇编代码和执行图，表示该结果是禁止的。]

测试的两个小变体可能具有指导意义。在下面的 CoRR0 中，x的初始状态写是由线程0完成的，被禁止的结果仅仅是线程1以与其程序顺序相反的顺序看到了线程0的两个写。在下面的 CoRR2 中（像IRIW但只有一个共享位置，而不是两个），对x=1和x=2的两个写是由不同的线程完成的（都与读取线程不同），所以它们没有先天的顺序，但两个读取线程仍然必须以相同的顺序看到它们：禁止线程2看到2然后是1，而同一执行中线程3看到1然后是2。

[说明：此处原文为两张图示，分别展示了CoRR0和CoRR2测试的执行图，表示它们的结果都是禁止的。]

我们用 co 边表示对同一地址的写操作之间的相干性；在一个完整的执行中，对于每个地址，这些边必须形成一个全序。所有写操作都隐含地在相干性上晚于其地址的初始状态写。上面的图表演示了写a在相干性上先于写b的执行。

一个位置的相干性顺序可以通过两种方式进行实验观察。在简单的场景中，如果任何位置最多只有两个写操作，如此处所示，人们可以读取最终状态（在所有线程完成并有适当的屏障之后）。通常，可以有一个额外的线程（对每个位置）执行一系列读取，按顺序看到每个连续的值。例如，从写a（值为v1）到写b（值为v2）的co边意味着任何线程都不应该观察到x先取值v2后取值v1。

9 石蕊测试周期表

在看过了我们用来阐述各种松弛内存现象的所有石蕊测试之后，人们可能会问它们在某种意义上是否是完备的。我们现在展示它们可以被系统地处理，将它们组织成具有相似行为的测试家族的“周期表”，并给出一种感觉，即这涵盖了某些特定类型的所有“小”测试。这些表不包括所有有趣的测试；我们将在后面的部分回到其他一些测试。

9.1 石蕊测试家族

首先，我们定义一个石蕊测试家族为一个测试组的共同形态，由读写事件指定，每个线程的事件由程序顺序 po 边关联，每个位置的写事件由相干性 co 边关联，写与任何从它们读取的读由读自 rf 边关联。例如，MP测试：

[说明：此处原文为一张MP测试的执行图。]

也定义了一个相关测试的家族，所有都具有相同的形态，通过用依赖或屏障替换程序顺序边获得。我们一直使用的术语已经暗示了这一点，例如用 MP+dmb+addr 表示在线程0上有一个 dmb 屏障并且在线程1上有一个地址依赖（也许是人为的）的MP变体。

9.2 一个家族的最小增强

对于任何测试家族，人们可以问需要对其程序顺序（po）边进行哪些**最小增强 (minimal strengthenings)**才能禁止指定的执行。为了精确地说明这一点，回想一下，防止局部重排序的读到读依赖是地址和 control-isb（ARM）或 control-isync（POWER）依赖（对读的控制依赖不阻止读被推测性地满足，不能有对读的数据依赖，单独的 isb 或 isync 在这种情况下没有效果），而防止局部重排序的读到写依赖是地址、数据、控制或 control-isb/isync 依赖。我们定义符号：

RRdep ::= addr | ctrlisb/ctrlisync
RWdep ::= addr | data | ctrl | ctrlisb/ctrlisync

初步近似地，不同种类的 RRdep 和 RWdep 依赖的行为彼此相似（但见第10.5节的一个微妙例外）。ARM dmb 屏障和 POWER lwsync 及 sync 屏障都比那些依赖强，给出了一个顺序：

po < {RRdep,RWdep} < lwsync < dmb/sync

换句话说，用一个 RRdep 或 RWdep 依赖替换一个普通的程序顺序边，或用一个 lwsync 屏障替换它们中的一个，或用一个 dmb 或 sync 屏障替换它们中的任何一个，应该总是安全的（给出相同或更少的允许行为）。正如我们之前看到的，一个读到读的控制依赖没有强制力，（对于正常的内存访问）没有关联控制依赖的 isb/isync 也没有，所以用它们中的一个替换程序顺序边应该没有效果。

现在考虑从该家族的基本测试形态通过用 isync, addr, ctrlisync, lwsync, 或 sync 替换其程序顺序（po）边得到的所有 POWER MP 变体（ARM 会类似，除了没有 lwsync 并且用 dmb 代替 sync）。图1中的图表显示了每个变体，如果它禁止不期望的结果则为绿色，如果该结果被允许则为红色；箭头显示了上述的顺序。具有‘相似’依赖因此应该行为相似的测试被分组在蓝色框中。最小的绿色测试是 MP+lwsync+addr 和 MP+lwsync+ctrlisync，显示在 POWER 上要排除 MP 的不期望行为，至少需要在线程0上有一个 lwsync 并且在线程1上有一个地址或 control-isync 依赖。所有在这两个之上的测试也都是绿色的，表明在这种情况下我们的排序是有意义的。

[说明：此处原文为图1，一张复杂的流程图，展示了MP测试的各种变体及其允许/禁止状态，该图已忽略。]

9.3 4边双线程测试和RF扩展

我们现在更系统地审视我们的测试家族集合，给出每个家族的最小增强，如下表所示。我们到目前为止已经提到了几个家族，其中 MP、S、SB、R、2+2W 和 LB 都有两个线程、两个共享位置，以及每个线程上的两个读或写。此外，我们已经看到它们的几个三或四线程变体：RWC、WRC、ISA2 和 IRIW。我们也看到了几个相干性测试，但它们的特性略有不同；它们指定的执行在不需要任何依赖或屏障的情况下就被禁止，因此探索变体的兴趣较小。

看表，在左列我们看到那些双线程测试，按它们拥有的读自（rf）边的数量分组。在第一个块中，MP 和 S 是相似的：在 S 中，MP 从初始状态的读 d（相干性上先于写 a 到 x）被替换为一个相干性上先于 a 的写 d。它们在为防止不期望结果需要做什么方面也是相似的：MP 至少需要 lwsync/dmb 和一个读到读的依赖，而 S 至少需要 lwsync/dmb 和一个读到写的依赖。

接下来我们有三个没有 rf 边的测试：SB 及其变体 R 和 2+2W，它们分别将一个或两个最终的初始状态读替换为对 x 的写的相干性前驱的写。与第一组相反，SB 和 R 需要两个 syncs 或两个 dmbs；lwsync 在这里不充分。然而，对于最后一个变体 2+2W，即四个写的变体，lwsync 确实足够了。

最后是 LB 家族，有两个 rf 边。这里简单的依赖就足够了。

向右移动，第二和第三列是通过将一个或两个初始写“剥离”到新线程而从左列得到的测试。这里有几个奇特的变体，其中大多数（据我们所知）不是自然的用例，但它们包括了文献[BA08]中讨论的 WRC、IRIW 和 RWC 家族。值得注意的是，它们需要的增强与它们在第一列的基础测试完全相同：第一块中需要 lwsync/dmb 和一个依赖，SB 和 R 的扩展需要 syncs/dmbs，2+2W 的扩展需要 lwsyncs/dmbs；这就是屏障的累积性属性在起作用。

MP 家族可以在另一个维度上有用地变化，即考虑读之间的一系列依赖或其他边，如图中示意性地显示为 PPO（保留程序顺序）系列；我们将在第10节回到其中一些。

[说明：此处原文为一张大型图表，即“石蕊测试周期表”，系统地组织了各种2线程、3线程和4线程的石蕊测试。该图表已忽略。]

9.4 6边三线程测试

转向具有三个线程、三个共享位置以及每个线程两个读或写的测试，下面的表格显示了我们的11个家族。这里感兴趣的是：

  • ISA2: 我们在第5节中看到的消息传递到三个线程的推广，它只需要在第一个线程上有屏障；

  • 3.SB, 3.2W, 和 3.LB: SB, 2+2W, 和 LB 到三个线程的推广，它们需要的与双线程变体完全相同；以及

  • Z6.3: 它显示了在 POWER 上相干性和 lwsync 屏障的非传递性；我们将在第11节回到这一点。

我们期望 ISA2 在实践中是常见的，但很乐意听到其他家族的任何用例。

[说明：此处原文为一张大型图表，展示了11种6边3线程的石蕊测试家族。该图表已忽略。]

9.5 测试家族覆盖范围

显而易见的问题是，这些家族是否给出了在任何意义上都是完备的一组测试？人们可以尝试通过枚举所有达到一定规模（例如，线程数和每个线程指令数的某个界限）的多线程汇编程序来回答这个问题，但这很快就会产生难以处理的测试数量，其中许多将是无信息的。一个更好的方法是枚举所有达到一定规模（例如，最多四个线程和每个线程一定数量的读写动作）的家族。然而，仅仅枚举家族仍然包括许多无信息的测试，其中所讨论的执行在顺序一致模型中是允许的。因此，我们考虑由[SS88, Alg10, AMSS10]的**临界环 (critical cycles)生成的家族。为此，我们首先需要来自读的边 (from-reads edge)**的概念，由 Ahamad 等人 [ABJ+93] 引入（作为 reads-before 边），并由 Landin 等人 [LHH91] 引入（作为他们访问图中的一些边）。给定一个候选执行，及其读自关系（从每个写到所有从该写读取的读）和其相干关系（每个地址上写的某个线性顺序的并集），我们定义其来自读关系为有一条边从每个读到其读取的写的所有的相干性后继（或者，如果它从初始状态读取，则到该地址的所有写）。例如，考虑下面的候选执行，有5个写（可能由不同线程执行），按该相干顺序到x的1,…,5，以及一个从写b读取的读。b的相干性后继是写c, d, 和 e，所以我们构造一条从b到这些写中每一个的来自读的边。

[说明：此处原文为一张图示，解释了from-reads边的概念。]

我们可以用从该读到相同地址的写（们）的来自读的边替换从初始状态（到某个读）的读自边，而不会丢失任何信息。例如，对于MP和SB，我们有：

[说明：此处原文为一张对比图，展示了MP和SB测试用reads-from (rf)和from-reads (fr)边绘制的区别。]

注意右边的图在 rf, co, fr, 和 po 的并集中有环，实际上这样的环正是对顺序一致性的违反，如 [SS88, Alg10, AMSS10] 所示（也见 [LHH91] 中的定理5），所以通过枚举这样的环，我们可以精确地产生感兴趣的测试家族——潜在的非SC执行。

10 Preserved Program Order (PPO) Variations

我们现在探讨一些消息传递（MP）测试的进一步变体，这些变体阐明了一些关于架构在哪些情况下遵守（以及更重要的，不遵守）程序顺序的更微妙的点。

10.1 从rf;addr无写写依赖 (MP+nondep+dmb/sync)

在第4节中，我们看到了从读到读和写的依赖，但没有从写的‘依赖’。人们可能会认为，如果一个人向位置 x 写入一个值，然后在同一线程上读回它，然后有一个到另一个位置 y 的写的数据或地址依赖，那么这两个写就会就任何其他线程而言保持有序。事实并非如此，如下面的 MP+nondep+addr 示例所示：即使两个写可能必须按程序顺序提交，在没有任何屏障的情况下（并且因为它们是到不同地址的），它们仍然可以以任意顺序传播到其他线程。

[说明：此处原文为一张图示和一张表格，展示了MP+nondep+dmb/sync测试及其在多种处理器上的可观察性。]

10.2 无来自寄存器遮蔽的排序 (MP+dmb/sync+rs, LB+rs)

另一个可以想象的但未被架构遵守的排序来源是重用同一个处理器寄存器：硬件实现通常比架构的通用寄存器有更多的‘影子’寄存器，这些寄存器可以由机器码指令引用，并且硬件寄存器到架构寄存器的分配是动态完成的。这种寄存器重命名对程序员是可观察的，如下面两个例子所示。

首先，我们有一个 MP 的变体，它展现了可观察的寄存器遮蔽：线程1上对r3的两次使用并不妨碍第二次读取乱序满足，如果这些读取是到影子寄存器的（具体来说，线程1上对r3的前两次使用可能涉及一个影子寄存器，而第三次使用可能涉及另一个）。寄存器的重用在我们的图中没有表示，所以我们在标题中注明；细节只能在伪代码或测试的汇编版本中看到。

[说明：此处原文为一张图示和一张表格，展示了MP+sync+rs测试及其允许结果。]

同样，我们有一个 LB 的变体（取自 Adir 等人 [AAS03]），其中线程0上寄存器r1的重用不保持对x的读取和对y的写入的顺序。

[说明：此处原文为一张图示和一张表格，展示了LB+rs测试及其允许结果。]

在当前的实现中，MP+sync+rs 行为在 ARM 和 POWER 上都是可观察的，而 LB+rs 行为只在 ARM 上可观察，如下表所示。后者仅仅是因为基本的 LB 行为只在 ARM 上可观察（看起来当前的 POWER 实现不在有未完成的未提交读取的情况下提交写入）。尽管如此，两种行为在两种架构上都是架构允许的。

[说明：此处原文为一张表格，展示了LB+rs和MP+dmb/sync+rs测试在多种处理器上的实验结果。]

[从 10.3 到 17 的内容继续遵循只翻译文本，忽略复杂图示的原则]

10.3 保留程序顺序、推测和写前递 (PPOCA 和 PPOAA)

POWER 架构声明写操作不是推测性执行的，但我们在这里看到，虽然推测性写永远不会对其他线程可见，但它们可以被本地地前递到同一线程上程序顺序更晚的读；这种前递对程序员是可观察的。

在下面的 MP 的 PPOCA 变体中，f 地址依赖于 e，e 读取自写 d，而 d 控制依赖于 c。人们可能期望这条链会阻止读 f 在 c 之前绑定其值，但实际上在某些实现中 f 可以乱序绑定，如图所示——写 d 可以在线程内直接前递到 e，在写被提交到存储子系统之前，而 d、e 和 f 都仍然是推测性的（在 c 的控制依赖的分支解决之前）。

[说明：此处原文为一张图示，展示了 PPOCA 测试的执行图，结果为允许。]

用数据依赖替换控制依赖（测试 PPOAA，如下）消除了这种可能性，禁止了在当前硬件上给出的结果，据我们的实验结果显示，以及在我们的模型中。

[说明：此处原文为一张图示和一张表格，展示了 PPOAA 测试的执行图及其在多种处理器上的实验结果。]

10.4 激进的乱序读 (RSW 和 RDW)

鉴于第8节中关于相干性的讨论，人们可能期望对同一地址的两次读取必须按程序顺序被满足。通常是这样，但在两个读取恰好从同一个写中读取的特殊情况下（不仅仅是它们读取相同的值），则不是。

在下面的 MP 的 reads-from-same-writes (RSW) 变体中，对 x 的两次读取 d 和 e，恰好都从同一个写（初始状态）中读取。在这种情况下，尽管 d 和 e 是从同一地址读取，e/f 对可以乱序满足它们的读取，在 c/d 对之前，允许了所示的结果。e 的地址是已知的，所以它可以被提早满足，而 d 的地址直到其对 c 的地址依赖被解决后才为人所知。

[说明：此处原文为一张图示，展示了 RSW 测试的执行图，结果为允许。]

相比之下，在 d 和 e 从 x 的不同写中读取的相同代码的执行中（测试 RDW，如下），其中另一个线程对 x 有另一次写），这是被禁止的——在模型中，第一次读（d）的提交会强制第二次（e）及其依赖（包括f）的重启，如果 e 最初是从 d 的不同写中读取的。在实际实现中，重启可能会更早，当一个无效化被处理时，但会产生相同的可观察效果。

[说明：此处原文为一张图示和一张表格，展示了 RDW 测试的执行图及其在多种处理器上的实验结果。]

10.5 可能访问相同地址

到目前为止我们看到的例子中，对写的地址和数据依赖有相同的效果，阻止写在提供依赖值的指令被提交之前对其他线程可见。然而，可能会有一个二阶效应区分它们：对写的地址依赖的存在可能意味着另一个程序顺序更晚的写在不知道第一个写不是到相同地址之前不能继续，而对写的数据依赖对静态已知是到不同地址的程序顺序更晚的写没有这样的效果。这可以在下面 LB 测试的两个变体中看到。在这两个变体中，每个线程的中间都插入了对两个不同地址的额外写。在左边，这些写是地址依赖于第一个读，因此在这些读被满足之前，中间的写不知道它们与每个线程上最后的写是到不同的地址。在右边，中间的写仅仅是数据依赖于第一个读，所以它们静态地已知是到与每个线程上最后的写不同的地址。

[说明：此处原文为两张图示，对比了LB+addrs+WW和LB+datas+WW测试，前者被禁止，后者被允许。]

第一个在我们测试过的任何 ARM 实现（Tegra 2、Tegra 3、APQ8060、A5X）上都是不可观察的，而第二个在除了 APQ8060 之外的所有实现上都是可观察的。对于 POWER，回想一下我们没有在任何当前实现上观察到基本的 LB 行为，而这些变体也同样不出所料地是不可观察的。

[说明：此处原文为一张图示和一张表格，展示了相关测试及其在多种处理器上的实验结果。]

我们在 PLDI 2011 [SSA+11] 中给出的操作模型精确地匹配了这些观察，为每个测试给出了如上所示的‘禁止’或‘允许’状态。但一个架构模型是否应该允许或禁止它所禁止的两个，可能是值得商榷的。

10.6 可观察的读请求缓冲

我们最后一个例子是我们的 PLDI 2011 [SSA+11] 模型（在那里主要针对 POWER 测试）对于在 ARM（特别是 APQ8060）上可观察到的行为是不健全的一个案例，并且该行为在架构上是意图被允许的。

该测试是消息传递（MP）的另一个变体，写入端有一个强的 dmb 屏障。在读取端，对 y 的读取之后是对 y 的回写（必须是相干性更晚的值），然后是对该值的读取，最后是一个 control-isb 依赖于最终对 x 的读取。

control-isb 意味着对 x 的读 f 在对 y=2 的读 e 被提交之前不能被满足，而该读在它所读的写 d 被提交之前不能被提交。

在我们的 PLDI 2011 模型中，为了维持相干性，那个写 d 在程序顺序上可能到相同地址的更早的读和写被提交之前不能被提交，这阻塞了整个链条，确保了 f 在 c 之后被满足。

要看合法的硬件如何可能做到相反，假设对 c 的读请求被缓冲了。它可以继续对同一地址的写 d，让那个写被 e 读取并且 e 和 f 继续，只要硬件能保证读请求最终会被写 d 的一个相干性前驱所满足。如果读请求和写被缓冲在同一个每位置 FIFO 缓冲中，那自然会发生。

这可以在 PLDI 2011 模型的一个变体中通过允许写在稍微更宽松的情况下提交来适应。

[说明：此处原文为一张图示和一张表格，展示了相关测试及其在多种处理器上的实验结果。]

11 相干性与 lwsync (Z6.3+lwsync+lwsync+addr)

这个 POWER 示例（在我们早期的工作中称为 blw-w-006）表明，人们不能假设 lwsync 和相干性边的传递闭包能保证写对的排序，这对过于简化的模型是一个挑战。在我们的抽象机中，存储子系统提交 b 在相干顺序上先于 c 这一事实，对写 a 和 d 传播到线程2的顺序没有影响。线程1不从任何一个线程0的写中读取，所以它们不需要被发送到线程1，所以没有累积性在起作用。换句话说，相干性边不会将写带入 POWER 屏障的“A组”。

[说明：此处原文为一张图示和一张表格，展示了相关测试及其在POWER处理器上的实验结果。]

在某些实现中，以及在我们的模型中，用 syncs 替换两个 lwsyncs 会禁止这种行为。ARM 没有 lwsync 的类似物，所以那里没有这个例子的类似物。

12 不可观察的互连拓扑 (IRIW+addrs-twice)

我们在第6.1节中看到的 IRIW+addrs 行为的一个直接的微架构解释是，存在一个存储层次结构，其中线程0和1是“邻居”，能够比其他线程更早地看到彼此的写，同样线程2和3是“邻居”。

然而，实际上，在一些当前的 POWER 机器上，IRIW+addrs-twice 行为是可观察的（在微架构上，虽然它们确实有一个存储层次结构 [LSF+07, KSSF10]，但仅缓存协议行为就足以给出观察到的行为，并且线程在某些情况下也可以被虚拟机监视器重新分配）。此外，对于架构来说，不要求在程序开始执行前就固定一个单一的拓扑是可取的：就正确性而言，硬件线程都应该是可互换的。如果程序员通过像 IRIW+addrs-twice 或其他测试来学习互连拓扑，并用它来在他们的代码中做选择，他们不应该期望一致和可预测的行为。

[说明：此处原文为一张图示和一张表格，展示了相关测试及其在POWER处理器上的实验结果。]

13 加载-保留/存储-条件

加载-保留/存储-条件原语由 Jensen 等人 [JHB87] 作为比较并交换（CAS）指令的 RISC 架构替代品引入；它们自1992年以来已在 PowerPC 架构上使用，并且也存在于 ARM、MIPS 和 Alpha 中。它们也被称为加载-链接/存储-条件（LL/SC），或者在 ARM 上，加载-独占/存储-独占。它们提供了一种简单的乐观并发形式（非常粗略地说，是单个位置上的乐观事务）。

Herlihy [Her93] 使用加载-保留/存储-条件来实现各种无等待和无锁算法，注意到（对于 CAS 也是如此，但不同于 test-and-set 和 fetch-and-add）它在共识数方面是通用的，而且加载-保留/存储-条件在实践中优于 CAS，因为它能防御 ABA 问题。

我们将通过下面的序列来说明加载-保留/存储-条件的属性，该序列实现了一个原子加法操作。第一个序列是伪代码，后面是 ARM 汇编和 POWER 汇编。

[说明：此处原文为一张表格，并列展示了原子加法操作的伪代码、ARM汇编和POWER汇编版本。]

让我们通过各个组件来理解上面的代码。加载-保留从某个内存地址加载，并为加载线程在该地址上建立一个保留 (reservation)。后续对同一地址的存储-条件将成功或失败。此外，存储-条件会设置一个标志，以便后续指令可以确定它是否成功；加载-保留/存储-条件对通常会重复直到成功。注意，在加载-保留和存储-条件之间允许有其他操作，包括内存读写，尽管与事务不同，如果存储-条件失败，没有任何东西会被回滚。

那么存储-条件何时能成功，何时必须失败？加载-保留和存储-条件通常如上成对使用。它们必须共同确保的关键属性是，如果存储-条件成功，其对应的存储必须紧接着加载-保留所读自的存储。回顾相干性，关键条件是成功的存储-条件的存储必须（在相干顺序上）紧接着紧邻的前一个加载-保留所读自的存储。此外，这种情况不应该随着系统的演进而改变（不应该有其他写能插进来）。一个微妙之处是 POWER 允许来自同一线程（与加载-保留和存储-条件相同的线程）的存储出现在上述两个存储之间的相干顺序中。这只能通过程序顺序上在加载-保留和存储-条件之间的对同一位置的干预存储来实现。

如果这个相干性条件是可能的，存储-条件就可以成功，如果它不再可能（例如，如果另一个对同一地址的写传播到该线程，在读自的写和存储-条件的写之间，这意味着第三个写必须成为相干性上在这两者之间的），它就必须失败。另请注意，这仅仅是可能成功的条件，存储-条件可能会伪失败 (spuriously fail)，因此在理论上使得任何关于前进或公平性的强保证都变得不可能，尽管在实践中这可能不是一个问题。

14 Peterson 算法在 POWER 上的分析

下面的伪代码是 Peterson 互斥算法 [Pet81] 的一个简化。所呈现的代码侧重于互斥，通过只呈现“加锁”片段——线程0（相应地，线程1）会通过向标志变量f0（相应地，f1）写入0来执行解锁；并通过简化这个加锁片段。实际上，在实际算法中，最后的 if 条件被一个 while 循环所取代，其条件是所呈现的最终条件的否定。例如，实际加锁片段的线程0代码可能以“while (f1 == 1 && vict == 0);”结尾。

[说明：此处原文为一张表格，展示了Peterson算法（PET）的简化伪代码。]

上述最终条件 crit0=1 ∧ crit1=1 表示互斥：如果在测试结束时 crit0 和 crit1 都持有值1，那么我们就目睹了互斥的失败。

由于布尔连接符 || 的标准短路编译，如果 crit0 持有值1，那么要么：

(1) 线程0从位置f1读取了值0，或者 (2) 线程0从位置f1读取了值1，然后从位置vict读取了值1。

类似地，如果 crit1 持有值1，那么要么：

(3) 线程1从位置f0读取了值0，或者 (4) 线程1从位置f0读取了值1，然后从位置vict读取了值0。

通常，Peterson算法正确性的证明会检查一方面(1)或(2)与另一方面(3)或(4)的任何两个条件的合取都会导致矛盾。这样的“矛盾”可以被解释为对顺序一致性的违反，正如我们所讨论的。

通过 uniproc 保证互斥

我们首先考虑 Peterson 算法改进了一个只考虑标志f0和f1的琐碎互斥算法的情况。更精确地说，如果两个线程都在对方的标志中读取到值1，那么获胜者是通过让每个线程读取 vict 来选择的，认为 vict 有一个指定竞争失败者的确定值。确实，在 POWER 上，我们不能同时拥有(2)和(4)，根据 uniproc 条件（见第9.6节）。

互斥失败，SB风格

我们现在考虑(1)和(3)同时成立的情况。也就是说，线程0从f1读取值0，而线程1从f0读取值0。

这种情况的特点是 SB（或 Dekker）测试的环路。因此，所描绘的执行在 POWER 架构上是允许的，就像 SB 测试一样。

互斥失败，R风格

我们现在考虑(1)和(4)同时成立的情况。也就是说，线程0从f1读取值0，而线程1从f0读取值1但被授予进入互斥区的权利，通过从vict读取0。

这些环是R风格的，它们在POWER上是允许和可观察的。

用栅栏确保互斥

为了恢复互斥，足以禁止前几节中描述的 SB 和 R 风格的顺序一致性违规。由于 SB+syncs 和 R+syncs 测试在 POWER 上是被禁止的，因此在每个线程代码中插入两个 sync 栅栏就足够了，一个在存储到标志f0或f1之后，一个在存储到 vict 之后。

15 测试来源及其对应关系

我们的几个测试是取自或改编自文献，如下所述。

15.1 Boehm 和 Adve 示例

Boehm 和 Adve [BA08] 在类C伪代码中给出了四个主要测试，使用了一个 fence 语句。将其视为 POWER sync 或 ARM DMB 屏障，它们对应于这里的测试如下：

  • IRIW [BA08, Fig. 4]: IRIW+dmbs/syncs

  • WRC [BA08, Fig. 5]: WRC+dmbs/syncs

  • RWC [BA08, Fig. 6]: RWC+dmbs/syncs

  • CC [BA08, Fig. 7]: 我们不讨论

15.2 ARM Cookbook 示例

我们的测试与 ARM Barrier Litmus Tests and Cookbook 文档 [ARM08b] 第6节示例的对应关系如下。我们以后者的节号标记后者为 ARMC6.1 等。

  • ARMC6.1 Simple Weakly Consistent Ordering Example 是 SB。

  • ARMC6.2.1 Weakly-Ordered Message Passing problem 是 MP。

  • ARMC6.2.1.1 Resolving by the addition of barriers 是 MP+dmbs。

  • ARMC6.2.1.2 Resolving by the use of barriers and address dependency. 主要示例是 MP+dmb+addr。

15.3 Power2.06 ISA 示例

Power2.06 ISA [Pow09] Book II Chapter 1 只有两个例子，在§1.7.1中，旨在说明A-和B-累积性。第一个是 WRC+syncs 的一个变体。第二个是一个迭代消息传递示例；我们的 ISA2+sync+data+addr 是一个类似的但无循环的测试。

15.4 Adir 等人示例

我们的测试与 Adir, Attiya, 和 Shurek [AAS03]（我们标记为 AdirNNN）的测试的对应关系如下。

  • Adir1 是 MP+syncs 示例。

  • Adir4 是一个在存储之间有 sync 且在加载之间有控制依赖的消息传递示例，显示了加载之间的控制依赖不被遵守，如在 MP+sync+ctrl 中。

  • Adir6 显示了寄存器的多副本对程序员是可见的；这里是 LB+rs 测试。

15.5 Adve 和 Gharachorloo 示例

来自 [AG96]:

  • Fig. 4(a), Fig. 5(a) SB

  • Fig. 4(b), Fig. 10(b) WRC

  • Fig. 5(b,c) MP

16 相关工作

关于松弛内存模型已有广泛的先前工作，我们在此仅回顾一些关于不具有顺序一致行为的主要当前处理器家族的模型：Sparc、x86、Itanium、ARM 和 POWER。Collier [Col92] 的早期工作基于对当时多处理器的经验测试开发了模型。对于Sparc，供应商文档有一个清晰的Total Store Ordering (TSO)模型[SFC91, Spa92]。对于x86，供应商的意图直到最近都相当不清楚，处理器实现的行为也是如此。Sarkar, Owens等人的工作[SSZN+09, OSS09, SSO+10]表明，对于正常的 用户或系统代码，它们也是TSO。这与我们在这里描述的工作精神相似，有一个被经验观察测试过的机械化语义。对于POWER，已经有几个先前的模型，但没有一个能满足对现实并发代码进行推理的需求。部分原因是架构随着时间发生了变化：lwsync 屏障被添加，屏障现在是累积的。

17 在线材料

各种支持材料可在线获取：http://www.cl.cam.ac.uk/~pes20/ppc-supplemental

  • 有描述 POWER 的操作性抽象机模型及其对加载-保留/存储-条件和 eieio 指令扩展的论文：

    • Understanding POWER multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. In Proc. PLDI, 2011. [SSA+11]

    • Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. In Proc. PLDI, 2012. [SMO+12]

  • 我们的 ppcmem 工具让人们可以交互式地探索 POWER 或 ARM 石蕊测试在我们模型下的行为；这通过一个网页界面提供：http://www.cl.cam.ac.uk/~pes20/ppcmem。ppcmem 的使用在 McKenney [McK11] 的一篇 Linux Weekly News (LWN) 文章中有描述。

  • 我们的 litmus 工具接受一个石蕊测试并构建一个测试工具（作为一个带有嵌入式汇编的C程序）来实验性地测试其可观察行为。这可以从 http://diy.inria.fr 下载，其中也包括我们用于从简洁规范生成石蕊测试的 diy 工具。litmus 工具在以下论文中有描述：

    • Litmus: running tests against hardware. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. In Proc. TACAS, 2011. [AMSS11b]

  • 测试和实验结果的摘要。

致谢 我们感谢 EPSRC 拨款 EP/F036345, EP/H005633, 和 EP/H027351，以及 ANR 项目 WMC (ANR-11-JS02-011) 的资助。

[说明：最后的参考文献部分（References）为标准学术引用格式，此处省略其翻译。]