释放+获取可以打破发生之前吗？

Question

当今许多编程语言都具有happens-before关系和release+acquire同步操作。

\n

其中一些编程语言：

\n

\n
• C/C++11：发生之前，释放+获取
\n
• Rust和Swift完全采用了 C/C++ 内存模型 \xe2\x80\x94，所以他们也有这个模型。
\n
• Java：发生在之前，释放+获取。
\n

\n

我想知道是否release+acquire可以违反happens-before：

\n

\n
• 如果可能的话，我想看一个例子
\n
• 如果不可能，那么我想得到简单明了的解释
\n

\n

---

\n

什么是release+acquire和happens-before

\n

Release/acquire建立happens-before不同线程之间的关系：换句话说，保证releasein之前的所有内容在afterThread 1中可见：Thread 2acquire

\n

 \\     Thread 1                        /            \n  \\    --------                       /             \n   \\   x = 1                         / Everything   \n    \\  y = 2                        /    here...    \n     \\ write-release(ready = true) /                \n      \xe2\x94\x94\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x98                 \n                   |                                \n                   \xe2\x94\x94\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x90 (happens-before) \n                                 V                  \n                    \xe2\x94\x8c\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x90     \n                   / Thread 2                  \\    \n ...is visible to /  --------                   \\   \n    everything   /   read-acquire(ready == true) \\  \n     here       /    assert(x == 1)               \\ \n               /     assert(y == 2)                \\\n

\n

不仅如此，happens-before还有严格的偏序。
\n这意味着它是：

\n

\n
• 传递性：Thread 2保证不仅可以看到 所做的写入Thread 1，还可以Thread 1看到其他线程的所有写入
\n
• 不对称：要么a发生在之前b，要么b发生在之前a，两者都不允许
\n

\n

---

\n

为什么我认为这release/acquire可能会破坏happens-before

\n

正如我们从 IRIW litmus 测试中得知的，release/acquire可能会导致两个线程以不同的顺序查看来自不同线程的写入（对于 C++，另请参阅此处的最后一个示例，以及来自 gcc wiki 的这 两个示例）：

\n

// Thread 1\nx.store(1, memory_order_release);\n// Thread 2\ny.store(1, memory_order_release);\n// Thread 3\nassert(x.load(memory_order_acquire) == 1 && y.load(memory_order_acquire) == 0)\n// Thread 4\nassert(y.load(memory_order_acquire) == 1 && x.load(memory_order_acquire) == 0)\n

\n

这里两个asserts 都可以通过，这意味着Thread 3和see以不同的顺序Thread 4写入 和x。y

\n

据我了解，如果它是普通变量，那么这将违反发生之前的不对称属性。\n但是因为 x 和 y 是原子，所以没关系。\n（顺便说一句，我对此不确定）
\nNate Eldredge在他的回答中证明了这个 IRIW 示例是可以的。

\n

但我仍然有一个潜在的怀疑，可能存在类似于 IRIW 的东西，这会导致Thread 3并Thread 4看到以不同顺序发生的常规写入 \xe2\x80\x94 这会破坏发生之前（它不会是传递性的）不再）。

\n

---

\n

注1

\n

在cppreference中也有这样的引用：

\n

\n

需要实现来确保发生之前关系是非循环的，必要时引入额外的同步（只有在涉及消耗操作时才有必要，请参阅 Batty 等人）

\n

\n

引用暗示可能存在happens-before违反并且需要额外同步的情况（“非循环”意味着发生在形成有向非循环图，这相当于说“严格偏序”）。

\n

如果可能的话我想知道这些情况是什么。

\n

---

\n

笔记2

\n

由于java允许数据竞争，我也对happens-before仅在存在数据竞争时违反的情况感兴趣。

\n

---

\n

编辑 1（2021 年 11 月 3 日）

\n

举个例子，这里解释了为什么顺序一致（SC）原子不能违反happens-before.
\n（对释放/获取原子的类似解释将是我问题的答案）。

\n

我所说的“违反happens-before”是指“违反 的公理happens-before，这是严格的偏序”。

\n

严格偏序直接对应于有向无环图（DAG）。

\n

以下是来自 wiki 的 DAG 示例（请注意，它没有循环）：
\n

\n

让我们证明 SC 原子happens-before图保持非循环。

\n

请记住，SC 原子按全局顺序发生（对于所有线程都相同），并且：

\n

\n
• 该顺序与每个线程内的操作顺序一致
\n
• 每个 SC 原子读取都会按照此总顺序对同一变量看到最新的 SC 原子写入
\n

\n

看这个happens-before图：

\n

 Thread1  Thread2  Thread3 \n =======  =======  ======= \n    \xe2\x94\x82        \xe2\x94\x82        \xe2\x94\x82    \n   W(x)      \xe2\x94\x82        \xe2\x94\x82    \n    \xe2\x86\x93        \xe2\x94\x82        \xe2\x94\x82    \n   Sw(a) \xe2\x94\x90   \xe2\x94\x82       W(y)  \n    \xe2\x94\x82    \xe2\x94\x82   \xe2\x94\x82        \xe2\x86\x93    \n    \xe2\x94\x82    \xe2\x94\x94> Sr(a)  \xe2\x94\x8c Sw(b) \n    \xe2\x94\x82        \xe2\x86\x93     \xe2\x94\x82  \xe2\x94\x82    \n    \xe2\x94\x82       Sr(b)<\xe2\x94\x80\xe2\x94\x98  \xe2\x94\x82    \n    \xe2\x94\x82        \xe2\x86\x93        \xe2\x94\x82    \n    \xe2\x94\x82       R(x)      \xe2\x94\x82    \n    \xe2\x94\x82        \xe2\x86\x93        \xe2\x94\x82    \n    \xe2\x94\x82       R(y)      \xe2\x94\x82    \n    \xe2\x94\x82        \xe2\x94\x82        \xe2\x94\x82    \n    V        V        V    \n

\n

在图表上：

\n

\n
• 时间向下流动
\n
• W(x)是R(x)常规操作：写入和读取x
\n
• Sw(a)是Sr(a)SC 原子：写入和读取a
\n
• 在每个线程中，操作按照程序顺序（也称为sequenced-before orderC++）发生：按照它们在代码中的顺序
\n
• 线程之间happens-before是由 SC 原子建立的
\n

\n

请注意，图上的箭头始终向下
\n=> 图不能有循环
\n=> 它始终是 DAG
\n=>happens-before不能违反公理

\n

同样的证明不适用于release/acquire原子，因为（据我所知）它们不会以全局顺序发生=> 之间的 HB 箭头Sw(a)可能Sr(a)向上=> 一个循环是可能的。（对此我不确定）

\n

Answer 1

Happens-before 是equenced-before 和synchronized-with 的传递闭包。Sequenced-before 只是每个线程内的程序顺序，synchronized-with 在获取加载从发布存储中获取其值时发生。因此，在您的程序中，为了使两个断言都通过，必须满足以下关系：

1. T3.x==1发生在T3.y==0（排序）之前
2. T4.y==1发生在之前T4.x==0（同样）
3. T1.x=1发生在之前T3.x==1（获取负载从发布存储中获取其值）
4. T2.y=1发生在之前T4.y==1（同样）
5. T1.x=1发生在之前T3.y==0（为了传递性）
6. T2.y=1发生在之前T4.x==0（同样）

您可以检查这是否满足部分排序的所有公理（反对称和传递）以及两个断言传递所隐含的所有 C++ 一致性规则。例如，它一定不是T2.y=1之前发生的情况T3.y==0，而且我们的排序中确实不存在这种关系。T3.y==0但以前发生的事情也不是真的T2.y=1，这也没有什么问题；毕竟 这是一个部分订单。T2.y=1并且T3.y==0完全是无序的。

由于存在与两个断言传递一致的有效的happens-before排序，因此当您运行程序时，两个断言可能都会通过。

确实，如果在任一方向上T3.y==0和 之间存在某种发生前关系，并且在和 之间同样存在，那么每种组合都会导致违反规则：要么违反一致性，要么出现偏序循环。但同样，它们无序是完全可以的，这样就不会发生违规行为。T2.y=1T4.x==0T1.x=1

如果加载和存储都是宽松的，或者即使 和x根本y不是原子的，那么任何规则都不会暗示上面的关系 3 和 4，因此发生在排序之前将变得简单：

1. T3.x==1发生在T3.y==0（排序）之前
2. T4.y==1发生在之前T4.x==0（同样）

这也与通过的两个断言一致。（在非原子情况下，T1.x=1负载无序的事实x意味着存在数据竞争，因此该行为在 C++ 中是未定义的。在 Java 等不同语言中，我们可能已经定义了行为，表示两个负载成功并返回 0 或 1，但我们仍然可以让两个断言都通过。）如果您认为将程序更改为使用非原子加载和存储会阻止两个断言通过，那么您就错了。

因此，获取和释放实际上加强了排序；必须存在更多的关系，并且程序的行为也将得到更好的定义。

Answer 2

答案：不，释放/获取不能破坏happens-before。

\n

Nate Eldredge 在评论中给出了证明：

\n

\n

哦，确实如此。事实上，我可能会看看如何证明这一点。HB 关系通过其构造是传递的。顺序关系是非循环的，因此如果 HB 中存在循环，则它必须至少包含一个同步步骤，粗略地说，这是一个从释放存储 S 中获取其值的获取加载 L。但是由于循环，L 发生在 S 之前。因此，到 p14，L 必须从 S 以外的某个存储中获取其值，矛盾。不完全是一个证明，因为我过度简化了atomics.order p2 中的synchronizes-with 的定义，但它只是一个开始。

\n

\n

我只是想把它放在一个单独的答案中，以便人们更容易注意到。

\n

另外，这里有我的额外解释（也许这会让某些人更容易理解）。

\n\n

首先，如果我们只使用release/acquire原子和非原子内存访问，那么happens-before通过构造是传递的（并且是非循环的）。

\n

与图类似SC，release/acquire边也总是指向下方：

\n

Thread1   Thread2   Thread3   Thread4\n=======   =======   =======   =======\n   \xe2\x94\x82         \xe2\x94\x82         \xe2\x94\x82         \xe2\x94\x82   \n   \xe2\x94\x82    \xe2\x94\x8c Wrel(a)\xe2\x94\x90     \xe2\x94\x82         \xe2\x94\x82   \nRacq(a)<\xe2\x94\x98    \xe2\x94\x82   \xe2\x94\x82\xe2\x94\x8c Wrel(b)\xe2\x94\x90     \xe2\x94\x82   \n   \xe2\x86\x93         \xe2\x94\x82   \xe2\x94\x82\xe2\x94\x82    \xe2\x94\x82   \xe2\x94\x94> Racq(b)\nRacq(b)<\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x82\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x82\xe2\x94\x98    \xe2\x94\x82         \xe2\x86\x93   \n   \xe2\x94\x82         \xe2\x94\x82   \xe2\x94\x94\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x82\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80> Racq(a)\n   \xe2\x94\x82         \xe2\x94\x82         \xe2\x94\x82         \xe2\x94\x82   \n   V         V         V         V   \n

\n

_{（顺便说一句，请注意，该图与SC:Thread 1和Thread 4see不同Wrel(a)，并且Wrel(b)顺序不同。但边缘仍然指向下方）}

\n

Wrel(x)从到 的边缘Racq(x)始终指向下方，因为Racq(x)看到之前的所有内容Wrel(x)都已完成（请参阅答案末尾的注释）。\n（在 C++ 规范中，这称为，您可以在此处了解更多信息。） Wrel(x)
synchronizes-with

\n

因此，与SC图类似，所有边总是向下
\n=> 图不能有循环
\n=> 它始终是 DAG
\n=>happens-before不能违反公理

\n

实际上happens-before由原子 \xe2\x80\x94 产生的基本上是Leslie Lamport在《分布式系统中的时间、时钟和事件排序》中release/acquire的原始介绍。\n我真的建议所有对\xe2\x80\x94 感兴趣的人阅读这篇论文 Lamport 的解释简短而清晰，而且这个想法真的很酷。happens-before
HB

\n\n

我们还用图片来演示为什么循环是不可能的。

\n

这是一个循环的样子：

\n

 Thread1    Thread2    Thread3   \n =======    =======    =======   \n    \xe2\x94\x82          \xe2\x94\x82          \xe2\x94\x82      \n  Racq(a)<\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x82\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x82\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x80\xe2\x94\x90\n    \xe2\x86\x93          \xe2\x94\x82          \xe2\x94\x82     \xe2\x94\x82\n  Wrel(b) \xe2\x94\x90    \xe2\x94\x82          \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82     \xe2\x94\x82    \xe2\x94\x82          \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82     \xe2\x94\x94> Racq(b)      \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82          \xe2\x86\x93          \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82        Wrel(c) \xe2\x94\x90    \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82          \xe2\x94\x82     \xe2\x94\x82    \xe2\x94\x82     \xe2\x94\x82\n    \xe2\x94\x82          \xe2\x94\x82     \xe2\x94\x94> Racq(c) \xe2\x94\x82\n    \xe2\x94\x82          \xe2\x94\x82          \xe2\x86\x93     \xe2\x94\x82\n    \xe2\x94\x82          \xe2\x94\x82        Wrel(a) \xe2\x94\x98\n    \xe2\x94\x82          \xe2\x94\x82          \xe2\x94\x82      \n    V          V          V      \n

\n

每个线程内happens-before都有源代码中的操作顺序（sequenced-before在 C++ 和program orderJava 中称为）。
\n显然，HB这里不可能有循环。

\n

这意味着“返回”并关闭循环的边必须是像上图中的边synchronizes-with一样的边。Wrel(a)->Racq(a)

\n

注意一个矛盾：

\n

\n
• Wrel(a)必须在 之前完成Racq(a)，因为Racq(a)读取由 写入的值Wrel(a)
\n
• Racq(a)必须在之前完成Wrel(a)，因为有一个链Racq(a)->Wrel(b)->Racq(b)->Wrel(c)->Racq(c)->Wrel(a)，其中每个Wrel(x)（及其之前的所有内容）在Racq(x)读取之前完成。
\n

\n

这意味着Wrel(a)->Racq(a)边缘是不允许的 => 循环是不可能的。

\n

就 C++ 内存模型而言，它违反了一致性要求：

\n

\n

由评估 B 确定的原子对象 M 的值应是由修改 M 的某些副作用 A 存储的值，其中 B 不会在 A 之前发生。

\n

\n\n

笔记。

\n

我指出：

\n

\n

Racq(x)看到之前的一切Wrel(x)都已完成 Wrel(x)

\n

\n

但在 C++ 标准中并没有直接说明。
\n相反，它有这个：

\n

\n
• happens-before定义了阅读所看到的内容
\n
• Racq(x)和之间的关系Wrel(x)称为synchronizes-with
\n
• happens-beforesynchronizes-with由大量其他规则和命令构建而成
\n

\n

可以从 C++ 标准推导出我的陈述，尽管这可能并不容易。（这就是为什么我建议阅读这篇文章）。

\n

我使用该语句是因为它简洁地描述了内存屏障指令的作用，并且这就是如何happens-before（并且可能是）轻松实现的。
\n通常，我们只需要实现一条内存屏障指令happens-before及其所有数学属性。
\n对于不同 CPU 上的这些指令的概述，我推荐Paul E. McKenney 的《内存屏障：软件黑客的硬件视图》中的相关部分。\n（例如，PowerPC 中的内存屏障基本上与C++ 中的原子作用
相同）release/acquire

\n