理解 POWER 多处理器

标题：Understanding POWER Multiprocessors

日期：2011/06/04

作者：Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams

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

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

摘要

要利用当今的多处理器，就需要高性能且正确的并发系统代码（例如优化编译器、语言运行时、操作系统内核等），而这反过来又要求对可依赖的、可观察的处理器行为有很好的理解。然而，不幸的是，对于几种当前的多处理器而言，这个关键的硬件/软件接口并不清晰。

在本文中，我们描述了 IBM POWER 多处理器的行为特征，它们具有一种微妙且高度宽松的内存模型（ARM 多处理器在这方面有非常相似的架构）。我们对几代处理器进行了广泛的实验：POWER G5、5、6 和 7。基于这些实验、已发布的微架构细节以及与 IBM 员工的讨论，我们给出了一个抽象机语义，该语义从大部分实现细节中抽象出来，但能解释一系列微妙示例的行为。我们的语义用散文解释，但在严格的、可由机器处理的数学中定义；我们还通过一个可执行的检查器确认，它为我们的示例捕获了可观察的处理器行为或架构意图。虽然未经供应商官方认可，但我们相信该模型为推理当前的 POWER 多处理器提供了一个合理的基础。

我们的工作应该为这些架构上的并发系统编程带来新的清晰度，并且是任何分析或验证的必要前提。它也应该为像 C 和 C++ 这样的语言设计提供信息，在这些语言中，内存模型受到可以高效编译到此类多处理器上的能力的约束。

类别和主题描述符 C.1.2 [多数据流架构 (多处理器)]: 并行处理器; D.1.3 [并发编程]: 并行编程; F.3.1 [程序的规约、验证和推理]

通用术语 文档、语言、可靠性、标准化、理论、验证

关键词 宽松内存模型、语义

1. 引言

多年来，Power 多处理器（包括 IBM POWER 5、6、7 以及各种 PowerPC 实现）一直采用激进的实现方式，提供高性能，但也暴露了一个非常宽松的内存模型，这要求在并发代码中谨慎使用依赖关系和内存屏障来强制执行顺序。人们可能先验地期望，多处理器的行为会由供应商的架构文档，在这里是 Power ISA v2.06 规范 [Pow09]，进行足够好的定义。对于指令的顺序行为，这通常是正确的。然而，对于并发代码，Power 多处理器的可观察行为是极其微妙的，正如我们将看到的，供应商规范给出的保证并不总是清晰。因此，我们着手发现实际的处理器行为，并定义一个严谨且可用的语义，作为未来系统构建和研究的基础。

这些多处理器的程序员可观察的宽松内存行为，是从一个复杂的微架构 [SKT+05, LSF+07, KSSF10] 中涌现出的一个全系统属性。这在不同代际之间可能会有显著变化，例如从 POWER 6 到 POWER 7，但其包括：执行乱序和推测性执行的核心，带有许多影子寄存器；分层的存储缓冲，其中一些缓冲在对称多线程（SMT）核心的线程之间共享，并具有多级缓存；按地址分区的存储缓冲；以及具有许多缓存行状态和复杂互连拓扑的缓存协议，其中缓存行失效消息是缓冲的。一致性内存和内存屏障的实现涉及所有这些部分的协同工作。为了制作一个有用的模型，必须从尽可能多的复杂性中抽象出来，这既是为了让模型足够简单易懂，也是因为详细的硬件设计是专有的（已发表的文献没有足够详细地描述微架构以自信地预测所有可观察的行为）。当然，模型还必须是可靠的（sound），允许硬件实际表现出的所有行为，并且足够强大（strong），捕获系统程序员所依赖的硬件提供的任何保证。它不必是紧凑的（tight）：做一个宽松的规范可能是可取的，允许一些当前硬件不表现出的行为，但程序员并不依赖其不存在，这可能是为了简化或为了接纳未来的不同实现。模型不必在细节上与硬件的内部结构相对应：我们正在捕获合理实现的外部行为，而不是实现本身。但它应该与实现微架构有一个清晰的抽象关系，以便模型能真正解释示例的行为。

为了开发我们的模型，并建立对其可靠性的信心，我们进行了广泛的实验，在几代处理器上运行了数千个测试，包括手写的和自动生成的，每个测试迭代次数高达 10¹¹ 次。我们在第 2 节中介绍一些简单的测试，以引入 Power 所允许的宽松行为。

（接第一页）…以及在第 6 节中一些更微妙的示例，并在第 7 节中提供代表性的实验数据。为了确保我们的模型以一种忠实地从实际硬件中抽象出来的方式解释测试行为，并使用适当的概念，我们依赖于与 IBM 员工的广泛讨论。为了根据实验验证模型，我们构建了一个检查器，该检查器基于从数学定义自动生成的代码，来计算测试的允许结果（第 8 节）；这证实了对于我们描述的所有测试以及一个系统生成的包含约 300 个其他测试的家族，该模型都给出了正确的结果。

宽松内存模型通常以公理化（axiomatic）或操作化（operational）的风格来表达。在这里，我们采用后者，在第 3 节和第 4 节中定义一个抽象机。我们期望这比典型的公理化模型更直观，因为它有一个直观的全局时间概念（在抽象机转换的轨迹中），并且从实际硬件的抽象更为直接。更具体地说，为了解释一些示例，似乎有必要明确地对乱序和推测性读取进行建模，这在抽象机设置中更容易做到。这项工作旨在制作一个尽可能简单但又不过于简单的模型：该模型比某些模型（例如用于 TSO 处理器如 Sparc 和 x86）要复杂得多，但它确实捕获了一系列微妙示例的处理器行为或架构意图。此外，虽然定义在数学上是严谨的，但它只需几页散文即可解释清楚，因此对于必须关注这些问题的专家级系统程序员（并发库、语言运行时、优化编译器等的开发者）来说，它应该是易于理解的。我们最后讨论了相关工作（第 9 节）和未来方向的简要总结（第 10 节），最后回到供应商架构。

2. 简单示例

我们首先通过示例非正式地介绍 Power 多处理器的行为，引入一些关键概念，但将模型的解释留到后面。

2.1 宽松行为

在没有内存屏障或依赖关系的情况下，Power 多处理器表现出一种非常宽松的内存模型，如下面四个经典测试的行为所示。

SB: Store Buffering (存储缓冲) 这里，两个线程写入共享内存位置，然后各自读取另一个位置——这是 Dekker 互斥算法核心的一个惯用法。在伪代码中：

线程 0

线程 1

x=1

y=1

r1=y

r2=x

初始共享状态: x=0 and y=0 允许的最终状态: r1=0 and r2=0

在指定的执行中，两个线程都从初始状态读取值（在后面的示例中，除非另有说明，否则初始值均为零）。为了消除关于究竟执行了哪些机器指令的任何歧义，无论是来自源语言语义还是编译问题，我们都将我们示例的权威版本视为 PowerPC 汇编（可在线获取 [SSA+11]），而不是伪代码。然而，汇编代码不易阅读，所以我们在这里将示例呈现为图表，展示了由初始和最终状态约束指定的执行中所涉及的内存读写事件。在此示例中，伪代码 r1 和 r2 代表机器寄存器，因此对它们的访问不是内存事件；在指定的最终状态下，唯一可行的执行有两个写操作（标记为 a 和 c）和两个读操作（标记为 b 和 d），其值如下。它们通过程序顺序 po（program order，稍后我们将省略隐含的 po 边）相关联，两个读都从初始状态（0）读取的事实由传入的“读自”（reads-from，rf）边表示（从写操作指向读取它们的读操作）；点表示初始状态的写。

图表内容描述: Test SB: Allowed (测试 SB：允许)

  • 线程 0:

    • a: W[x]=1 (写 x=1)

    • po (程序顺序)

    • b: R[y]=0 (读 y=0)，有一条 rf 边从初始状态的 y 指向它。

  • 线程 1:

    • c: W[y]=1 (写 y=1)

    • po

    • d: R[x]=0 (读 x=0)，有一条 rf 边从初始状态的 x 指向它。

这个例子说明了在 Sparc 或 x86 TSO 模型 [Spa92, SSO+10] 中允许的关键松弛。接下来的三个例子展示了 Power 提供更弱模型的一些方式。

MP: Message passing (消息传递) 这里线程 0 写入数据 x，然后设置一个标志 y，而线程 1 读取该标志 y 的写，然后读取 x。在 Power 上，该读取不保证能看到线程 0 对 x 的写；它可能反而会读到该写操作“之前”的值，尽管存在 po 和 rf 边的链条：

图表内容描述: Test MP: Allowed (测试 MP：允许)

  • 线程 0:

    • a: W[x]=1

    • po

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1，有一条 rf 边从 b: W[y]=1 指向它。

    • po

    • d: R[x]=0，有一条 rf 边从初始状态的 x 指向它。

在真实代码中，对 y 的读取 c 可能在一个循环中，重复进行直到读取到值为 1。这里，为了简化实验测试，我们没有循环，而是只考虑那些读取值为 1 的执行，这通过对测试源中最终寄存器值的约束来表达。

WRC: Write-to-Read Causality (写到读的因果性) 这里线程 0 通过写入 x=1 与线程 1 通信。线程 1 读取到该值，然后在程序顺序的后面通过写入 y 向线程 2 发送消息。在线程 2 读取到 y 的写之后，问题是，程序顺序后续在线程 2 对 x 的读取是否保证能看到线程 0 写入的值，还是可能读到“之前”的值，如下图所示，同样是尽管存在 rf 和 po 链。在 Power 上这是可能的。

图表内容描述: Test WRC: Allowed (测试 WRC：允许)

  • 线程 0: a: W[x]=1

  • 线程 1:

    • b: R[x]=1，rf 边从 a 指向 b。

    • po

    • c: W[y]=1

  • 线程 2:

    • d: R[y]=1，rf 边从 c 指向 d。

    • po

    • e: R[x]=0，rf 边从初始状态的 x 指向 e。

IRIW: Independent Reads of Independent Writes (独立读的独立写) 这里两个线程（0 和 2）写入不同的位置，而另外两个线程（1 和 3）各自从这两个位置读取。在指定的允许执行中，它们以不同的顺序看到这两个写（线程 1 的第一个读看到了对 x 的写，但程序顺序后续的读没有看到对 y 的写，而线程 3 看到了对 y 的写，但没有看到对 x 的写）。

图表内容描述: Test IRIW: Allowed (测试 IRIW：允许)

  • 线程 0: a: W[x]=1

  • 线程 2: d: W[y]=1

  • 线程 1:

    • b: R[x]=1，rf 边从 a 指向 b。

    • po

    • c: R[y]=0，rf 边从初始状态的 y 指向 c。

  • 线程 3:

    • e: R[y]=1，rf 边从 d 指向 e。

    • po

    • f: R[x]=0，rf 边从初始状态的 x 指向 f。

Coherence (一致性) 尽管有上述所有情况，但我们确实得到了一个一致性的保证：在任何执行中，对于每个位置，所有（来自任何处理器的）对该位置的写操作都有一个单一的线性顺序（coherence order，co），所有线程都必须遵守这个顺序。下面的四个案例说明了这一点：一个线程的一对读不能与一致性顺序相反地读取（CoRR1）；一个线程的一对写操作的一致性顺序必须尊重程序顺序（CoWW）；一个读不能从一个被另一个程序顺序先于该读的写所“一致性隐藏”的写中读取（CoWR），并且一个写不能在一致性顺序上先于一个被程序顺序先于该写的读所读取的写。我们现在可以澄清上面 MP 和 WRC 讨论中的“之前”的含义，即相对于 x 的一致性顺序。

图表内容描述: 以下四个测试均为 Forbidden (禁止)

  1. Test CoRR1:

    • 线程 0: a: W[x]=1

    • 线程 1:

      • b: R[x]=1，rf 边从 a 指向 b。

      • po

      • c: R[x]=0，rf 边从初始状态指向 c。

  2. Test CoWW:

    • 线程 0:

      • a: W[x]=1

      • po

      • b: W[x]=2

    • 存在一条 co 边从 b 指向 a。

  3. Test CoWR:

    • 线程 0:

      • a: W[x]=1

      • po

      • b: R[x]=2，rf 边从 c 指向 b。

    • 线程 1: c: W[x]=2

    • 存在一条 co 边从 a 指向 c。

  4. Test CoRW:

    • 线程 0:

      • a: R[x]=2，rf 边从 c 指向 a。

      • po

      • b: W[x]=1

    • 线程 1: c: W[x]=2

    • 存在一条 co 边从 b 指向 c。

2.2 强制执行顺序

Power ISA 提供了几种强制更强顺序的方法。这里我们讨论 sync（重量级同步，或 hwsync）和 lwsync（轻量级同步）屏障指令，以及依赖关系和 isync 指令，将 load-reserve/store-conditional 对和 eieio 留待未来工作。

使用 sync 恢复顺序一致性 (SC) 如果在每对程序顺序的指令之间添加一个 sync（创建测试 SB+syncs, MP+syncs, WRC+syncs, 和 IRIW+syncs），那么上面所有非 SC 的结果都被禁止，例如：

图表内容描述: Test MP+syncs: Forbidden (测试 MP+syncs：禁止)

  • 线程 0:

    • a: W[x]=1

    • sync

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1

    • sync

    • d: R[x]=0

  • rf 边连接 b 和 c，rf 边从初始状态指向 d。

使用依赖关系 屏障可能会带来显著的运行时成本，在某些情况下，仅仅通过存在从内存读到另一个内存访问的依赖关系就足以保证足够的顺序。存在多种依赖关系：

  • 地址依赖 (addr)：从一个读操作到一个程序顺序后续的内存读或写操作存在地址依赖，如果存在一个数据流路径从该读操作，通过寄存器和算术/逻辑运算（但不通过其他内存访问），到第二个读或写的地址。

  • 数据依赖 (data)：从一个读操作到一个内存写操作存在数据依赖，如果存在这样一个路径到被写入的值。地址和数据依赖的行为相似。

  • 控制依赖 (ctrl)：从一个读操作到一个内存写操作存在控制依赖，如果存在这样一个数据流路径到一个条件分支的测试，该分支是该写操作的程序顺序前驱。我们也指从读到读的控制依赖，但在那种情况下，读的顺序通常不受尊重。

  • 控制+isync 依赖 (ctrlisync)：从一个读操作到另一个内存读操作存在控制+isync依赖，如果存在这样一个数据流路径，从第一个读到条件分支的测试，该分支程序顺序上先于一个 isync 指令，而该 isync 指令又在第二个读之前。

有时人们可以使用算法中自然存在的依赖关系，但有时为了其排序属性而人为引入一个依赖关系也是可取的，例如，通过将一个值与自身进行异或（XOR）运算，然后将其加到地址计算中。

仅有依赖关系通常是不够的。例如，在读/读和读/写对之间添加依赖关系，得到测试 WRC+data+addr（在线程 1 上有数据依赖，在线程 2 上有地址依赖）和 IRIW+addrs（在线程 1 和 3 上有地址依赖），非 SC 行为仍然是允许的。人们不能向 SB 添加依赖关系，因为它只有写/读对，而人们只能在 MP 的读/读侧添加依赖关系，使得写操作不受约束，非 SC 行为仍然存在。

然而，与屏障结合使用时，依赖关系可能非常有用。例如，MP+sync+addr 是 SC 的：

图表内容描述: Test MP+sync+addr: Forbidden (测试 MP+sync+addr：禁止)

  • 线程 0:

    • a: W[x]=1

    • sync

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1，rf 边从 b 指向 c。

    • addr

    • d: R[x]=0，rf 边从初始状态指向 d。

这里，屏障保持了写操作的顺序（从任何线程看），而地址依赖保持了读操作的顺序。

与人们可能预期的相反，线程局部的 reads-from 边和依赖关系的组合并不能保证另一个线程看到的写-写对的顺序；这两个写可以以任一顺序传播（这里 [x]=z 最初）：

图表内容描述: Test MP+nondep+sync: Allowed (测试 MP+nondep+sync：允许)

  • 线程 0:

    • a: W[x]=y

    • rf

    • b: R[x]=y

    • addr

    • c: W[y]=1

  • 线程 1:

    • d: R[y]=1，rf 边从 c 指向 d。

    • sync

    • e: R[x]=z，rf 边从初始状态指向 e。

控制依赖、可观察的推测性读和 isync 回想一下，控制依赖（没有 isync）只在从读到写时被遵守，而不是从读到读。如果在 MP+sync+addr 中用一个到条件分支的数据流路径替换地址依赖（得到下面名为 MP+sync+ctrl 的测试），这并不能确保线程 1 上的读按程序顺序绑定它们的值。

图表内容描述: Test MP+sync+ctrl: Allowed (测试 MP+sync+ctrl：允许)

  • 线程 0:

    • a: W[x]=1

    • sync

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1，rf 边从 b 指向 c。

    • ctrl

    • d: R[x]=0，rf 边从初始状态指向 d。

在分支和第二个读之间添加一个 isync 指令（得到测试 MP+sync+ctrlisync）就足够了。

数据/地址依赖对读和写都有效，而控制依赖只对写有效，这一事实在 C++0x 低级原子操作的设计 [BA08, BOS+11] 中很重要，其中 release/consume 原子操作让人们可以利用数据依赖的优势而无需屏障（并限制优化），以确保所有源语言的控制依赖都得到尊重。

Cumulativity (累积性) 对于 WRC，在线程 1 上放置一个 sync 并在线程 2 上放置一个依赖就足够了；非 SC 行为随即被禁止：

图表内容描述: Test WRC+sync+addr: Forbidden (测试 WRC+sync+addr：禁止)

  • 线程 0: a: W[x]=1

  • 线程 1:

    • b: R[x]=1，rf 边从 a 指向 b。

    • sync

    • c: W[y]=1

  • 线程 2:

    • d: R[y]=1，rf 边从 c 指向 d。

    • addr

    • e: R[x]=0，rf 边从初始状态指向 e。

这说明了我们称之为 Power 屏障的 A-累积性：一个在屏障之前的边链是受尊重的。在这种情况下，线程 1 在执行 sync 之前（按程序顺序）从线程 0 的写中读取，然后线程 1 写入另一个位置；任何其他线程（这里是 2）都保证在看到线程 1 的写之前看到线程 0 的写。然而，交换 sync 和依赖的位置，例如，仅用一个 rf 和 data 边连接写 a 和 c，并不能保证其他线程看到的这些写的顺序：

图表内容描述: Test WRC+data+sync: Allowed (测试 WRC+data+sync：允许)

  • 线程 0: a: W[x]=1

  • 线程 1:

    • b: R[x]=1，rf 边从 a 指向 b。

    • data

    • c: W[y]=1

  • 线程 2:

    • d: R[y]=1，rf 边从 c 指向 d。

    • sync

    • e: R[x]=0，rf 边从初始状态指向 e。

与 WRC+data+sync 相比，一个在 sync 之后的 reads-from 边和依赖的链确实能确保一个在 sync 之前的写和一个在 sync 之后的写之间的顺序得到尊重，如下所示。这里，对 z 和 x 的读 e 和 f 不能乱序地看到写 a 和 d。我们称之为一个 B-累积性 属性。

图表内容描述: Test ISA2+sync+data+addr: Forbidden (测试 ISA2+sync+data+addr：禁止)

  • 线程 0: a: W[x]=1

  • 线程 1:

    • b: W[y]=1

    • sync

    • c: R[y]=1，rf 边从 b 指向 c。

    • data

    • d: W[z]=1

  • 线程 2:

    • e: R[z]=1，rf 边从 d 指向 e。

    • addr

    • f: R[x]=0，rf 边从初始状态指向 f。

使用 lwsync lwsync 屏障与 sync 大致相似，包括累积性属性，但它不排序 store/load 对，且执行成本更低；它足以在 MP+lwsyncs（每个线程都有 lwsync 的 MP）、WRC+lwsync+addr（WRC 在线程 1 有 lwsync，在线程 2 有地址依赖）和 ISA2+lwsync+data+addr 中保证 SC 行为，而 SB+lwsyncs 和 IRIW+lwsyncs 仍然是允许的。我们稍后会回到 sync 和 lwsync 之间的其他差异。

3. 模型设计

在本节中，我们描述我们模型的高级设计，下一节将给出细节。我们将模型构建为一组（硬件）线程和一个单一的存储子系统的组合，它们通过各种消息进行同步。

图表内容描述: 一个示意图展示了多个 Thread 组件和一个 Storage Subsystem 组件。线程向存储子系统发送 Write request, Read request, Barrier request 消息。存储子系统向线程发送 Read response, Barrier ack 消息。

读请求/读响应对是紧密耦合的，而其他消息是单向的。这两部分之间没有缓冲。

Coherence-by-fiat (指令一致性) 我们的存储子系统完全从处理器实现的存储缓冲、缓存层次结构以及缓存协议中抽象出来：我们的模型没有显式的内存，无论是系统整体的，还是任何缓存或存储队列的（能够从所有这些中抽象出来本身就很有趣）。相反，我们以一个读可以从哪些写事件中读取的角度来工作。我们的存储子系统为每个地址维护着它所见过的写之间的一致性顺序的当前约束，作为一个严格偏序（传递但非自反）。例如，假设存储子系统已经看到了四个写操作，w₀, w₁, w₂ 和 w₃，都指向同一个地址。它可能已经建立了下面左图所示的一致性约束，其中 w₀ 已知在 w₁, w₂ 和 w₃ 之前，w₁ 已知在 w₂ 之前，但 w₁ 和 w₃ 之间，以及 w₂ 和 w₃ 之间的关系尚未确定。

图表内容描述: 左图是一个偏序图：w₀ 是顶部节点，有边指向 w₁ 和 w₃。w₁ 还有一条边指向 w₂。w₂ 和 w₃ 之间没有路径。 右图显示，在左图的基础上，增加了一条从 w₁ 到 w₃ 的边。

存储子系统还记录了它已传播 (propagated) 到每个线程的写列表：那些为响应读请求而发送的写，那些由线程自己完成的写，以及那些在传播屏障过程中传播到该线程的写。这些与已传播到该线程的屏障记录交错在一起。请注意，这是一个存储子系统模型的概念：传播到某个线程的写不一定已经在读响应中发送给了该线程模型。

现在，给定一个线程 tid 的读请求，响应中可以发送哪些写？从上面左边的状态来看，如果传播到线程 tid 的写只有 [w₁]，也许是因为 tid 已经从 w₁ 读过，那么：

  • 它不能被发送 w₀，因为 w₀ 在一致性上先于 w₁ 这个写，而 w₁（因为它在已传播写的列表中）可能已经被读取过；

  • 它可以重新从 w₁ 读取，保持一致性约束不变；

  • 它可以被发送 w₂，同样保持一致性约束不变，在这种情况下 w₂ 必须被追加到传播给 tid 的事件列表中；或者

  • 它可以被发送 w₃，同样追加到传播给 tid 的事件列表中，但这还意味着要提交 w₃ 在一致性上后于 w₁，如上面右图的一致性约束所示。注意，这仍然让 w₂ 和 w₃ 的相对顺序不受约束，所以另一个（线程）…

（接第五页）… 线程可以被发送 w₂ 然后 w₃ 或者（在另一次运行中）反过来（或者确实只有一个，或者一个都没有）。

在模型中，这种行为被分解为独立的存储子系统转换：有一条规则用于在两个迄今为止无关联的、对同一地址的写之间做出新的一致性承诺，一条规则用于将一个写传播到一个新的线程（这只有在足够的一致性承诺已经做出后才能触发），以及一条规则用于响应读请求向线程返回值。最后一条规则总是返回读线程已传播事件列表中对该读地址的最新写，因此该列表本质上充当了每个线程的内存（尽管它记录的信息不仅仅是字节数组）。我们采用这些分离的转换（我们称之为部分一致性承诺风格）以便于将模型转换与实际硬件实现事件联系起来：一致性承诺对应于写操作流经分层存储缓冲实现中的连接点。

Out-of-order and Speculative Execution (乱序与推测执行) 正如我们将在第 6 节中看到的，Power 行为的许多可观察到的微妙之处源于线程可以乱序和推测性地执行读指令，但如果一个冲突的写在指令提交之前到达，该指令会被重启，或者如果一个分支被证明是预测错误的，它会被中止。然而，写在它们的指令提交之前不会被发送到存储子系统，并且我们没有观察到可观察的值推测。因此，我们的线程模型允许非常自由的乱序执行，包括无界的推测性执行，越过尚未解决的分支和一些屏障，而我们的存储子系统模型则无需关心推测、重试或中止。另一方面，存储子系统维护当前的一致性约束，如上所述，而线程模型则无需访问它；线程模型通过以合理的顺序发出请求，并在必要时中止/重试来维护一致性。

对于每个线程，我们有一个已提交 (committed) 和执行中 (in-flight) 的指令实例树。新获取的指令成为执行中的，稍后，在满足适当的前提条件下，可以被提交。例如，下面我们展示了一组指令实例 {i₁, ..., i₁₃} 及其程序顺序后继关系。其中三个（{i₁, i₃, i₄}，用方框表示）已经提交；其余的正在执行中。

图表内容描述: 一个指令树/图。i₁（方框）是根。它指向 i₂，i₂ 指向 i₃（方框）和 i₅。i₃ 指向 i₄（方框）。i₅ 是一个分支，指向 i₆ 和 i₇。i₄ 指向 i₈。i₈ 是一个分支，指向 i₉ 和 i₁₀。i₁₀ 指向 i₁₁，i₁₁ 指向 i₁₂。i₄ 还指向 i₁₃。

指令实例 i₅ 和 i₈ 是分支，线程已经为它们获取了多个可能的后继；这里只有两个，但对于一个带有计算地址的分支，它可能会获取许多可能的后继。注意，已提交的实例不一定是连续的：这里 i₃ 和 i₄ 已经提交，尽管 i₂ 还没有，这只有在它们足够独立时才会发生。当一个分支被提交时，任何未被选择的替代路径都会被丢弃，并且跟随（按程序顺序）一个未提交分支的指令直到该分支提交后才能被提交，因此树在任何已提交（方框）指令之前必须是线性的。

在实现中，当缓存行失效被处理时，读操作会被重试。在模型中，为了从这究竟何时发生（以及从核心所做的任何必须重试的指令跟踪）中抽象出来，我们采用了一种延迟失效语义 (late invalidate semantics)，在提交一个读或写时重试适当的读（及其依赖）。例如，考虑程序顺序中的两个读 r₁ 和 r₂，它们已经从两个不同的、对同一地址的写中得到满足，r₂ 首先（乱序）从 w₁ 得到满足，r₁ 稍后从一致性上更晚的 w₂ 得到满足。当 r₁ 提交时，r₂ 必须被重启，否则将出现一致性违规。（这依赖于写操作永远不会被存储子系统以不一致的顺序提供的事实；线程模型不需要明确记录一致性顺序。）

Dependencies (依赖关系) 依赖关系完全由线程模型处理，涉及到每个指令实例读取和写入的寄存器（指令的寄存器足迹是静态已知的）。内存读在其地址确定之前无法被满足（尽管在重试时可能仍会改变），内存写在其地址和值完全确定之前无法被提交。我们不显式地建模寄存器重命名和影子寄存器，但我们的乱序执行模型包含了它们的效果，因为寄存器读从程序顺序前驱的寄存器写中取值。

Barriers (sync and lwsync) and cumulativity-by-fiat (指令屏障与累积性) 屏障的语义涉及模型的两个部分，如下所示。

当存储子系统收到一个屏障请求时，它将该屏障记录为已传播到其自己的线程，标记出已传播到该线程的写序列中的一个点。这些写是该屏障的 A 组写 (Group A writes)。当一个屏障的所有 A 组写（或它们的某个一致性后继）已经传播到另一个线程时，存储子系统也可以记录这一事实，将屏障传播到该线程（从而标记出已传播到该线程的写序列中的一个点）。一个写不能被传播到线程 tid，直到所有相关的屏障都传播到 tid，其中相关的屏障是那些在写本身之前传播到写线程的屏障。反过来（根据上述），这意味着那些屏障的 A 组写（或某些一致性后继）必须已经传播到 tid。这模拟了累积性的效果，同时从其实现细节中抽象出来。

此外，一个 sync 屏障可以在其所有的 A 组写已经传播到所有线程后，被确认（acknowledged）回发起线程。

在线程模型中，屏障约束了提交顺序。例如，在所有先前的 sync 屏障被提交和确认之前，任何内存加载或存储指令都不能被提交；并且 sync 和 lwsync 屏障在所有先前的内存读和写被提交之前不能被提交。此外，内存读在先前的 sync 屏障被提交和确认之前不能被满足。这里有各种可能的建模选择，应该不会产生任何可观察的差异——上述选择对应于一个适度激进的实现。

4. 模型详解

我们现在详细介绍存储子系统和线程模型之间的接口，以及它们各自的状态和转换。转换在 §4.3 和 §4.5 中以其前提条件、对相关状态的影响以及发送或接收的消息来描述。转换是原子的，并如图 1 所示进行同步；消息没有缓冲。这是我们在线可用的数学定义 [SSA+11] 的散文描述。

4.1 存储子系统/线程接口

存储子系统和线程交换消息：

  • 一个写请求 (write request) 或 write w 指定了写线程 tid、唯一的请求ID eid、地址 a 和值 v。

  • 一个读请求 (read request) 指定了发起线程 tid、请求ID eid 和地址 a。

  • 一个读响应 (read response) 指定了发起线程 tid、请求ID eid 和一个写 w（它本身指定了执行写的线程 tid'、其ID eid'、地址 a 和值 v）。这在读取的值被绑定时发送。

  • 一个屏障请求 (barrier request) 指定了发起线程 tid、请求ID eid 和屏障类型 b（sync 或 lwsync）。

  • 一个屏障确认 (barrier ack) 指定了发起线程 tid 和请求ID eid（一个屏障确认仅为 sync 屏障发送，在该屏障传播到所有线程之后）。

4.2 存储子系统状态

存储子系统状态 s 具有以下组件。

  • s.threads 是系统中存在的线程ID集合。

  • s.writes_seen 是存储子系统已经看到的所有写的集合。

  • s.coherence 是存储子系统已经看到的写之间的一致性顺序的当前约束。它是一个二元关系：如果存储子系统已提交写 w₁ 在写 w₂ 之前，则 s.coherence 包含对 (w₁, w₂)。这个关系随着时间的推移而增长，新的对被加入，因为存储子系统做出额外的承诺。对于每个地址，s.coherence 是对该地址的写请求的严格偏序。它不关联不同地址的写，也不关联任何尚未被存储子系统看到的写。

  • s.events_propagated_to 为每个线程提供一个列表，包含：

    1. 由该线程自己完成的所有写，

    2. 已传播到该线程的其他线程的所有写，以及

    3. 已传播到该线程的所有屏障。 我们称这些写为已传播到该线程的写。一个屏障的 A 组写是所有在屏障之前已传播到屏障线程的写。

  • s.unacknowledged_sync_requests 是存储子系统尚未确认的 sync 屏障请求的集合。

存储子系统的初始状态包含系统中存在的线程ID集合，每个内存地址恰好一个写，所有这些写都已传播到所有线程（这确保它们在一致性上先于任何其他对该地址的写），一个空的一致性顺序，以及没有未确认的 sync 请求。

4.3 存储子系统转换

接受写请求 (Accept write request) 一个线程 tid 的写请求总是可以被接受。动作：

  1. 将新的写加入到 s.writes_seen，以记录存储子系统看到了这个新写；

  2. 将新的写追加到 s.events_propagated_to(tid)，以记录这个新写已传播到它自己的线程；并且

  3. 更新 s.coherence 以注明新的写在一致性上后于所有（对同一地址的）先前已传播到此线程的写。

部分一致性承诺 (Partial coherence commitment) 存储子系统可以内部地为一个特定地址提交一个更受约束的一致性顺序，通过向 s.coherence 添加一条任意的边（在一对已经被看到但尚未通过一致性关联的、对该地址的写之间），连同由传递性所暗示的任何边，前提是最终的一致性顺序与所有对 (w₁, w₂)（对任何地址）的集合的并集没有环路，其中 w₁ 和 w₂ 在 w₂ 的线程的已传播事件列表中被一个屏障分隔。 动作：向 s.coherence 添加新的边。

将写传播到另一个线程 (Propagate write to another thread) 存储子系统可以将它已经看到的（由线程 tid 发出的）一个写 w 传播到另一个线程 tid'，如果：

  1. 该写尚未传播到 tid'；

  2. w 在一致性上后于任何已经传播到 tid' 的、对同一地址的写；并且

  3. 所有在 w 之前（在 s.events_propagated_to(tid) 中）传播到 tid 的屏障都已经传播到 tid'。 动作：将 w 追加到 s.events_propagated_to(tid')。

向线程发送读响应 (Send a read response to a thread) 存储子系统可以在任何时候接受一个线程 tid 的读请求，并用已经传播到 tid 的、对同一地址的最新写 w 进行回复。请求和响应被紧密耦合到一个原子转换中。动作：发送一个包含 w 的读响应消息。

接受屏障请求 (Accept barrier request) 一个线程 tid 的屏障请求总是可以被接受。动作：

  1. 将其追加到 s.events_propagated_to(tid)，以记录该屏障已传播到其自己的线程（并因此确定该屏障的 A 组写）；并且

  2. （对于 sync）将其加入到 s.unacknowledged_sync_requests。

将屏障传播到另一个线程 (Propagate barrier to another thread) 存储子系统可以将它已经看到的一个屏障传播到另一个线程，如果：

  1. 该屏障尚未传播到该线程；并且

  2. 对于每个 A 组写，该写（或某个一致性后继）已经传播到该线程。 动作：将该屏障追加到 s.events_propagated_to(tid)。

确认 sync 屏障 (Acknowledge sync barrier) 一个 sync 屏障 b 如果已经传播到所有线程，就可以被确认。动作：

  1. 向发起线程发送一个屏障确认消息；并且

  2. 从 s.unacknowledged_sync_requests 中移除 b。

图 1. 存储子系统和线程同步 (此处是一个表格，我将其转录如下)

存储子系统规则

消息

线程规则

接受写请求

写请求

提交执行中指令

部分一致性承诺

将写传播到另一个线程

向线程发送读响应

读请求/读响应

从存储子系统满足内存读

通过转发一个执行中写来满足内存读

接受屏障请求

屏障请求

提交执行中指令

将屏障传播到另一个线程

确认 sync 屏障

屏障确认

接受 sync 屏障确认

获取指令

从前一个寄存器写中读取寄存器

从初始寄存器状态中读取寄存器

内部计算步骤

4.4 线程状态

单个硬件线程的状态 t 由以下部分组成：

  • 其线程 ID。

  • 所有寄存器的初始值，t.initial_register_state。

  • 一个已提交指令实例的集合 t.committed_instructions。它们的所有操作都已执行，并且它们不会被重启或中止。

  • 一个执行中指令实例的集合 t.in_flight_instructions。这些指令已被获取，并且一些相关的指令语义微操作可能已经执行。然而，相关的写或屏障都尚未发送到存储子系统，并且任何执行中指令都可能被中止（连同其所有依赖项）。

  • 一个尚未被存储子系统确认的 sync 屏障集合 t.unacknowledged_syncs。

线程的初始状态没有已提交或执行中的指令，也没有未确认的 sync 屏障。

每个指令实例 i 包含一个唯一的 ID、一个表示其指令语义当前状态的表示、其输入和输出寄存器的名称、它已从中读取的写的集合、指令地址、程序顺序前一个指令实例的 ID，以及从前一个实例到达此实例所需的任何值约束。指令语义分步执行，进行内部计算、寄存器读写、内存读，最后是内存写或屏障。

4.5 线程转换

获取指令 (Fetch instruction) 一个指令 inst 可以在其程序顺序前驱 iprev 之后，从地址 a 被获取，如果

  1. a 是 iprev 的一个可能的下一个获取地址；并且

  2. inst 是程序在 a 处的指令。

可能的下一个获取地址允许对计算出的跳转和条件分支进行推测；它们的定义如下：

  1. 对于非分支/跳转指令，是后继指令地址；

  2. 对于跳转到常量地址的指令，是那个地址；

  3. 对于跳转到尚未完全确定的地址的指令（即，存在一个未提交的指令，其数据流路径通向该地址），是任何地址；并且

  4. 对于条件分支，是跳转的可能地址以及后继地址。

动作：构造一个初始化的指令实例并将其加入到执行中指令集合。这是线程的内部动作，不涉及存储子系统，因为我们假设一个固定的程序而不是用读来建模取指；我们不建模自修改代码。

提交执行中指令 (Commit in-flight instruction) 一个执行中指令可以被提交，如果：

  1. 其指令语义没有待处理的读（内存或寄存器）或内部计算（数据或地址算术）；

  2. 所有对此指令有数据流依赖的指令（即寄存器输出馈送到此指令的寄存器输入的指令）都已提交；

  3. 所有程序顺序前驱的分支都已提交；

  4. 如果涉及内存加载或存储，所有可能访问其地址的程序顺序前驱指令（即，具有尚未确定的地址或具有与该地址相等的已确定地址的指令）都已提交；

  5. 如果涉及内存加载或存储，或者此指令是 sync、lwsync 或 isync，那么 (a) 所有先前的 sync、lwsync 和 isync 指令都已提交，并且 (b) 此线程没有未确认的 sync 屏障；

  6. 如果是一个 sync 或 lwsync 指令，所有先前的内存访问指令都已提交；

  7. 如果是一个 isync，那么所有访问内存的程序顺序前驱指令的地址都已完全确定，这里的“完全确定”是指所有作为相关地址传入数据流依赖源的指令都已提交，并且任何内部地址计算都已完成。

动作：注意该指令现在已提交，并且：

  1. 如果是一个写指令，重启任何执行中的内存读（及其数据流依赖项），这些读已从同一地址但不同的写中读取（并且该读不能通过转发一个执行中写来满足）；

  2. 如果是一个读指令，找到所有执行中的程序顺序后继，这些后继已从同一地址的不同写中读取，或者它们跟随一个程序顺序在此指令之后的 lwsync 屏障，并重启它们及其数据流依赖项；

  3. 如果这是一个分支，中止任何未被选择的推测性执行路径，即，任何通过该分支无法到达的指令实例；并且

  4. 根据指令语义的要求，发送任何写请求或屏障请求。

接受 sync 屏障确认 (Accept sync barrier acknowledgement) 一个 sync 屏障确认总是可以被接受（总会有一个已提交的 sync，其屏障具有匹配的 eid）。动作：从 t.unacknowledged_syncs 中移除相应的屏障。

从存储子系统满足内存读 (Satisfy memory read from storage subsystem) 一个执行中指令的指令语义中的待处理读请求可以通过发出一个读请求并从存储子系统得到一个包含写的读响应来满足，如果：

  1. 要读取的地址已确定（即，任何具有到该地址的数据流路径的其他读都已满足，虽然不一定已提交，并且任何对此路径的算术运算已完成）；

  2. 所有程序顺序前驱的 sync 都已提交和确认；并且

  3. 所有程序顺序前驱的 isync 都已提交。 动作：

  4. 更新读指令的内部状态；并且

  5. 记录该写已被该指令读取。

其余的转换都是线程内部的步骤。

通过转发一个执行中写直接满足读指令 (Satisfy memory read by forwarding an in-flight write directly to reading instruction) 一个来自执行中（未提交）指令的待处理内存写 w 可以被直接转发到一个指令 i 的读，如果

  1. w 是一个到同一地址的未提交写，它在程序顺序上先于该读，并且没有程序顺序上 intervening 的内存写可能写到同一地址；

  2. i 的所有程序顺序前驱的 sync 都已提交和确认；并且

  3. i 的所有程序顺序前驱的 isync 都已提交。 动作：与从存储子系统满足内存读的规则中的动作相同。

从前一个寄存器写中读取寄存器 (Register read from previous register write) 一个寄存器读可以从一个程序顺序前驱的寄存器写中读取，如果后者是程序顺序上在它之前的对同一寄存器的最后一次写。动作：更新执行中读指令的内部状态。

从初始寄存器状态读取寄存器 (Register read from initial register state) 如果程序顺序上在它之前没有对同一寄存器的写，一个寄存器读可以从初始寄存器状态中读取。动作：更新执行中读指令的内部状态。

内部计算步骤 (Internal computation step) 一个执行中指令如果其语义有一个待处理的内部转换，例如对于一个算术操作，它可以执行一个内部计算步骤。动作：更新执行中指令的内部状态。

4.6 最终状态

最终状态是那些没有转换可以进行的状态。对于所有这样的状态，所有指令实例都应该是已提交的。

5. 解释简单示例

抽象机解释了我们之前看到的所有简单测试的允许和禁止行为。例如，概括地说：

MP 线程 0 对 x 和 y 的写请求可能有序也可能无序，但无论哪种方式，因为它们是到不同地址的，它们可以以任一顺序传播到线程 1。此外，即使它们按程序顺序传播，线程 1 对 x 的读也可以首先被满足（看到初始状态），然后是 y 的读，它们可以以任一顺序提交。

MP+sync+ctrl (控制依赖) 这里的 sync 保持了写到线程 1 的传播顺序，但线程 1 对 x 的读可以推测性地被满足，在控制依赖的条件分支被解决之前，以及在程序顺序前驱的线程 1 对 y 的读被满足之前；然后这两个读可以按程序顺序提交。

MP+sync+ctrlisync (isync) 在条件分支和线程 1 对 x 的读之间添加 isync，阻止了该读在 isync 提交之前被满足，而 isync 提交又必须在程序顺序前驱的分支提交之后，而分支提交又必须在第一个读被满足和提交之后。

WRC+sync+addr (A-累积性) 线程 0 的写请求 a:W[x]=1 必须被发出，并且该写必须传播到线程 1，以便 b 从中读取 1。线程 1 然后为其 sync 发出一个屏障请求，该请求在 a 之后传播到线程 1（所以写 a 在该屏障的 A 组集合中），然后发出写请求 c:W[y]=1。该写必须传播到线程 2 以便 d 从中读取，但在那之前 sync 必须传播到线程 2，而在这之前 a 必须传播到线程 2。同时，线程 2 上的依赖意味着读 e 的地址是未知的，因此 e 不能被满足，直到读 d 被满足（从 c）。由于这不能发生直到 a 传播到线程 2 之后，读 e 必须从 a 读取 1，而不是从初始状态读取 0。

WRC+data+sync 相比之下，虽然线程 0/线程 1 的 reads-from 关系和线程 1 的依赖确保了写请求 a:W[x]=1 和 c:W[y]=1 是按那个顺序发出的，并且线程 2 的 sync 保持了其读的顺序，但这些写传播到线程 2 的顺序是不受约束的。

ISA2 (B-累积性) 在 ISA2+sync+data+addr B-累积性示例中，线程 0 的写请求和屏障请求必须按程序顺序到达存储子系统，所以 sync 的 A 组是 {a}，并且在 b 写请求到达存储子系统之前，sync 已传播到线程 0。为了 c 从 b 读取，后者必须已传播到线程 1，这要求 sync 传播到线程 1，这反过来又要求 A 组写 a 已传播到线程 1。现在，线程 1 的依赖意味着 d 在读 c 被满足（并提交）之前不能被提交，因此 d 必须在 sync 传播到线程 1 之后。最后，为了 e 从 d 读取，后者必须已传播到线程 2，为此 sync 必须传播到线程 2，因此 A 组写 a 也传播到线程 2。线程 2 的依赖意味着 f 不能…

（接第九页）… 在 e 满足之前满足，所以它必须从 a 读取，而不是从初始状态。 对于此测试的 lwsync 变体，同样的结果和推理成立（注意推理不涉及 sync acks 或任何程序顺序在 sync 之后的内存读）。

IRIW+syncs 这里的两个 sync（在线程 1 和 3 上）有它们对应的写（a 和 d）在它们的 A 组中，因此这些写必须在相应的 sync 被确认之前传播到所有线程，而确认又必须在程序顺序后续的读 c 和 f 被满足之前发生。但为了这些读能读到 0，即从 a 和 d 的一致性前驱中读取，后者就不能已传播到所有线程（特别是，它们不能分别传播到线程 3 和 1）。换句话说，要发生这种情况，抽象机执行时间中必须存在一个环路：

a: W[x]=1 传播到最后一个线程 → 线程 1 sync 确认 → 线程 1 c: R[y]=0 满足 d: W[y]=1 传播到最后一个线程 → 线程 3 sync 确认 → 线程 3 f: R[x]=0 满足

如果用 lwsyncs 代替 syncs，这种行为是允许的，因为 lwsyncs 没有一个类似的确认机制，当它们的 A 组写已经传播到所有线程时，并且内存读不等待先前的 lwsyncs 到达那个点。

6. 不那么简单的例子

我们现在讨论一些更微妙的行为，并根据我们的模型逐一解释。

写转发 (Write forwarding) 在下面的 MP 的 PPOCA 变体中，f 在地址上依赖于 e，e 读取自写 d，而 d 控制依赖于 c。人们可能期望这个链条会阻止读 f 在 c 之前绑定它的值（通过从存储子系统满足内存读规则），但实际上在某些实现中，f 可以乱序绑定，如图所示——写 d 可以在它被提交到存储子系统之前，在线程内部直接转发给 e。通过转发一个执行中写来满足内存读规则模拟了这一点。用数据依赖替换控制依赖（测试 PPOAA，未显示）消除了这种可能性，据我们的实验结果显示，在当前硬件上禁止了给定的结果，在我们的模型中也是如此。当前的架构文本 [Pow09] 未指定 PPOAA 的结果，但我们预计未来的版本会明确禁止它。

图表内容描述: Test PPOCA: Allowed (测试 PPOCA：允许)

  • 线程 0:

    • a: W[z]=1

    • sync

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1，rf 边从 b 指向 c。

    • ctrl

    • d: W[x]=1

    • rf

    • e: R[x]=1，rf 边从 d 指向 e。

    • addr

    • f: R[z]=0，rf 边从初始状态 z 指向 f。

激进的乱序读 (Aggressively out-of-order reads) 在上面 MP 的 reads-from-same-writes (RSW) 变体中，x 的两个读 d 和 e 恰好从同一个写（初始状态）中读取。在这种情况下，尽管 d 和 e 从同一地址读取，e/f 对可以在 c/d 对之前乱序满足它们的读，从而允许了所示的结果。e 的地址是已知的，所以它可以很早被满足，而 d 的地址直到它对 c 的地址依赖被解决后才是已知的。相比之下，在一个 d 和 e 从 x 的不同写中读取的执行中（测试 RDW，未显示），这是被模型禁止的——第一个读（d）的提交会强制重启第二个读（e）及其依赖（包括 f），如果 e 最初从一个与 d 不同的写中读取。在实际实现中，重启可能更早，当一个失效被处理时，但会产生相同的可观察效果。

图表内容描述: Test RSW: Allowed (测试 RSW：允许)

  • 线程 0:

    • a: W[z]=1

    • sync

    • b: W[y]=2

  • 线程 1:

    • c: R[y]=2

    • addr

    • d: R[x]=0

    • po

    • e: R[x]=0

    • addr

    • f: R[z]=0

  • 所有读的 rf 边都来自初始状态。

一致性与 lwsync: blw-w-006 这个例子表明，我们不能假设 lwsync 和一致性边的传递闭包能保证写对的顺序，这对过于简化的模型是一个挑战。在我们的抽象机中，存储子系统提交 b 在一致性上先于 c 这一事实对写 a 和 d 传播到线程 2 的顺序没有影响。线程 1 没有从任何线程 0 的写中读取，所以它们不需要被发送到线程 1，因此没有累积性在起作用。

图表内容描述: Test blw-w-006: Allowed (测试 blw-w-006：允许)

  • 线程 0:

    • a: W[x]=1

    • lwsync

    • b: W[y]=1

  • 线程 1:

    • c: W[y]=2，co 边从 b 指向 c。

    • lwsync

    • d: W[z]=1

  • 线程 2:

    • e: R[z]=1，rf 边从 d 指向 e。

    • addr

    • f: R[x]=0，rf 边从初始状态指向 f。

在一些实现中，以及在模型中，用 syncs 替换两个 lwsyncs（bsync-w-006）会禁止这种行为。在模型中，这需要在抽象机执行时间中有一个环路，从 a 传播到其最后一个线程的点，到线程 0 sync 确认，到 b 写被接受，到 c 传播到线程 0，到 c 传播到其最后一个线程，到线程 1 sync 确认，到 d 写被接受，到 d 传播到线程 2，到 e 被满足，到 f 被满足，到 a 传播到线程 2，到 a 传播到其最后一个线程。当前的架构文本再次未指定这一点，但人们会期望在各处添加 sync（或者，在这种情况下，在两个读之间添加一个地址依赖）应该能恢复 SC。

一致性与 lwsync: 2+2W and R01 下面的 2+2W+lwsyncs 例子是一个一致性和 lwsyncs 的交互确实禁止了某些行为的案例。没有 lwsyncs (2+2W)，给定的执行是允许的。有了它们，写必须按程序顺序提交，但在一个部分一致性承诺（比如说 d 在 a 之前）做出后，另一个（b 在 c 之前）就不再被允许了。（由于这个测试只有写，注意到这里的一致性顺序边可以通过读取最终状态或用额外的线程两次读 x 和两次读 y 来观察，这可能会有所帮助。测试两个版本给出了相同的结果。）这个例子对于每个线程有一个视图顺序的公理化模型是一个挑战，因为需要一些东西来打破对称性。对于带有 syncs 的版本（2+2W+syncs），给定的行为也是禁止的。

图表内容描述: 左侧：Test 2+2W+lwsyncs: Forbidden (禁止)

  • 线程 0:

    • a: W[x]=1，co 边从 d 指向 a。

    • lwsync

    • b: W[y]=1

  • 线程 1:

    • c: W[y]=2，co 边从 b 指向 c。

    • lwsync

    • d: W[x]=2

右侧：Test R01: Allowed (允许)

  • 线程 0:

    • a: W[x]=1

    • lwsync

    • b: W[y]=2

  • 线程 1:

    • c: W[y]=1，co 边从 b 指向 c。

    • sync

    • d: R[x]=0，rf 边从初始状态指向 d。

上面右侧的 R01 测试是一个相关案例，我们在实践中没有观察到给定的允许行为，但它目前没有被架构禁止，我们的模型也允许它。在模型中，写都可以到达存储子系统，b/c 部分一致性承诺可以被做出，c 可以传播到线程 0，sync 可以被提交和确认，d 可以被满足，所有这些都在 a 和 lwsync 传播到线程 1 之前。

LB 和 (无) thin-air reads SB 示例的这个 LB 对偶是另一个我们在实践中没有观察到给定允许行为的案例，但它显然是架构上意图允许的，所以程序员应该假设未来的处理器可能会允许它，我们的模型也允许。添加数据或地址依赖（例如在 LB+datas 中）应该禁止给定的行为（数据依赖案例可能涉及凭空（out-of-thin-air）读），但这里的实验测试是空洞的，因为 LB 本身就未被观察到。

图表内容描述: Test LB: Allowed (测试 LB：允许)

  • 线程 0:

    • a: R[x]=1

    • po

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1

    • po

    • d: W[x]=1

  • rf 边从 d 指向 a，从 b 指向 c。

寄存器遮蔽 (Register shadowing) Adir 等人 [AAS03] 给出了 LB 的另一个变体（我们称之为 LB+rs，表示寄存器遮蔽），在线程 1 上有依赖，但在线程 0 上重用相同的寄存器，以证明影子寄存器的可观察性。这在我们的模型中也是允许的，但在我们的测试中不可观察——毫不奇怪，因为我们连 LB 本身都未观察到。然而，下面 MP 的变体确实表现出可观察的寄存器遮蔽：线程 1 上对 r3 的两次使用并没有阻止第二次读被乱序满足，如果读是进入影子寄存器。寄存器的重用在我们的图表中没有表示，所以对于这个例子，我们必须给出底层的 PowerPC 汇编代码。

图表内容描述: Test MP+sync+rs: Allowed (测试 MP+sync+rs：允许)

  • 线程 0:

    • a: W[x]=1

    • sync

    • b: W[y]=1

  • 线程 1:

    • c: R[y]=1

    • po

    • d: R[x]=0

  • rf 边从 b 指向 c，从初始状态指向 d。

# 线程 0
li r1,1
stw r1,0(r2)
sync
li r3,1
stw r3,0(r4)

# 线程 1
lwz r3,0(r2) # 对应 c: R[y]=1
mr r1,r3
lwz r3,0(r4) # 对应 d: R[x]=0

# 初始状态: 0:r2=x ^ 0:r4=y, 1:r2=y ^ 1:r4=x
# 允许: 1:r1=1 ^ 1:r3=0

7. 硬件实验

使用小型“石蕊测试 (litmus-test)”程序来讨论宽松内存模型的行为是公认的做法，但大多数先前的工作（除了少数著名例外）并没有凭经验调查测试在实际硬件上的行为。我们使用我们的 litmus 工具 [AMSS11] 在装有各种 Power 处理器的机器上运行测试：Power G5（又名 PowerPC 970MP，基于 POWER4 核心）、POWER 5、POWER 6 和 POWER 7。该工具接受 PowerPC 汇编的测试，并在一个旨在给处理器施加压力、以增加有趣结果可能性的测试 harness 中运行它们。这是黑盒测试，人们不能从某个观察的缺席中得出任何确定的结论，但我们的经验是，该工具相当有辨别力，识别了先前模型的许多问题（并且 [AMSS10] 报告了使用它发现了一个处理器勘误）。

我们的工作在所用测试的范围和数量上也是不寻常的。对于本文，我们建立了一个基于文献 [Pow09, BA08, AAS03, ARM08] 中测试的库、新的手写测试（例如 §6 中的 PPOCA, PPOAA, RSW, RDW, 和 2+2W，以及许多其他测试），以及几个测试（SB, MP, WRC, IRIW, ISA2, LB, 和另外两个 RWC 和 WWC）的所有可能屏障或依赖组合的系统性变体；我们称之为“VAR3”家族，共 314 个测试。我们在 Power G5、6 和 7 上运行了所有这些。此外，我们使用 diy 工具 [AMSS10] 系统地生成了数千个有趣的、带有增加大小的边循环（依赖、读自、一致性等）的测试，并测试了其中一些。作为一个重要的风格要点，我们使用带有最终值（并因此也对读取的值）约束的测试，而不是循环，以使它们易于测试。我们下面给出了我们实验结果的摘录，以提供一些风味；更多内容可在线获取 [SSA+11]。例如，PPOCA 在 POWER G5 (1.0k/3.1G) 上是可观察的，在 POWER 6 上不可观察，然后在 POWER 7 上再次可观察——这与 POWER 6 的不那么激进的乱序微架构是一致的。

(此处有一个实验结果表格，我将摘要其内容并转录)

测试

模型结果

POWER 6 结果

POWER 7 结果

WRC

Allow

ok 970k/12G

ok 23M/93G

WRC+data+addr

Allow

ok 562k/12G

ok 94k/93G

WRC+syncs

Forbid

ok 0/16G

ok 0/110G

WRC+sync+addr

Forbid

ok 0/16G

ok 0/110G

WRC+lwsync+addr

Forbid

ok 0/16G

ok 0/110G

WRC+data+sync

Allow

ok 150k/12G

ok 56k/94G

PPOCA

Allow

unseen 0/39G

ok 62k/141G

PPOAA

Forbid

ok 0/39G

ok 0/157G

LB

Allow

unseen 0/31G

unseen 0/176G

注：ok 表示模型与实验一致，unseen 表示模型允许但未观察到。数字对表示 观察次数/总迭代次数。

手动测试、系统测试和与 IBM 员工的讨论之间的相互作用对于我们模型的开发至关重要。例如：PPOCA/PPOAA 行为是在手动测试中发现的，导致我们推测它应该由写转发来解释，这后来通过讨论得到证实；blw-w-006 测试，在系统测试中发现，突出了早期模型中一致性和 lwsync 的困难；一致性和 sync 确认在当前实现中的作用是通过讨论产生的。

8. 执行模型

宽松内存模型的复杂性（以及我们考虑的测试数量）使得拥有工具支持来探索模型、自动计算模型允许的石蕊测试结果，并将它们与实践中观察到的结果进行比较也变得至关重要。为了简化模型开发，并保持对工具的信心，其核心应该从模型定义自动生成，而不是手工编码。我们的抽象机在 Lem 中定义，这是一种用于机器形式化的数学定义、类型、函数和归纳关系的新型轻量级语言 [OBZNS]。我们从中生成 HOL4 证明器代码（并因此生成机器的自动排版版本）和可执行的 OCaml 代码，使用一个有限集库，用于每个转换规则的前提条件和动作。我们还为我们测试所需的指令集的小片段形式化了一个符号化操作语义。使用这些，我们构建了一个详尽的记忆化搜索过程，找到石蕊测试的所有可能的抽象机执行。

这证实了模型对于我们在本文中提到的 41 个测试，对于 VAR3 家族的 314 个系统测试的其余部分，（接第十一页）以及对于各种其他测试，都具有预期的行为。在大多数情况下，模型与 Power7 的实验结果完全匹配，除了少数几个它包含实验结果但故意更松散的案例；这适用于我们 333 个测试批次中的 60 个。具体来说：模型允许指令乱序提交，这允许 LB 和 LB+rs 测试结果（实践中未观察到）；模型还允许一个 isync 即使在存在先前未提交的内存访问时也提交，而像带有 lwsync 和 isync 的 WRC 这样的测试的指定结果尚未被观察到；并且 R01 测试结果未被观察到。在所有这些情况下，模型遵循架构意图，这已与 IBM 员工确认。

我们的实验结果还证实，Power G5 和 6 严格强于 Power 7（尽管方式不同）：我们没有在那些处理器上看到任何在 Power 7 上也观察不到的测试结果。因此，就我们所知，该模型对于那些处理器也是可靠的。

9. 相关工作

关于宽松内存模型，已有大量先前的工作。我们关注那些不具有顺序一致性行为的主要当前处理器家族的模型：Sparc, x86, Itanium, ARM, 和 Power。Collier [Col92] 的早期工作基于对当时多处理器的经验测试开发了模型。对于 Sparc，供应商文档有一个清晰的 Total Store Ordering (TSO) 模型 [SFC91, Spa92]。它还引入了 PSO 和 RMO 模型，但这些在实践中未使用。对于 x86，供应商的意图直到最近都相当不清晰，处理器的实现行为也是如此。Sarkar, Owens 等人的工作 [SSZN+09, OSS09, SSO+10] 表明，对于正常的 用户或系统代码，它们也是 TSO。他们的工作精神与我们类似，有一个被经验观察测试的机械化语义。Itanium 提供了一个比 TSO 弱得多的模型，但一个由供应商比 x86 更精确定义的模型 [Int02]；它也已被形式化在 TLA [JLM+03] 和高阶逻辑 [YGLS03] 中。

对于 Power，已经有几个先前的模型，但没有一个能令人满意地用于推理实际的并发代码。部分原因在于架构随时间变化：lwsync 屏障已被添加，屏障现在是累积的。Corella, Stone 和 Barton [CSB93] 给出了一个早期的 PowerPC 公理化模型，但正如 Adir 等人指出的 [AAS03]，这个模型是有缺陷的（它允许我们在 §2 中展示的 MP+syncs 例子的非 SC 最终状态）。Stone 和 Fitzgerald 后来给出了 PowerPC 内存顺序的散文描述，很大程度上是根据当时的微架构 [SF95]。Gharachorloo [Gha95] 在一个通用框架中为不同架构给出了多种模型，但 PowerPC 的模型被描述为“近似的”；它显然是基于 Corella 等人 [CSB93] 和 May 等人 [MSSW94]。Adve 和 Gharachorloo [AG96] 明确指出 PowerPC 非常宽松，但没有讨论依赖诱导排序的复杂性，或更现代的屏障。Adir, Attiya, 和 Shurek 给出了一个详细的公理化模型 [AAS03]，用每个线程的视图顺序来表达。该模型是“通过一个反复求精的迭代过程、与 PowerPC 架构师的大量讨论，以及对示例和反例的分析而开发的”，并且它对一些石蕊测试（我们这里也使用了一些）的后果被详细描述。这些事实激发了一些信心，但要理解公理的威力并不容易，并且它描述的是非累积性屏障，遵循 pre-PPC 1.09 PowerPC 架构；当前的处理器似乎相当不同。最近，Chong 和 Ishtiaq 给出了一个 ARM 的初步模型 [CI08]，它有一个与 Power 非常相似的架构内存模型。在我们在这个领域的初始工作 [AFI+09] 中，我们基于对 Power ISA 2.05 和 ARM ARM 规范的解读，给出了一个公理化模型，并对一些测试进行了实验结果（描述为进行中的工作）；这对于某些方面似乎是正确的，但对于屏障给出了一个无法使用的弱语义。

最近，我们给出了一个相当不同的公理化模型 [AMSS10]，在 Alglave 的论文 [Alg10] 中作为一个通用框架的实例进一步发展；它在一个简单的全局时间设置中建模了 Power 的非多副本原子性（non-multi-copy-atomic）性质（例如 IRIW+addrs 被正确地允许）。该公理化模型相对于我们的实验测试是可靠的，并在此基础上可用于推理，但它比观察到的行为或某些重要示例的架构意图要弱。此外，它主要基于黑盒测试，其与实际处理器实现的关系不如我们这里提出的操作模型清晰，后者更牢固地建立在微架构和架构讨论之上。更详细地说，公理化模型对于 lwsync 和累积性可能比人们想要的要弱：它允许 MP+lwsync+addr 和 ISA2+sync+data+addr，这些没有被观察到并且旨在被架构禁止。它也禁止 R01，这个没有被观察到但架构上意图允许，并且在我们这里给出的模型中是允许的。因此，这两个模型是不可比较的。

我们还提到了 Lea 的《JSR-133 Cookbook for Compiler Writers》[Lea]，它为几个多处理器提供了非正式（且近似）的模型，并强调了清晰模型的必要性。

10. 结论

总结我们的贡献，我们通过示例和给出一个语义模型，描述了 Power 多处理器的实际行为。我们的示例包括说明了几个先前未描述的现象的新测试，以及经典测试的变体和一大套自动生成的测试；我们已经在多种处理器上凭经验调查了它们的行为。我们的模型是：严谨的（在机器类型检查的数学中）；经过实验验证的；易于理解的（以抽象机风格，并在这里用几页散文详细描述）；可用的（由示例的解释所证明）；有工具支持的，用于计算测试的可能结果；并且足以解释我们的示例和测试所暴露的微妙行为。它是一个新的抽象，通过指令维护一致性和累积性属性，但明确地建模乱序和推测性执行。

该模型应为 Power 多处理器的并发系统代码开发者（例如并发库、语言运行时、OS 内核和优化编译器的开发者）提供一个良好的直觉。此外，由于 ARM 架构内存模型非常相似，它很可能（经过微小调整）也适用于 ARM。

该模型还为验证理论和工具的未来研究开辟了许多方向。例如，现在可以陈述关于将 C++0x 并发原语正确编译到 Power 处理器的结果，并考虑在该上下文中进行屏障和依赖感知的优化。我们这里主要关注…

（接第十二页）… 实现的实际行为，但还需要工作来识别程序员实际依赖的保证，这可能会稍弱一些——据我们所知，我们的一些更奇特的例子不是自然的用例。还需要未来的工作来扩大模型的范围，这里只覆盖了可缓存内存而没有混合大小的访问。

我们主要根据其自身的术语和观察到的行为来描述我们的模型，没有深入探讨模型与底层微架构之间的关系，或与供应商架构规范 [Pow09] 的关系；这仍是未来的工作。后者内存模型文本的一个核心概念是，一个线程的内存读或写何时相对于另一个线程执行 (performed)，这有一个假设性（或虚拟）的定义，例如，对于加载：“处理器 P1 的一个加载相对于处理器 P2 执行，当要返回的值不能再被 P2 的一个存储改变时”，而那个 P2 的存储甚至可能在所考虑的程序中不存在（同样，ARM 也类似）。这个定义在最初的白盒设置 [DSB86] 中非常有意义，其中系统的内部结构是已知的，人们可以想象假设的 P2 存储出现在某个内部接口上，但在商业多处理器的黑盒设置中，要使其精确变得困难或不可能，尤其是在像 PPOCA 这样的例子中。我们的抽象机模型可能为改进架构定义提供一个踏脚石，也许通过新的公理化特征。

致谢 我们感谢 EP-SRC 拨款 EP/F036345, EP/H005633, 和 EP/H027351，ANR 项目 ParSec (ANR-06-SETIN-010)，以及 INRIA 关联团队 MM 的资助。

参考文献 (此部分为文献列表，按照要求不翻译具体条目)