如何依据C++标准解释seq_cst在IRIW测试中保证断言不触发？

示例代码（来自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(z.load() != 0)永远不会触发，核心是要证明**y.store（#2）happens before y.load（#4）** 或者 x.store（#1）happens before x.load（#6） 至少成立一个，这样z的值至少为1。

目前已推导出以下基础条件：

• x.store（#1）与x.load（#3）构成synchronizes-with关系
• y.store（#2）与y.load（#5）构成synchronizes-with关系
• x.load（#3）在同一线程中sequenced before y.load（#4）
• y.load（#5）在同一线程中sequenced before x.load（#6）

由此可进一步推导：

• x.store（#1）inter-thread happens before y.load（#4）
• y.store（#2）inter-thread happens before x.load（#6）

但无法直接推导出y.store与y.load（#4）、x.store与x.load（#6）的happens-before关系。结合seq_cst的全局总序S，仅能得到：

• 在S中，x.store（#1） < x.load（#3） < y.load（#4）
• 在S中，y.store（#2） < y.load（#5） < x.load（#6）
  （<表示全局总序中的“先于”关系）

依据C++标准的正式解释 #

根据C++标准对memory_order_seq_cst的定义，所有seq_cst原子操作（store、load、read-modify-write）必须构成一个单一的全局总序S，且该总序需满足两个核心约束：

1. 与线程内顺序一致：同一线程中的seq_cst操作，在S中的顺序必须和线程内的sequenced-before顺序匹配。
2. 与synchronizes-with关系一致：若seq_cst store操作A与seq_cst load操作B构成synchronizes-with关系，则在S中A必须先于B。

我们用反证法推导：假设assert(z.load() == 0)成立，即两个if分支都不执行，意味着：

• y.load（#4）读取到false → 在S中y.load（#4）先于y.store（#2）
• x.load（#6）读取到false → 在S中x.load（#6）先于x.store（#1）

结合之前的全局总序关系，会得到一个循环链：
x.store（#1） < x.load（#3） < y.load（#4） < y.store（#2） < y.load（#5） < x.load（#6） < x.store（#1）

这直接违反了全局总序S的传递性和非循环性（全序关系不允许存在循环），因此假设不成立。

结论：不可能同时出现y.load（#4）读false和x.load（#6）读false的情况，至少有一个load操作会读到true，z的值至少为1，assert(z.load() != 0)永远不会触发。

内容的提问来源于stack exchange，提问作者xmh0511