C++23中std::memory_order_seq_cst的先行关系及内存序优化问题

示例代码 #

#include <atomic>
#include <thread>
#include <cassert>

std::atomic<int> x{0}, y{0};
int r1, r2;

void thread1() {
    x.store(1, STORE_ORDER);
    r1 = y.load(LOAD_ORDER);
}

void thread2() {
    y.store(1, STORE_ORDER);
    r2 = x.load(LOAD_ORDER);
}

int main() {
    std::thread t1(thread1);
    std::thread t2(thread2);
    t1.join();
    t2.join();
    assert(r1 == 1 || r2 == 1); // 要求该断言永不失败
}

问题1：全seq_cst内存序下的正确性证明 #

基于C++标准的核心概念推导：

1. 先序于（sequenced before）：同一线程内代码顺序靠前的操作先序于靠后的操作。即thread1中x.store(1, seq_cst)先序于y.load(seq_cst)；thread2中y.store(1, seq_cst)先序于x.load(seq_cst)。
2. 同步于（synchronizes with）：所有seq_cst操作构成一个全局全序（total order），该顺序无环且满足传递性。
3. 线程间先行于（inter-thread happens before）：若操作A在全局seq_cst顺序中先于操作B，则A线程间先行于B。
4. 可见副作用（visible side effect）：seq_cst load会读取全局全序中位于它之前的最后一个同变量seq_cst store的值。

反证法推导： #

假设断言失败，即r1 == 0且r2 == 0：

• r1 == 0说明thread1的y.load(seq_cst)读取到y的初始值，因此在全局seq_cst顺序中，该load必须先于thread2的y.store(seq_cst)。
• r2 == 0说明thread2的x.load(seq_cst)读取到x的初始值，因此在全局seq_cst顺序中，该load必须先于thread1的x.store(seq_cst)。

结合线程内先序关系，会形成全局顺序的循环链：
x.store(thread1) < y.load(thread1) < y.store(thread2) < x.load(thread2) < x.store(thread1)
这直接违反了全局全序的无环性，因此假设不成立，断言永不失败。

问题2：部分放松内存序的正确性分析 #

情况1：LOAD_ORDER=relaxed，STORE_ORDER=seq_cst #

该设置不正确，断言可能失败。
relaxed load不参与seq_cst全局全序，也没有获取语义，仅保证线程内的先序关系。即使thread2的y.store(seq_cst)已执行，thread1的y.load(relaxed)仍可能读取到y的初始值；同理thread2的x.load(relaxed)也可能读取到x的初始值，最终两个load都返回0，断言失败。

情况2：STORE_ORDER=relaxed，LOAD_ORDER=seq_cst #

该设置不正确，断言可能失败。
relaxed store没有发布语义，不参与seq_cst全局全序。seq_cst load仅保证读取全局全序中之前的seq_cst store值，因此thread1的y.load(seq_cst)可能始终读取初始值0，thread2的x.load(seq_cst)同理，最终断言失败。

问题3：最宽松的内存序组合 #

保证断言不失败的最宽松（最高效）内存序组合是：
STORE_ORDER = std::memory_order_release，LOAD_ORDER = std::memory_order_acquire

正确性说明： #

• release store：保证线程内所有先于该store的操作的副作用，对后续读取该变量的acquire load可见。
• acquire load：保证线程内所有后于该load的操作，能看到该load读取到的store操作之前的所有副作用。

用反证法推导：
假设断言失败，即r1 == 0且r2 == 0：

• r1 == 0说明thread1的y.load(acquire)未看到thread2的y.store(release)，即y.store(release)不线程间先行于y.load(acquire)。
• r2 == 0说明thread2的x.load(acquire)未看到thread1的x.store(release)，即x.store(release)不线程间先行于x.load(acquire)。

结合线程内先序关系x.store(release) < y.load(acquire)、y.store(release) < x.load(acquire)，会形成逻辑循环：x.store → y.load → y.store → x.load → x.store，这违反了C++标准的执行一致性规则，因此假设不成立，断言永不失败。

该组合的开销远低于seq_cst，且是满足要求的最宽松设置——任何更宽松的组合（如relaxed store/load）都无法保证必要的可见性和同步关系。

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