ESOP'21-Verifying Visibility-Based Weak Consistency

$$$$

摘要

多线程程序通常依赖高效且线程安全的并发对象，如集合、键值映射和队列。虽然一些并发对象的操作被设计为原子性行为，见证其在线性化顺序中的前驱操作的原子效果，但其他操作为了避开复杂的控制和同步瓶颈而放弃了这种强一致性。例如，键值映射的 contains(value) 方法可能在不阻塞并发更新的情况下遍历键值条目，以避免不必要的性能瓶颈，因此可能会忽略某些在线性化顺序上的前驱操作的效果。尽管这些弱一致性的操作可能不具备原子性，但它们仍然提供了一些保证，比如只观察到已经存在的值。

在这项工作中，我们开发了一种方法来证明并发对象实现遵循弱一致性规范。特别是，我们考虑了对放宽可见性规范的（前向）模拟证明，允许指定的操作忽略它们的一些线性化顺序上的前驱操作，即表现得好像这些操作从未发生过一样。除了标注实现代码以识别逻辑效应发生的点（即操作的线性化点），我们还标注代码以识别可见操作，即那些效果被观察到的操作；实际上，这种标注可以通过跟踪每个访问内存位置的写入者自动完成。我们在一个通用的状态转换系统概念上形式化了我们的方法论，该概念独立于任何特定的编程语言或内存模型，并展示了其应用。

Introduction

编写高效的多线程程序通常涉及仔细组织共享内存访问，以促进线程间通信并避免同步瓶颈。现代软件平台如 Java 包含可重用的抽象（abstractions），这些抽象将低级别的共享内存访问和同步封装为熟悉的高级抽象数据类型（ADTs）。这些所谓的并发对象通常包括互斥原语如锁、原子整数等数值数据类型，以及 collections 如集合、键值映射和队列；Java 的标准版平台包含每种类型的许多实现。此类对象通常提供强一致性保证，如线性化能力 [18]，确保每个操作看起来像是原子地发生，根据某些线性化顺序观察到并发执行操作的原子效果。

虽然这些强一致性保证对于使用并发对象的程序进行逻辑推理非常理想，但这些保证对于许多操作来说过于严格，因为它们排除了简单和/或高效的实现——Java 的并发集合方法中超过一半的方法放弃了原子性以实现弱一致性 [13]。一方面，基本操作如键值映射的 get 和 put 方法通常允许相对简单的原子实现，因为它们的行为基本上取决于存储相关键值映射的单个内存单元。另一方面，使聚合操作如 size 和 contains(value) 原子化会引入同步瓶颈，或引入复杂的控制结构，因为它们的原子行为取决于同时存储在许多内存单元上的值。有趣的是，即使底层内存操作顺序一致，此类实现也不是线性化的，例如 Java 8 的并发集合，其内存访问是数据竞争自由的 [8]。

$$\begin{gathered} o_1:contains(v)\text{ \\ o2:insert(k1,v) \\ o3:remove(k2)} \end{gathered}$$

例如，Java 的并发哈希映射的 contains(value) 方法在不阻塞并发更新的情况下迭代键值条目，以避免不合理的性能瓶颈。因此，在给定的执行中，contains-value-v 操作 $o_1$ 将忽略操作 $o_2$ 的并发插入 $k_1\mapsto v$，因为它已经遍历了键 $k_1$。这种忽视使 $o_1$ 可能得出值 $v$ 不存在的结论，而只能通过 $o_1$ 在 $o_2$ 之前线性化来解释。在操作 $o_3$ 在 $o_1$ 到达键 $k_2$ 之前并发地移除 $k_2\mapsto v$ 的情况下，只有在 $o_2$ 完成后，原子性才被违反，因为在线性化的每种可能情况下，映射 $k_2\mapsto v$ 和 $k_1\mapsto v$ 二者之一总是存在。尽管如此，此类弱一致性操作仍然提供保证，例如，从未观察到的值永远不会被观察到，且初始存在的值不会被移除。

在本工作中，我们开发了一种方法论，用于证明并发对象实现遵守其弱一致性规范所规定的保证。我们方法的关键方面是通过可见性放松（visibility relaxation）[13] 提升现有的顺序 ADT 规范，以及利用基于放松可见性 ADTs 的简单且可机械化的基于前向模拟 [25] 的推理。实际上，我们的方法论扩展了基于线性化证明的前向模拟方法，适用于具有弱一致性操作的并发对象，并使弱一致性保证的证明自动化。

为了利用现有的顺序 ADT 规范，我们采用了最近的可见性放松方法 [13]。与线性化 [18] 类似，每个操作的返回值由其前驱的原子效果决定，这些前驱在某些（即，存在量化）线性化顺序中。为了允许一致性减弱，允许操作在一定程度上忽略其线性化顺序前驱，表现得好像它们没有发生。直观上，这种（也存在量化）可见性捕捉了跨多个内存单元存储的值的无法或不愿意原子观察。为了提供保证，可见性放松的范围在不同程度上受到限制。值得注意的是，绝对操作的可见性必须包括其所有线性化顺序的前驱，而单调操作的可见性必须包括所有发生在前驱之前的操作，以及对它们可见的所有操作。Java 的并发集合方法大多数是绝对或单调的 [13]。例如，在上述包含值示例中，通过考虑操作 $o_2$ 对 $o_1$ 不可见，可以得出 $v$ 不存在的结论。这可以通过线性化顺序 $o_2;o_3;o_1$ 来证明，其中 $o_1$ 看到了 $o_3$ 删除 $k_2\mapsto v$ 但没有看到 $o_2$ 插入 $k_1\mapsto v$。将单调可见性归因于包含值方法相当于保证除非被移除（即并发地），否则初始存在的值将被观察到。

虽然放松可见性规范提供了一种描述弱一致性并发对象操作提供的保证的手段，但系统地建立实现的遵从性需要一种策略来证明模拟 [25]，即实现的每一步都被（操作表示的）规范的某一步所模拟。我们贡献的核心因此是三重的：首先，识别与实现级别转换相关的相关规范级别动作；其次，识别实现级别注释，这些注释将转换与规范级别动作相关联；第三，开发系统地设计此类注释的策略。例如，基于线性化点的现有方法 [18] 实际上相当于注释实现级别转换，这些转换在其规范级别动作（即其原子效应）发生时发生。放松可见性规范不仅需要一个存在量化线性化顺序的见证，还需要一个存在量化可见性关系，因此需要第二种注释来解决操作的可见性。我们提出了一种可见性动作的概念，使操作能够声明其对其他操作的可见性，例如，指定它读取的内存单元的写入者。

我们方法的其余部分在于设计一种系统的方法来构建模拟证明，以实现自动验证。本质上，我们识别了一种系统地注释实现的策略，给定线性化点注释和可见性边界（即，绝对或单调），然后使用现成的验证工具对相应的模拟检查进行编码。对于后者，我们利用 civl [16]，这是一种用于 Owicki-Gries 风格模块化证明的并发程序语言和验证器，支持任意数量的线程。原则上，由于我们的方法将模拟简化为安全性验证，任何安全性验证器都可以使用，尽管 civl 通过在任意程序点捕获干扰来促进多线程程序的推理。使用 civl，我们验证了 Java 的并发哈希映射和并发链式队列的包含值方法和大小方法的单调性，以及 add 和 remove 操作的绝对一致性。尽管我们的模型是用 civl 编写的，并假设顺序一致的内存访问，但它们捕捉了 Java 中弱一致性的困难方面，包括基于堆的内存访问；此外，我们的模型在 Java 8 的内存模型下也是合理的，因为它们的 Java 8 实现保证了数据竞争自由。

总之，我们提出了第一个使用顺序规范和前向模拟来验证弱一致性操作的方法。贡献包括：

• 我们的方法论在一般意义上的转换系统上的形式化，不依赖于任何特定的编程语言或内存模型（$\mathcal{S}3$）；
• 将我们的方法论应用于验证一个弱一致性键值映射的包含值方法（$\mathcal{S}4$）；以及
• 使用自动化定理证明器验证弱一致性 Java 方法模型的机械化（$\mathcal{S}5$）。

除了上述大纲外，本文还通过可见性放松总结了现有的弱一致性规范方法论（$\mathcal{S}2$），总结了相关工作（$\mathcal{S}6$），并得出结论（$\mathcal{S}7$）。所有定理和引理的证明都列在附录 A 中。

Weak Consistency

我们验证弱一致性并发对象的方法论依赖于弱一致性规范的精确描述，以及用于建立规范遵从性的证明技术。在本节中，我们回顾并概述了一种称为可见性放松 [13] 的描述，它是顺序抽象数据类型 (ADT) 规范的扩展，在这种规范中，某些操作的返回值可能不反映先前执行的操作的效果。

在本文的其余部分，记号上，$\epsilon$ 表示空序列，$\mathrm{\varnothing }$ 表示空集，$\mathrm{\_}$ 表示未使用的绑定，$\mathrm{\top }$ 和 $\mathrm{\perp }$ 分别表示布尔值 true 和 false。我们用 $R(x)$ 表示关系 $R$ 中包含元组 $x$；用 $R[x\mapsto y]$ 表示关系 $R$ 的扩展 $R\cup \{xy\}$，其中包含 $xy$；用 $R\mid X$ 表示关系 $R$ 在集合 $X$ 上的投影 $R\cap X^{\ast }$；用 $\bar{R}$ 表示关系 $R$ 的补集 $\{x:x\notin R\}$；用 $R(x)$ 表示关系 $R$ 在 $x$ 上的像 $\{y:xy\in R\}$；用 $R^{-1}(y)$ 表示关系 $R$ 在 $y$ 上的前像 $\{x:xy\in R\}$；$R(x)$ 是指包含还是镜像（inclusion or an image）将根据上下文清楚。最后，我们用 $x_i$ 表示元组 $x=x_0{x}_1\dots$ 的第 $i$ 个元素。

Weak-Visibility Specications

对于 ADT 规范的一般概念，我们考虑固定的方法名称集合 $\mathbb{M}$ 和参数或返回值集合 $\mathbb{X}$。一个操作标签 $\lambda =⟨m,x,y⟩$ 是一个方法名称 $m\in \mathbb{M}$ 以及参数和返回值 $x,y\in \mathbb{X}$。只读谓词是一个操作标签上的单目关系 $R(\lambda )$，操作序列 $s={\lambda }_0{\lambda }_1\dots$ 是操作标签的序列，而顺序规范 $S=\{s_0,s_1,\dots \}$ 是操作序列的集合。我们说 $R$ 与 $S$ 兼容，当 $S$ 在删除只读操作后是封闭的，即，${\lambda }_0\dots {\lambda }_{j-1}{\lambda }_{j+1}\dots {\lambda }_i\in S$ 当 ${\lambda }_0\dots {\lambda }_i\in S$ 且 $R({\lambda }_j)$。

示例 1

键值映射 ADT 顺序规范 $S_m$ 是包含所有序列 ${\lambda }_0\dots {\lambda }_i$ 的前缀封闭集合，其中 ${\lambda }_i$ 是以下之一：

• $⟨\mathrm{put},kv,b⟩$，且 $b=\mathrm{\top }$ 当且仅当某个 $⟨\mathrm{rem},k,\mathrm{\_}⟩$ 跟随任何先前的 $⟨\mathrm{put},kv,\mathrm{\_}⟩$；
• $⟨\mathrm{rem},k,b⟩$，且 $b=\mathrm{\top }$ 当且仅当没有其他 $⟨\mathrm{rem},k,\mathrm{\_}⟩$ 跟随某个先前的 $⟨\mathrm{put},kv,\mathrm{\_}⟩$；
• $⟨\mathrm{get},k,v⟩$，且没有 $⟨\mathrm{put},k{v}^{\prime },\mathrm{\_}⟩$ 也没有 $⟨\mathrm{rem},k,\mathrm{\_}⟩$ 跟随某个先前的 $⟨\mathrm{put},kv,\mathrm{\_}⟩$，且 $v=\mathrm{\perp }$ 如果没有这样的 $⟨\mathrm{put},kv,\mathrm{\_}⟩$ 存在；或
• $⟨\mathrm{has},v,b⟩$，且 $b=\mathrm{\top }$ 当且仅当没有先前的 $⟨\mathrm{put},k{v}^{\prime },\mathrm{\_}⟩$ 也没有 $⟨\mathrm{rem},k,\mathrm{\_}⟩$ 跟随某个先前的 $⟨\mathrm{put},kv,\mathrm{\_}⟩$。

只读谓词 $R_m$ 在以下情况下成立：

• $R_m(⟨\mathrm{put},\mathrm{\_},b⟩)$ 如果 $\mathrm{\neg }b$
• $R_m(⟨\mathrm{rem},\mathrm{\_},b⟩)$ 如果 $\mathrm{\neg }b$
• $R_m(⟨\mathrm{get},\mathrm{\_},\mathrm{\_}⟩)$
• $R_m(⟨\mathrm{has},\mathrm{\_},\mathrm{\_}⟩)$

这是 Java 的 Map ADT 的简化版本，即，方法较少。

为了从顺序规范推导弱规范，我们考虑一个集合 $\mathbb{V}$ 中恰好包含两个可见性标签，这些标签来自先前的工作 [13]：绝对和单调。一个可见性注释 $V:\mathbb{M}\to \mathbb{V}$ 将每个方法 $m\in \mathbb{M}$ 映射到一个可见性 $V(m)\in \mathbb{V}$。

直观上，绝对可见性要求操作观察其所有线性化顺序前驱的效果。较弱的单调可见性要求操作观察其所有发生在前驱（即，程序和同步顺序）的效果，以及那些前驱已经观察到的效果，即，可见效果的集合在发生在前驱的操作链上单调递增；相反，操作可以忽略那些已经被其发生在前驱忽略的效果，只要那些效果不是通过程序和同步顺序传递相关的。

定义 1

一个弱可见性规范 $W=⟨S,R,V⟩$ 是一个顺序规范 $S$，带有兼容的只读谓词 $R$ 和可见性注释 $V$。

示例 2

弱一致性包含值映射 $W_m=⟨S_m,R_m,V_m⟩$ 为示例 1 中的键值映射 ADT 方法 $S_m$ 注释如下：

$ V_m(\put) = V_m(\rem) = V_m(\get) = \text{absolute}, \quad V_m(\mathrm{has}) = \text{monotonic}. $

Java 的并发哈希映射似乎与这一规范一致 [13]。

我们通过描述并发方法调用返回的值来赋予规范语义，给定调用顺序的约束。实际上，调用之间的发生顺序由程序顺序确定，即，同一线程中的调用，以及同步顺序，即，访问同一原子对象（例如，锁）的不同线程中的调用。一个历史 $h=⟨O,inv,ret,hb⟩$ 是一个数值操作标识符集合 $O\subseteq \mathbb{N}$，以及一个调用函数 $inv:O\to \mathbb{M}\times \mathbb{X}$ 将操作标识符映射到方法名称和参数值，一个部分返回函数 $ret:O\to \mathbb{X}$ 将操作标识符映射到返回值，以及一个（严格）部分发生顺序关系 $hb\subseteq O\times O$；空历史 $h_{\mathrm{\varnothing }}$ 有 $O=inv=ret=hb=\mathrm{\varnothing }$。一个操作 $o\in O$ 是完整的当 $ret(o)$ 被定义，否则是不完整的；然后 $h$ 是完整的当每个操作都是完整的。一个完整操作 $o$ 的标签 $o$ 有 $inv(o)=⟨m,x⟩$ 和 $ret(o)=y$ 是 $⟨m,x,y⟩$。

为了将给定历史中的操作返回值与顺序规范关联起来，我们考虑这些操作的某些排序。一个历史 $h=⟨O,\mathrm{\_},\mathrm{\_},hb⟩$ 的线性化是一个包含 $hb$ 的全序 $lin\supseteq hb$，以及一个可见性投影 $vis$ 将每个操作 $o\in O$ 映射到一个子集 $vis(o)\subseteq li{n}^{-1}(o)$ 的操作，这些操作在 $lin$ 中位于 $o$ 之前；注意 $⟨o_1,o_2⟩\in vis$ 意味着 $o_1$ 观察到 $o_2$。对于给定的只读谓词 $R$，我们说 $o$ 的可见性是单调的，当它包括每个发生在前驱的操作，以及对一个发生在前驱的操作可见的操作，该操作不是只读的，即 $vis(o)\supseteq (h{b}^{-1}(o)\cup vis(h{b}^{-1}(o)))\mid \bar{R}$。我们说 $o$ 的可见性是绝对的，当 $vis(o)=li{n}^{-1}(o)$，并且 $vis$ 本身是绝对的，当每个 $vis(o)$ 是绝对的。一个抽象执行 $e=⟨h,lin,vis⟩$ 是一个历史 $h$ 以及 $h$ 的线性化和可见性投影 $vis$。一个抽象执行是顺序的，当 $hb$ 是全序的，完整的，当 $h$ 是完整的，以及绝对的，当 $vis$ 是绝对的。

示例 3

一个抽象执行可以使用线性化定义如下：

$$⟨\mathrm{put},⟨1,1⟩,\mathrm{\top }⟩⟨\mathrm{get},1,1⟩⟨\mathrm{put},⟨0,1⟩,\mathrm{\top }⟩⟨\mathrm{put},⟨1,0⟩,\mathrm{\perp }⟩⟨\mathrm{has},1,\mathrm{\perp }⟩$$

以及一个发生顺序，与线性化顺序相比，保持 $⟨\mathrm{has},1,\mathrm{\perp }⟩$ 与 $⟨\mathrm{put},⟨0,1⟩,\mathrm{\top }⟩$ 和 $⟨\mathrm{put},⟨1,0⟩,\mathrm{\perp }⟩$ 无序，并且一个可见性投影，其中每个 $\mathrm{put}$ 和 $\mathrm{get}$ 的可见性包括所有线性化前驱，而 $⟨\mathrm{has},1,\mathrm{\perp }⟩$ 的可见性包括 $⟨\mathrm{put},⟨1,1⟩,\mathrm{\top }⟩$ 和 $⟨\mathrm{put},⟨1,0⟩,\mathrm{\perp }⟩$。回忆在 $⟨k,v⟩$ 参数中，键 $k$ 优先于值 $v$。

为了确定个别历史与弱可见性规范的一致性，我们考虑它们对应的抽象执行的一致性。设 $h=⟨O,inv,ret,hb⟩$ 是一个历史，$e=⟨h,lin,vis⟩$ 是一个完整的抽象执行。则 $e$ 与可见性注释 $V$ 和只读谓词 $R$ 一致，如果对于每个操作 $o\in \mathrm{dom}(lin)$ 与 $inv(o)=⟨m,\mathrm{\_}⟩$，$vis(o)$ 是绝对的或单调的，分别根据 $V(m)$ 和 $R$。标签 ${\lambda }_0{\lambda }_1\dots$ 的全序 $o_0\prec o_1\prec \dots$ 的完整操作序列是操作标签的序列，即，${\lambda }_i$ 是操作 $o_i$ 的标签。则 $e$ 与顺序规范 $S$ 一致，当标签 $⟨lin\mid (vis(o)\cup \{o\})⟩$ 包含在 $S$ 中，对于每个操作 $o\in \mathrm{dom}(lin)$。最后，我们说 $e$ 与弱可见性规范 $⟨S,R,V⟩$ 一致，当它与 $S$、$R$ 和 $V$ 一致。

示例 4

示例 3 中的执行与弱一致性包含值映射 $W_m$ 一致，该映射在示例 2 中定义。

注释 1

适用于现代软件平台（如 Java）的一致性模型基于发生顺序关系，这些关系抽象了实时执行顺序。由于发生顺序与实时不同，不是必然的区间顺序，因此组合操作的顺序可能不一致。

Establishing Consistency with Forward Simulation

Proof Methodology

Implementation and Evaluation

Related Work

Conclusion and Future Work