\[ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \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 对象提供更强的规格说明。
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 $ 中，第一个添加操作对大小不可见。
