\[ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\hbs{\mathsf{hbs}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \]
摘要
有效的软件规格说明能够支持模块化推理，允许客户端在不了解模块实现细节的情况下建立程序属性。虽然一些模块的操作表现得像原子操作一样，但其他模块为了提高性能而采用了较弱的一致性。由于当前的方法无法捕捉到具有不同非原子一致性水平的操作所提供的保证，因此规格说明变得无效，失去了为调用非原子操作的程序建立属性的能力。
在这项工作中，我们开发了一种方法来指定那些操作满足多个不同一致性级别的软件模块。特别是，我们开发了一个简单的注释语言，通过可见性放松来指定弱一致性操作，在这种注释中对操作之间的可见性施加了不同的约束。为了与现代软件平台集成，我们识别了一种新的称为“顺序发生前一致性”的一致性特性，它允许有效验证。实验上，我们通过推导和验证 Java 并发对象的放松可见性规格说明，展示了我们方法的有效性。此外，我们还通过实验证明了我们的注释语言是优化的，即使更细粒度的语言也不能为 Java 对象提供更强的规格说明。
作者：
- MICHAEL EMMI, SRI International, USA
- CONSTANTIN ENEA, IRIF, Univ. Paris Diderot & CNRS, France
INTRODUCTION·
许多软件平台通过提供优化的并发对象来实现高性能多线程代码，这些并发对象将无锁共享内存访问协议封装到高级抽象数据类型中。例如，jdk 提供了 16 种原子原始寄存器类型（例如，具有原子增量方法）和 14 种并发数据结构（例如，具有原子提供、查看和轮询方法）。这些并发对象由专家设计和实施，并经过大量 jdk 用户审查，可提供高性能和可靠性。鉴于依赖这些并发对象的软件数量可能非常庞大，因此保持精确的规范并确保实现遵守其规范非常重要。许多方法都应具有原子行为，这意味着并发执行的调用的结果与这些相同调用的某些串行执行的结果相匹配；尽管采用了大量优化来避免阻塞和利用并行性，但它们仍应具有原子行为，例如，优先使用专用机器指令（如原子比较和交换）而不是基于锁的同步。
尽管无锁实现可以显著提高性能，但对原子性的坚持通常会带来根本的同步瓶颈 [Gilbert and Lynch 2002]。因此，一些方法，如 JDK 并发数据结构中的迭代器方法，采用了比原子性更弱的一致性标准。虽然从原子性放松到“弱一致性”为性能优化提供了灵活性，但它阻碍了模块化推理。与通过线性化 [Herlihy and Wing 1990] 给出精确形式意义的原子性保证不同，“弱一致性”操作提供的保证是模糊的，因为一致性可以在许多方面被削弱。
例如，在两个并行线程中调用集合的弱一致性大小方法 { add(1); remove(2) } 和 { add(2); size() ⇒ $ n $ } 可能在某些执行中返回 $ n = 0 $，其中调用交错执行。1 这个结果是原子操作所不允许的，因为在每次线性化中 $ n > 0 $：如果大小在第一个线程的操作之间执行，则 $ n = 2 $；否则 $ n = 1 $。我们对“弱一致性”的直观理解可能允许在上述示例中 $ n = 0 $，通过考虑大小与第一个线程的操作交错执行，但仅观察到移除的效果。然而，我们的直观理解可能不会允许 $ n = 100 $ 或 $ n = -1 $。然而，如果不识别“弱一致性”的精确语义，我们将放弃所有保证，使客户端推理变得不可能。
在这项工作中，我们研究了一种方法，用于精确指定具有弱一致性操作的并发对象。我们的起点是现有的方法论，用于考虑操作可见性的并发对象的公理一致性规范 [Burckhardt et al. 2014; Perrin et al. 2016]。这种方法本质上扩展了基于线性化的规范方法论，引入了操作之间的动态可见性关系，除了标准的动态实时顺序和线性化关系。允许较弱的可见性关系模型的结果是，一个操作可能不会观察到线性化在其之前的操作的效果。例如，在上述示例的完整线性化 add(1); add(2); remove(2); size() ⇒ $ n $ 中 $ n = 1 $，放松大小的可见性允许 $ n = 0 $ 的结果，在部分可见的线性化 add(2); remove(2); size() ⇒ $ n $ 中，第一个添加操作对大小不可见。
MOTIVATION
VISIBILITY RELAXATION
为了指定典型软件 API 的非原子操作，我们提出了一种简单的注释语言，它捕捉了第 2 节中描述的有限观察现象。这种注释语言的语义基于一种抽象的执行概念，它捕捉了程序调用中观察到的返回值和排序约束。除了考虑调用的各种线性化，我们的语义还考虑了在给定线性化中，任何给定调用可能或不可能被后来发生的调用观察到。然后，规范通过在这个观察关系上施加约束来决定给定抽象数据类型（ADT）允许的抽象执行。我们的注释语言补充了抽象数据类型给出的 API 的功能规范，以确定其实现的观察行为是否应该被接受。
不失一般性——见备注 1——我们考虑了一种简单的程序概念，具有简单的控制和数据流。形式上，一个 m-调用 \(i\) 是一个方法名 \(m\)，以及一个参数值向量 \(\vec{v}\)，和一个能够区分具有相同参数值的相同方法调用的标识符；一个 M-调用是某个方法 \(m \in M\) 的 m-调用。一个操作是调用与返回值的配对。抽象数据类型 A 在方法 M 上是一个从 M-调用序列 \(i_{0} i_{1} \ldots i_{n}\) 到返回值序列 \(A(i_{0} i_{1} \ldots i_{n}) = v_{0} v_{1} \ldots v_{n}\) 的映射。程序 \(p = \langle \po, \hbs \rangle\) 在抽象数据类型 A（在方法 M 上）是一个部分程序顺序 po 在 M-调用上，给定为代表线程的全序的并集，以及在 po 的调用上的一组 happens-before（先行发生）的部分顺序 hbs，每个都包括 po。除了程序顺序，这些先行发生的顺序通常代表平台定义的同步约束，这些约束被强加于 API 调用之外，包括监视器动作的释放-获取排序，以及顺序一致性对象的写-读动作的排序。我们不是直接模拟同步动作，而是通过给定程序中调用之间可能的先行发生顺序来捕捉它们的影响。
在整个工作中，我们使用熟悉的符号编写程序顺序，作为调用序列的并行组合 \(\set{\dots} \| \set{\dots}\)，例如，\(\set{i_1; i_2; i_3}\)，如图 2-4 所示。相应的程序顺序 po 关联序列内的调用，例如，\(\langle i_{1}, i_{2} \rangle \in\) po，但不关联不同序列的调用。我们的程序概念假设可能的先行发生顺序可以被静态地确定和列举。虽然这对于具有任意控制和数据流的程序通常是不可能的，但我们简单的程序概念使得这种静态确定对于常见的同步原语（如锁和易变变量）成为可能——见备注 1。
我们的注释语言语义依赖于序列和顺序的一些基本概念。我们用 \(\sigma(\alpha)\) 表示序列 \(\sigma\) 上以元素 \(\alpha\) 结尾的前缀，用 \(\pi(\alpha)=\set{\langle\alpha_{1},\alpha_{2}\rangle\in\pi: \langle\alpha_{2},\alpha\rangle\in\pi \lor \alpha_{2}=\alpha}\) 表示偏序 \(\pi\) 上以 \(\alpha\) 结尾的前缀。（笔者注：我觉得此处定义是笔误，应该是 \(\pi_\alpha = \set{\langle \alpha_1, \alpha_2 \rangle \in \pi \mid \langle \alpha_2, \alpha \rangle \in \textcolor{red}{\pi_\alpha} \lor \alpha_2 = \alpha }\)）当 \(\sigma_{1}\) 通过从 \(\sigma_{2}\) 删除元素得到时，我们称序列 \(\sigma_{1}\) 是另一个序列 \(\sigma_{2}\) 的子序列，记作 \(\sigma_{1} \preceq \sigma_{2}\)。我们将子序列的概念扩展到偏序，并说一个顺序 \(\pi_{1}\) 是另一个顺序 \(\pi_{2}\) 的子序，如果 \(\pi_{1} \subseteq \pi_{2}\)。为了统一，当 \(\pi_{1}\) 是 \(\pi_{2}\) 的子序时，我们写 \(\pi_{1} \preceq \pi_{2}\)。此外，为了简单起见，我们不区分序列和全序，在全序的上下文中重用前缀和子序列等概念。最后，当 \(i\) 是序列 \(\sigma\) 的元素时，我们写 \(i \in \sigma\)，当 \(i\) 是偏序 \(\pi\) 的元素时，我们写 \(i \in \pi\)，即存在 \(j\) 使得 \(\langle i, j\rangle\) 或 \(\langle j, i\rangle\) 被包含在 \(\pi\) 中。
扩展通常的概念以包括调用的观察，行为 \(b=\langle hb, ret\rangle\) 的一个线性化 \(\ell=\langle lin, vis\rangle\) 是：
- 一个全序 \(lin\)，它包括 \(hb\)，
- 一个函数 \(vis\)，将每个调用 \(i\) 映射到 \(lin(i)\) 的一个子序列，包括 \(i\)。
当 \(i_{1} \in \operatorname{vis}(i_{2})\) 时，我们说调用 \(i_{1}\) 对 \(i_{2}\) 是可见的，并且 \(i_{2}\) 可以看到 \(i_{1}\)。当对于 \(\ell\) 的每个调用 \(i\)，对 \(i\) 可见的调用的结果是 \(\operatorname{ret}^{\prime}=A(\operatorname{vis}(i))\)，并且与 \(i\) 的返回值上的 ret 一致时，即 ret(i) = ret'(i) —— ret 和 ret' 对于对 \(i\) 可见的其他调用的返回值可能不一致。当 \(b\) 的某个线性化被 A 接受时，行为 b 被 A 接受，当某个具有结果 ret 的行为被 A 接受时，结果 ret 被 A 接受。
