2110在因果一致的共享内存下的可判定验证0OriLahav以色列特拉维夫大学orilahav@tau.ac.il0Udi BokerHerzliya以色列跨学科中心（IDC）udiboker@idc.ac.il0摘要因果一致性是比顺序一致性更弱的最基本和广泛使用的一致性模型之一。本文研究了在因果一致的共享内存模型下运行的有限状态并发程序的安全属性验证。我们证明了这个问题在标准的因果一致性模型（也称为“因果收敛”和“强释放/获取”）下是可判定的。我们的证明通过开发一种基于“线程潜力”概念的替代操作语义，该语义等价于现有的声明性语义，并构成了一个良好结构化的转换系统。特别地，我们的结果允许验证Release/Acquire片段的C/C++11（RA）中的大量程序。实际上，虽然最近已经证明了通用程序下RA的验证是不可判定的，但由于RA与我们在这里研究的模型在写/写竞争自由程序方面是一致的，所以对于这个广泛使用的程序类别，在RA下的验证的可判定性可以从我们的结果中得出。这种新颖的操作语义在研究弱一致性共享内存模型及其验证方面也可能具有独立的用途。0CCS概念：∙软件及其工程→软件验证；并发编程语言；∙计算理论→并发性；逻辑和验证；程序验证；∙信息系统→分布式数据库事务。0关键词：弱内存模型、因果一致性、释放/获取、共享内存、并发、验证、可判定性、良好结构化的转换系统0未经ACM许可，可以制作本作品的全部或部分数字或印刷副本，供个人或课堂使用，但不得为了牟利或商业优势而制作或分发副本，并且副本必须带有本声明和第一页的完整引用。必须尊重ACM以外其他人拥有的本作品组成部分的版权。允许进行带有署名的摘要。要进行其他复制、再版、发布到服务器或重新分发到列表，需要事先获得特定的许可和/或支付费用。请向permissions@acm.org申请权限。PLDI '20，2020年6月15日至20日，英国伦敦，©2020年计算机协会。ACM ISBN978-1-4503-7613-6/20/06。https://doi.org/10.1145/3385412.33859660ACM参考格式：Ori Lahav和UdiBoker。2020年。在因果一致的共享内存下的可判定验证。在第41届ACM SIGPLAN国际编程语言设计与实现会议（PLDI'20）论文集中，2020年6月15日至20日，英国伦敦。ACM，美国纽约，16页。https://doi.org/10.1145/3385412.338596601 引言假设有人想要验证给定的顺序程序是否满足某个安全规范（例如，它永远不会崩溃）。如果数据域是有界的，我们可以将程序表示为有限状态转换系统，这个验证问题是可以轻松判定的。对于并发程序，假设（非现实的）顺序一致的共享内存语义并不会改变太多——内存构成了另一个有限状态系统，并且它与表示不同线程的系统的交错同步也可以很容易地表示为有限状态系统。另一方面，如果内存不能确保顺序一致性，而是提供较弱的一致性保证，那么安全验证问题的可判定性就完全不清楚了。在本文中，我们关注的是在因果一致的共享内存下的安全验证问题。因果一致性是比顺序一致性更弱的最基本的一致性模型之一。它在分布式数据库中特别常见且广泛研究（参见，例如，[37]和mongoDB文档[40]）。粗略地说，通过允许节点对某些内存操作的相对顺序存在分歧，并且只要求对“因果相关”操作的顺序达成全局共识，因果一致性允许可扩展、容错和可用的实现。如今，因果一致性模型在多线程编程中也变得非常重要。特别地，Release/Acquire模型（RA）是一种因果一致性形式，它指定了C/C++11中使用memory_order_release和memory_order_acquire进行同步访问的语义[14,23, 24]。一种更强的因果一致性形式，称为SRA（StrongRelease/Acquire），它等价于标准的因果一致性模型2120PLDI '20，2020年6月15日至20日，英国伦敦，Ori Lahav和Udi Boker0在分布式数据库[18]中，1描述了“多副本原子”多处理器体系结构（如POWER）提供的保证。具体而言，正如[30]所示，SRA精确地捕捉了从C/C++的发布/获取片段编译的程序在POWER体系结构中提供的保证。尽管它很重要，但直到最近，关于因果一致性下的安全验证问题还不太清楚。首先，挑战在于因果一致性模型的标准语义是声明性的（将程序行为与遵守某些形式一致性约束的部分有序执行历史进行了等同），而验证通常应用于操作模型。此外，因果一致性的操作版本本质上是无限状态的，因为线程通常可以从无限过去读取。实际上，Atig等人的研究[11]从有损FIFO通道机器到x86-TSO语义的可达性的降低可以直接适应因果一致性模型（具体而言，RA和SRA）。这意味着在因果一致性下的安全验证问题上存在非原始递归下界。最近，Abdulla等人证明了在一种因果一致性实例下，即RA模型下，安全验证问题是不可判定的[3]。本文的主要贡献是在SRA模型下建立安全验证的可判定性。如果特别关注RA下的验证，我们的结果提供了一个（相当紧密的）欠估（SRA下的错误意味着RA下的错误），并且由于RA和SRA在无竞争写入的程序上是一致的，我们获得了对于这个大型和广泛使用的程序类的RA下安全验证的可判定性。为了获得可判定性，我们使用了良构过渡系统的框架[2, 7,22]。直观地说，这个框架允许建立无限状态的“有损”系统的可判定性，其中（i）状态可以非确定性地忘记它们包含的一些信息；（ii）确定一个状态是否通过丢失信息从另一个状态获得构成了一个良好的拟序。然而，这种方法不能直接应用于（SRA的操作化版本），其自然状态是执行历史。首先，从历史中遗忘信息通常会导致更弱的因果约束，允许无法在不丢失信息的情况下获得的结果。其次，执行历史仅部分有序，并且（一般）部分序之间的嵌入不是良好的拟序。我们的解决方案是开发一种与SRA等效的新颖操作语义，对于这种语义，我们可以使用良构过渡系统的框架。关键思想在于01这种等价性不包括读-修改-写的原子性，在多线程编程中这是至关重要的，但在[18]中定义的因果一致性中并不提供（参见第3.1节）。0这种语义是为了保持机器状态中每个线程未来读取的潜力。这种语义可以直接地变得“有损”，因为失去一些潜力的部分从不允许额外的行为。此外，可以使用总序来表示潜力，其嵌入关系（基于普通子序列关系）是一个良好的拟序。在这种语义中，读取转换非常简单，它们只消耗潜力的前缀。复杂性留给了需要以适当方式增加不同线程的潜力以确保因果一致性的写入转换。我们的基本观察是，当另一个线程写入内存时，某个线程的潜力增加的方式可以仅根据两个线程的现有潜力来定义。这种直觉在我们的形式化（并在Coq中机械化）的对应证明中得到了明确的阐述，这些证明在新的有损语义和SRA的直观“操作化”语义之间建立了模拟（前向一方向和后向一方向）的关系。0相关工作。最近在[29]中概述了因果一致的共享内存模型、它们的验证问题和解决这些问题的方法，我们解决的问题仍然没有解决。正如上面提到的，Abdulla等人在[3]中证明了RA下的安全验证是不可判定的。在[30]中开发了SRA的操作性消息传递语义。它对我们的目的来说是不足的，因为它不能在不影响其允许的结果的情况下变得有损失。安全验证问题以前在TSO（x86多处理器的总存储顺序模型）下进行了研究，它比这里研究的任何模型都要强大。Atig等人通过将其归约到（从）有损信道系统中的可达性来证明了这个问题的可判定性（和非原始递归下界）。由于因果一致性模型不是多副本原子的，并且它们缺乏从位置到值的全局映射的任何概念，所以不能将其归约到SRA。值得注意的是，SRA不能完全通过程序转换（指令重排序和合并）[33]来解释，而除了最近的[3]中的不可判定性外，所有现有的结果（特别是[12]中的结果）都是针对完全由这些转换考虑的模型的。最近，Abdulla等人通过开发和利用TSO的“加载缓冲”语义大大简化了以前对TSO的证明（并在某些基准测试中展示了更好的实际运行时间）。加载缓冲区与我们的潜在列表大致相似，但是加载缓冲区是FIFO队列，而我们的列表必须允许将未来的读取插入到不同的位置，同时满足某些（新颖的）条件，以确保不违反因果一致性。此外，TSO的“加载缓冲”语义包括全局机器内存，而我们的语义不使用任何这样的概念。在因果一致性下的程序验证（特别是在RA下）近年来受到了相当多的关注。不同的方法包括（非自动化的）程序逻辑[21, 25, 32, 48, 49]，基于部分顺序缩减的（有界）模型检查[3,5, 27, 35]和鲁棒性验证[17, 31,41]。后一种方法将验证问题归约到顺序一致性下的验证和程序对因果一致性的鲁棒性的验证。因此，这种方法对于满足其安全规范但仍然表现出非顺序一致行为的程序是无效的。最后，[16]中研究了一个给定实现是否提供因果一致性保证的问题。然而，它与我们在这里研究的假设因果一致性的客户程序的验证是独立的。ğ2 we provide preliminary definitions. In ğ3 we present theSRA model and its safety verification problem, and provethat RA and SRA coincide for write/write-race-free programs.In ğ4 we present a straightforward operational version ofSRA’s declarative semantics. In ğ5 we introduce our noveloperational semantics of SRA. In ğ6 we show how this se-mantics is used to decide the safety verification problem.We conclude in ğ7. The appendices to this paper, publiclyavailable in [1], provide full proofs. Mechanized Coq proofsof the equivalence of the two semantics of SRA are availablein the artifact accompanying this paper.2Preliminariesand 𝑟 := CAS(𝑥,𝑒R,𝑒W) atomically loads the value of 𝑥 to 𝑟,compares it to the value of 𝑒R, and if the two values are equal,replaces the value of 𝑥 by the value of 𝑒W.A sequential program 𝑆 is a function from a set of the form{0, 1, ... ,𝑁 } (the possible values of the program counter) toinstructions. We denote by SProg the set of all sequentialprograms. A (concurrent) program 𝑃 is a top-level parallelcomposition of sequential programs, defined as a mappingfrom a finite set Tid ⊆ {T1, T2, ...} of thread identifiers toSProg. In our examples, we often write sequential programsas sequences of instructions delimited by line breaks, use ‘∥’for parallel composition, and refer to the program threadsas T1, T2, ... following their left-to-right order in the programlisting (see, e.g., Ex. 3.5 on Page 6).2130可判定的验证在一个因果一致的共享内存PLDI '20，2020年6月15日至20日，英国伦敦0在第2节中，我们提供了初步定义。在第3节中，我们介绍了SRA模型及其安全验证问题，并证明了RA和SRA在无写/写竞争程序中是一致的。在第4节中，我们提出了SRA的声明性语义的直观操作版本。在第5节中，我们介绍了我们的新颖SRA的操作语义。在第6节中，我们展示了如何使用这个语义来决定安全验证问题。我们在第7节中总结。本文的附录在[1]中公开提供，提供了完整的证明。在本文的附带工件中，提供了SRA两种语义等价性的机械化Coq证明。0大纲。本文的其余部分组织如下。在0SRA是一种声明性内存模型，通过对执行图施加一定的一致性约束来定义。后者描述了程序运行的（部分有序的）历史。在本节中，我们为声明性内存模型提供了初步定义：我们介绍了一个玩具编程语言（第2.1节），将其程序解释为转换系统（第2.2节），并将这些系统与执行图（第2.3节）相关联。02.1 编程语言 令 Val � N，Loc � { x , y , ... }，Reg � { a , b , ... }为有限值集合（共享）内存位置和寄存器名。图1展示了我们的玩具语言。它的表达式由寄存器（局部变量）和值构成。指令包括赋值和条件分支，以及内存操作。直观地说，赋值 � : = � 将 � 的值赋给寄存器 �（不涉及内存访问）；如果 � goto �，则当 的值不为0时，将程序计数器设置为 �；一个 łwritež � : = � 将 � 的值存储在 � 中；一个łreadž � : = � 将 � 的值加载到寄存器 �；� : = FADD ( �,� ) 原子地将 � 的值增加 � 并的旧值加载到 �；� : = XCHG ( �,� ) 原子地将 � 与 � 的值交换，并将 � 的旧值加载到�；and � : = CAS ( �,� R ,� W ) 原子地将 � 的值加载到 �，将其与 � R的值进行比较，如果两个值相等，则将 � 的值替换为 � W 的值。顺序程序 � 是从形如 {0 , 1 , ... ,� } 的集合（程序计数器的可能值）到指令的函数。我们用 SProg表示所有顺序程序的集合。一个（并发）程序 �是顺序程序的顶层并行组合，定义为从有限集 Tid � { T 1 , T 2 , ... } 的线程标识符到SProg的映射。在我们的示例中，我们经常将顺序程序写成由换行符分隔的指令序列，使用‘ ∥’表示并行组合，并按照程序列表中从左到右的顺序引用程序线程（参见，例如，第6页上的示例3.5）。02.2 从程序到标记迁移系统顺序和并发程序引出了标记迁移系统。0标记迁移系统。标记迁移系统（LTS）�是一个关于字母表Σ的三元组 � �,� 0 ,� �，其中 �是一组状态，� 0 � �是初始状态集合，� � � × Σ× �是一组转换。我们用 �. Q，�. Q 0 和 �. T 表示LTS�的组成部分；用 � −→ � 表示关系 {� �,� ′ � | � �, �,� ′ � ∈ �. T }，用 −→ �表示关系 � � ∈ Σ � −→ � 。状态 � ∈ �. Q 在 �中是可达的，如果存在 � 0 ∈ �. Q 0 使得 � 0 −→ � � �。序列 � 1 ,... ,� � 是 � 的轨迹，如果存在 � 0 ∈ �. Q 0 和 � ∈ �. Q 使得 � 0 � 1−→ � ∙∙∙ � � −−→ � �。对于给定符号 � ∈ Σ，集合 � � �. Q的前驱集合（关于符号 �）用 pred � � ( � ) 表示，由 { � ∈ �. Q | � � ′∈ �. � � −→ � � ′ } 给出。我们定义 pred � ( � ) � � � ∈ Σ pred � � ( � ) 。0对于顺序程序，字母表是标签的集合（扩展了 �以表示静默转换），如下所定义。0定义2.1. 标签要么是 R ( �, � R )（读标签），要么是 W ( �, � W)（写标签），或者是 RMW ( �, � R , � W)（读-修改-写标签），其中 � ∈ Loc，� R ，� W ∈Val。我们用 Lab 表示所有标签的集合。函数 typ、loc、valR 和 val W 返回（如果适用）给定标签 � 的类型（R / W /RMW）、位置、读取值和写入值。0一个顺序程序 � ∈ SProg 会在Lab ∪ { �}上引出一个LTS。它的状态是一对 � = � pc ,� �，其中 �� ∈N（称为程序计数器）和 � : Reg →Val（称为本地存储器，并按照明显的方式扩展到表达式）。它唯一的初始状态是 � 0 , �� ∈ Reg . 0�，其转换如图2所示，遵循上述非正式描述。（特别地，�中的读指令会引发 | Val |个具有不同读标签的转换。）我们将顺序程序与其引出的LTS等同起来（例如，当写作 �. Q 和 −→ �时）。反过来，一个并发程序 � 被认为是在 Tid × ( Lab ∪ { �}) 上的LTS。它的状态是函数，通常用 � 表示，为每个 � ∈ Tid分配一个状态 � ( � ) . Q；它的初始状态集是 { � | � �. � ( � ) ∈ � ( � ) .Q 0 }；它的转换是𝑣 ∈ Val ⊆ Nvalues𝑥,𝑦,𝑧 ∈ Loc ⊆ {x, y, ...}locations𝑟 ∈ Reg ⊆ {a, b, ...}registers𝜏, 𝜋,𝜂 ∈ Tid ⊆ {T1, T2, ...}thread identifiers𝑆 ∈ SProg ≜ {0, 1, ... ,𝑁 } → Instsequential programs𝑃 : Tid → SProg(concurrent) programs𝑒 ::= 𝑟 | 𝑣 | 𝑒 + 𝑒 | 𝑒 = 𝑒 | 𝑒 ≠ 𝑒 | ...Inst ∋ inst ::= 𝑟 := 𝑒 | if 𝑒 goto 𝑛 | 𝑥 := 𝑒 | 𝑟 := 𝑥 |𝑟 := FADD(𝑥,𝑒) | 𝑟 := XCHG(𝑥,𝑒) | 𝑟 := CAS(𝑥,𝑒,𝑒)𝑆(pc) = 𝑟 := 𝑒𝜙′ = 𝜙[𝑟 ↦→ 𝜙(𝑒)]⟨pc,𝜙⟩ 𝜀−→ ⟨pc + 1,𝜙′⟩𝑆(pc) = if 𝑒 goto 𝑛𝜙(𝑒) ≠ 0⟨pc,𝜙⟩ 𝜀−→ ⟨𝑛,𝜙⟩𝑆(pc) = if 𝑒 goto 𝑛𝜙(𝑒) = 0⟨pc,𝜙⟩ 𝜀−→ ⟨pc + 1,𝜙⟩𝑆(pc) = 𝑥 := 𝑒𝑙 = W(𝑥,𝜙(𝑒))⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙⟩𝑆(pc) = 𝑟 := 𝑥𝑙 = R(𝑥, 𝑣) 𝜙′ = 𝜙[𝑟 ↦→ 𝑣]⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙′⟩𝑆(pc) = 𝑟 := FADD(𝑥,𝑒)𝑙 = RMW(𝑥, 𝑣, 𝑣 + 𝜙(𝑒))𝜙′ = 𝜙[𝑟 ↦→ 𝑣]⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙′⟩𝑆(pc) = 𝑟 := XCHG(𝑥,𝑒)𝑙 = RMW(𝑥, 𝑣,𝜙(𝑒))𝜙′ = 𝜙[𝑟 ↦→ 𝑣]⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙′⟩𝑆(pc) = 𝑟 := CAS(𝑥,𝑒R,𝑒W)𝑙 = RMW(𝑥,𝜙(𝑒R),𝜙(𝑒W))𝜙′ = 𝜙[𝑟 ↦→ 𝜙(𝑒R)]⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙′⟩𝑆(pc) = 𝑟 := CAS(𝑥,𝑒R,𝑒W)𝑙 = R(𝑥, 𝑣)𝑣 ≠ 𝜙(𝑒R)𝜙′ = 𝜙[𝑟 ↦→ 𝑣]⟨pc,𝜙⟩ 𝑙−→ ⟨pc + 1,𝜙′⟩𝑙 ∈ Lab𝑝(𝜏) 𝑙−→𝑃 (𝜏) 𝑠′𝑝 𝜏,𝑙−−→ 𝑝[𝜏 ↦→ 𝑠′]𝑝(𝜏) 𝜀−→𝑃 (𝜏) 𝑠′𝑝 𝜏,𝜀−−→ 𝑝[𝜏 ↦→ 𝑠′]2140PLDI ’20, 六月 15-20, 2020, 伦敦, 英国 Ori Lahav 和 Udi Boker0图 1. 域、元变量和编程语言语法。0图 2. 由顺序程序 � ∈ SProg 引起的 LTS 的转换。0� 的组件的交错转换，给定为：02.3 从 LTS 到执行图我们介绍了用于为并发程序分配声明性语义的一般概念。首先，我们定义了执行图，从它们的节点开始，称为事件。0定义 2.2. 事件是一个三元组 � = � �,�,� � ，其中 � ∈ Tid是线程标识符，� ∈ N 是序列号，� ∈ Lab 是标签（定义2.1）。函数 tid 返回事件的线程标识符。函数 typ、loc、valR 和 val W 以显而易见的方式推广到事件。我们用 E表示所有事件的集合，并使用 R、W、RMW 表示其子集：R �{ � | typ ( � ) ∈ { R , RMW }}，W � { � | typ ( � ) ∈ { W ,RMW }} 和 RMW � R ∩W。上下标用于将这些集合限制为特定的位置（例如，W � ={ � ∈ W | loc ( � ) = � }）和/或线程标识符（例如，E � = { �∈ E | tid ( � ) = � }）。0我们对事件的表示引导了它们之间的偏序关系：<表示同一线程的事件根据它们的序列号进行排序（即，� � 1 ,� 1,� 1 � < � � 2 ,� 2 ,� 2 � 当且仅当 � 1 = � 2 且 � 1 < � 2）。反过来，执行图由一组事件、一个 reads-from映射（确定每个读事件从哪个写事件读取其值）和一个修改顺序（对每个位置的写进行全序排序）组成。0定义 2.3. 如果关系 rf 是事件集 � 的 reads-from关系，则满足以下条件：0• 如果 � �,� � ∈ rf ，则 � ∈ � ∩ W ，� ∈ � ∩ R ，loc ( � ) =loc ( � ) 且 val W ( � ) = val R ( � ) 。0• 如果��1,��，��2,�� ∈ rf，则�1 = �2（即rf-1 = {��,�� | ��,�� ∈rf}是功能性的）。• �� ∈ �∩R. ��. ��,�� ∈rf（每个读取事件都从某个写入事件读取）。0定义2.4.如果�是事件的集合，则mo是�的修改顺序，其中mo是关系{mo�}�∈Loc的不相交并，每个mo�是�∩W�上的严格全序。0定义2.5. 执行图�是三元组� = ��, rf,mo�，其中�是有限事件集，rf是�的读取-写入关系，mo是�的修改顺序。我们用EGraph表示所有执行图的集合。�的组成部分由�.E，�.rf，�.mo表示，�.po表示对<的限制（即�.po � {��1,�2� ∈ � × � | �1 <�2}）。对于集合��E，我们将�.E ∩ �表示为�.�（例如�.W� = �.E ∩W�）。0下一个定义用于将执行图与程序关联起来。下面的多个示例（第6页）展示了不同程序的执行图。0符号2.6. 对于事件集合�，线程标识符� ∈ Tid和标签� ∈Lab，NextEvent(�,�,�)表示由��, 1 + max ({� ∈ N | ��′ ∈ Lab. ��,�,�′� ∈�}),��给出的事件。0定义2.7. 执行图�由程序�和最终状态�生成，如果存在�0 ∈�.Q0，使得��0,�0� → � ��,��，其中�0表示空执行图（由�0 ���,�,��给出），→由以下定义：0� �,� −−→ � � ′ � ′ = � ∪ { NextEvent ( �,�,� )}0rf � rf ′ mo � mo ′0��, ��, rf, mo�� → �� ′ , �� ′ , rf ′ , mo ′ 0� �,� −−→ � � ′0��,�� → �� ′ ,��2150可判定的因果一致性共享内存PLDI'20，2020年6月15日至20日，英国伦敦03 强释放/获取模型0声明式内存模型，如StrongRelease/Acquire（SRA），通过对执行图上的约束进行集合来定义，这些约束确定了与模型兼容的一致性执行图。在本节中，我们对SRA的约束进行了定义，并定义了SRA下的安全验证问题，讨论了等效的替代形式（3.1节），提供了几个示例（3.2节），并研究了SRA和RA之间的关系（3.3节）。0符号3.1（关系）。给定关系�，dom(�)表示其定义域；�?和�+表示其自反和传递闭包；�−1表示其逆。关系�1，�2的（左）合成由�1 ; �2表示。我们用[�]表示集合�上的恒等关系，因此[�] ; � ; [∩ (� × �)。0因果一致性模型基于以下基本的派生的happens-before关系：0�.hb � (�.po ∪ �.rf)+0happens-before关系捕捉了执行图中的因果关系。换句话说，hb是包含程序顺序（po）和读取-写入（rf）关系的最小传递关系。我们注意到所有的读取都与它们读取的写入进行同步（rf � hb），与更复杂的模型（如RC11[34]）不同，在这些模型中，只有某些读取-写入边缘引发同步。给定hb，SRA模型由三个约束组成，每个约束禁止执行图中的某种模式。这三个不允许的模式如下所示：0E0( hb ∪ mo ) +0不可约hb-mo0W � W0R �0rf hb0mo0读取一致性0W � W0RMW �0rf mo0mo0原子性0irr-hb-mo。这个约束要求修改顺序mo与因果顺序一致：0（�.hb∪�.mo）+是非自反的（irr-hb-mo）0特别地，它意味着�.hb确实是一个偏序。因此，SRA禁止所谓的load-buffering行为[39]，除非适当限制，否则会导致臭名昭著的out-of-thin-air问题[13, 26]。0读一致性。这个约束直观地要求线程在知道同一位置的后续写入时不能读取值。将线程�知道某个写事件�解释为从�到（某个事件的）�的hb路径，并使用修改顺序mo来解释一个写在另一个写之后，精确的条件要求：0�.mo; �.hb; �.rf−1是非自反的（读一致性）0实际上，如果一个读事件�从一个写事件�1中读取，同时知道同一位置的一个mo-later写事件�2，我们有��1,�2�∈mo，��2,��∈hb和��,�1�∈rf−1。0原子性。这个条件确保了RMW比读后写更强。它要求RMW从其直接的mo前驱中读取：0�.mo; �.mo; �.rf−1是非自反的（原子性）0换句话说，如果一个RMW事件�从一个写事件�中读取，那么在�和�之间不能有其他写事件介入。我们将满足上述三个条件的执行图称为SRA一致。根据这个定义，我们可以正式地提出SRA下的可达性问题，在本文中我们证明了这个问题是可判定的。0定义3.2.如果程序�生成了一些SRA一致的执行图，并且最终状态为�（参见定义2.7），则我们称程序�的状态�在SRA下是可达的。0定义3.3（SRA可达性）。SRA下的可达性问题如下：输入：一个程序�和一个不良状态�∈�。Q。问题：在SRA下，�是否可达？0通过从有损FIFO通道机器的可达性进行约简，可以实现对该问题的较低复杂度下界，这直接遵循Atig等人[11]对x86-TSO下安全性验证的类似约简。0定理3.4. SRA可达性是非原始递归的。03.1SRA的其他表述。我们上面的表述遵循[30]，其中SRA被引入为RA的加强。后者是C/C++11模型[14,34]的片段，包括发布存储、获取读取和获取-发布RMW。此外，SRA在文献中以多种伪装形式出现：0POWER.如[30]中所证明的，当将后者限制为通过标准编译方案[38]（即在每个存储之前放置lwsync并在每个加载之后放置ctrl+isync）编译C/C++11程序的发布/获取片段时，SRA与[9]的POWER模型完全一致。0分布式键值存储。忽略RMW，SRA模型等价于[16]中的因果收敛模型（CCv）（当应用于标准读/写内存顺序规范时），以及[37]中的因果一致性模型，当限制为单指令事务时。这些模型在[18,20]中以可见性（���）和仲裁（��）关系的形式进行了阐述。将���=hb，并将��设置为扩展hb∪mo的某个全序，可以得到这种对应的一个方向。对于反向的情况，我们将rf与同一位置的��-最大写相关联，该写在�之前是���-之前的。2160PLDI '20，2020年6月15日至20日，英国伦敦Ori Lahav和Udi Boker0并设置mo =��∈Loc[W�];��;[W�]。此外，我们的程序顺序（po）对应于会序（��），而SRA的一致性确保了强会话保证（������）[47]。式数据库中，RMW需要昂贵的全局协调。将RMW的天真实现为从/到同一位置读取和写入的事务不保证原子性，因为它允许丢失更新异常（例如，它将允许下面的Ex.3.9中的结果）。在某些位置仅由RMW访问的特定情况下，它的访问由hb完全排序，这对应于将某些事务标记为可串行化，如[15, 36]中的Red-Blue模型。0并行快照隔离。当所有存储指令都使用原子交换来实现（将x:= e实现为r :=XCHG(x,e)）时，SRA精确地捕捉到并行快照隔离模型（PSI）[10, 15, 19, 43,45]，限制为单指令事务。因此，我们对SRA的可决定性结果包含了对具有单指令事务的PSI的可决定性。03.2示例我们列举一些众所周知的litmus测试，以演示SRA（其中一些在后续部分中重新讨论）。为了简化演示，我们不是引用可达的程序状态，而是考虑将最终值分配给（某些）寄存器的可能程序结果。如果在SRA下可以达到某些状态，其中寄存器被分配了它们在O中的值，则允许程序在声明性模型SRA下的结果O（参见Def. 3.2）。我们使用程序注释注释（ł //ž）来表示特定的结果。0注1.为了简化我们的演示，我们要求内存位置的显式初始化，并将示例调整为包括显式初始化。从未初始化的位置读取会阻塞线程。（例如，由单个线程组成的程序从某个位置读取，而没有先写入该位置，只生成初始执行图G0。）这只是一种演示方式：可以通过向程序添加额外的线程来实现隐式初始化，该线程将所有变量设置为其初始值，然后通知所有其他线程（使用额外的标志）开始运行。0例3.5（存储缓冲）。以下程序结果是SRA允许的。0x := 0 x:= 1 a :=y // 00y := 0 y:= 1 b :=x // 00� SRA0W(x, 0) W(y, 0)0W(x, 1)0R(y, 0)0W(y, 1)0R(x, 0)0mo0rf0mo0rf0(SB)0在其执行图中，由于读取的值，强制执行rf边，而由于irr-hb-mo，强制执行mo边。可以轻松验证执行图是SRA一致的。0例3.6（消息传递）。SRA支持非常常见的“基于标志”的同步。也就是说，以下结果是不允许的：0x := 0x := 1y := 10a := y // 1b := x // 00� SRA0W(x, 0)0W(x, 1)0W(y, 1)0R(y, 1)0R(x, 0)0rf0mo0(MP)0此结果的执行图必须具有如上所示的rf和mo边。然而，我们从W(x, 0)到W(x, 1)有mo，从W(x, 1)到R(x, 0)有hb，从W(x,0)到R(x,0)有rf。因此，读一致性不成立，执行图不是SRA一致的。0例3.7（传递消息传递）。在因果一致性中，po和rf边对hb的贡献相同。因此，与Ex. 3.6一样，以下结果不被SRA允许。0x := 0y := 10a := y //1 x := 10b := x // 1 c := x// 0 � SRA0R（y，1）0R（x，1）0R（x，0）0rf mo0（MP-trans）0例3.8（独立读取独立写入）。SRA与x86-TSO模型[42]之间的一个主要区别是前者是非多副本原子的。换句话说，不同的线程可以以不同的顺序观察到不同的存储。因此，与x86-TSO不同，SRA模型允许以下结果，其中T2观察到W（x，1）但不观察到W（y，1），而T3观察到W（y，1）但不观察到W（x，1）。0x := 0x := 10a := x // 1b := y // 00c := y // 1d := x // 00y := 0 y := 1 �SRA0W（x，0））0R（x，1）0R（y，0）0R（y，1）0R（x，0）W（y，1）0mo mo rf rf0（IRIW）0例3.9。对于锁的实现，两个RMW永远不会从同一个写入读取：0x := 0 a :=CAS（x，0，1）// 00b :=CAS（x，0，1）// 00� SRA0RMW（x，0，1）RMW（x，0，1）0rf rf（2RMW）0由于mo必须对两个RMW进行排序，并且irr-hb-mo指示mo;rf是非自反的，因此RMW的任何顺序都会导致原子性的违反。0例3.10。对于未使用的位置的RMWs可以用作栅栏，因为一致性约束意味着hb必须完全排序�.W�，当除了一个（初始化）写入事件外，�中对�的所有写入事件都是RMWs。例如，放置这样的栅栏禁止了SB程序的弱结果（Ex.3.5）。此结果的执行图必须具有右侧所示的边缘，并且任何选择的2170可判定的验证在因果一致的共享内存PLDI '20，2020年6月15日至20日，英国伦敦0缺失的rf-边缘（到两个RMW事件）将违反SRA的条件。0z := 0 x := 0 x:= 1 a :=FADD（z，0）b := y // 00y := 0 y := 1 a:=FADD（z，0）c := x // 00� SRA0W（x，0）W（y，0）0R（y，0）0R（x，0）0rf（SBF）03.3 关于RA模型的关系0RA模型比SRA模型更弱。它强加了读一致性和原子性，就像SRA一样，但是它只不允许以下模式：0E0hb0irr-hb0W�0W �0hb mo0写一致性0首先，irr-hb要求hb是一个偏序：0�. hb是非自反的（irr-hb）0其次，RA只需要mo和hb之间的局部一致性，而不是全局一致性：0�. mo ; �. hb是非自反的（写一致性）0换句话说，如果hb对同一位置的两次写进行排序，那么mo必须按照相同的顺序进行。0例子3.11.hb∪mo中只涉及一个位置的循环是被写一致性所禁止的（使用mo对同一位置的写是完全的事实）。相反，irr-hb-mo（SRA的）也限制了[W�];mo;[W�]和[W�];mo;[W�]之间的关系即使�≠�。下面的例子（改编自[50]）展示了这种差异：0x := 1 y:= 2 a :=y // 10y := 1 x:= 2 a :=x // 10� RA � SRA0W(x, 1)0W(y, 2)0R(y, 1)0W(y, 1)0R(x, 1)0mo0rf (2+2W)0这种结果的执行图必须具有如上所示的rf和mo边（以满足读一致性），并且它包含一个(hb∪mo)-循环，这在RA下是允许的，但在SRA下是不允许的。0由于irr-hb-mo蕴含irr-hb和写一致性，因此以下显然成立：0命题3.12. SRA一致性蕴含RA一致性。0RA下的可达性与SRA下的可达性类似（在Def.3.2中将łSRAž替换为łRAž）。然后，我们清楚地知道在SRA下可达的�的所有状态也在RA下可达。反之不一定成立，但对于大型和广泛使用的无写/写竞争程序类来说是成立的。受DRF模型[8]的启发，我们展示了写
