seq_cst 命令如何正式保证 IRIW 石蕊测试的结果？

Question

考虑cppreference 中的这个示例

#include <thread>
#include <atomic>
#include <cassert>
 
std::atomic<bool> x = {false};
std::atomic<bool> y = {false};
std::atomic<int> z = {0};
 
void write_x()
{
    x.store(true, std::memory_order_seq_cst);  // #1
}
 
void write_y()
{
    y.store(true, std::memory_order_seq_cst); // #2
}
 
void read_x_then_y()
{
    while (!x.load(std::memory_order_seq_cst))  // #3
        ;
    if (y.load(std::memory_order_seq_cst)) {  // #4
        ++z;
    }
}
 
void read_y_then_x()
{
    while (!y.load(std::memory_order_seq_cst))  // #5
        ;
    if (x.load(std::memory_order_seq_cst)) {  // #6
        ++z;
    }
}
 
int main()
{
    std::thread a(write_x);
    std::thread b(write_y);
    std::thread c(read_x_then_y);
    std::thread d(read_y_then_x);
    a.join(); b.join(); c.join(); d.join();
    assert(z.load() != 0);  // will never happen
}

为了证明assert永远不会发生，我们应该证明要么y-store发生在 之前y-load-in-if，要么x-store发生在 之前x-load-in-if，或者两者都发生。他们将保证 的值z至少应大于 0，这使得这种情况assert永远不会发生，按照以下规则。

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

如果修改原子对象M的操作A发生在修改M的操作B之前，则A在M的修改顺序上应早于B。

如果原子对象 M 的值计算 A 发生在 M 的值计算 B 之前，并且 A 从 M 上的副作用 X 获取其值，则 B 计算的值应为 X 存储的值或存储的值由 M 上的副作用 Y 决定，其中 Y 在 M 的修改顺序中位于 X 之后。

如果原子对象 M 的值计算 A 发生在修改 M 的操作 B 之前，则 A 应从 M 上的副作用 X 中获取其值，其中 X 在 M 的修改顺序中先于 B。

如果原子对象 M 上的副作用 X 发生在 M 的值计算 B 之前，则评估 B 应从 X 或按照 M 的修改顺序从 X 后面的副作用 Y 获取其值。

然而我们只能具备这些条件

1. x-store synchronizes x-load-in-while
2. y-store synchronizes y-load-in-while
3. x-load-while is sequenced before y-load-in-if
4. y-load-while is sequenced before x-load-in-if 

根据 [intro.races] p10，项目符号 1 和 3 给出：

x-store 线程间发生在 y-load-in-if 之前

第 2 条和第 4 条给出：

y-store 线程间发生在 x-load-in-if 之前

然后，我找不到任何关联可以证明y-store发生在之前y-load-in-if，或x-store发生在之前x-load-in-if。这种情况的特殊之处在于它们都是seq操作，所以还有一个额外的规则，称为单全序S。即使有了这个规则，我也只能得出以下结论：

1. x-store < x-load-in-while < y-load-in-if, in S
2. y-store < y-load-in-while < x-load-in-if, in S

符号的<意思在前。除了这些结论之外，我无法获得更多信息来解释为什么该断言永远不会发生。如何正确使用当前的C++标准来解释这种情况？

Answer 1

两者++z（ at#4和#6）都发生z.load()在main（[thread.thread.member]/4，[intro.races]/9，/10.2）之前，如果它们发生的话。

这些副作用必然对负载 ( [intro.races]/18 ) 可见，因此触发 的唯一方法assert是同时读取#4和。#6false

在 中read_x_then_y，#3读取true由 写入#1，含义在( [atomics.order]/3.1#1 )之前是连贯排序的，并且强烈发生在( [intro.races]/12.1 )的加载之前。#3#3y#4

#4读取false会使其在写入trueat #1( [atomics.order]/3.3，其中X是 的初始“写入” false) 之前保持连贯有序。

这里需要澄清几点：

• [atomics.order]/3.3 的第一部分只是指出A和B必须是不同的原子操作，它并不将本项目符号的范围限制为仅读取-修改-写入操作。P0668，介绍该措辞的论文总结道：

  第三个项目对应于通常所说的“先读”：A 比 B 更早读取写入。

• 从技术上讲，对象的初始化不是副作用，这是CWG2587的主题，并且不是原子所独有的。我认为很明显，这里的意图是这些规则在谈论副作用时包括初始化。

• （常量）y发生 before的初始化#2是标准（至少根据我的阅读）未能明确指定的另一点，但我们可以再次应用常识：如果它没有发生 before #2，则该程序具有未定义的行为，因为它访问过期对象（[res.on.objects]/2），任何进一步的分析都是没有意义的。这当然是荒谬的，所以我们假设这#2实际上发生在y初始化之后，因此它遵循y( [intro.races]/15 ) 的修改顺序的初始化。

此分析为我们提供了在读取执行时操作的#1 < #3 < #4 < #2总顺序Sseq_cst ( [atomics.order]/4 )的排序。#4read_x_then_yfalse

重复相同的操作read_y_then_x（再次假设#6gets false）会产生#2 < #5 < #6 < #1。

在第一种情况下，#1先#2于S，在第二种情况下，#2先于#1。显然，不可能有S与这两者一致，这意味着#4并且#6不能同时读取false该程序的任何可能执行。再次引用P0668：

如果任何总阶数 S 都不能满足这些约束，则产生一致性阶数的候选执行无效。