线程3中的断言是否必然成立？原子同步内存序分析疑问

x = 0; // 初始值为0
y = 0; // 初始值为0

// 线程1：使用释放语义存储
y.store(20, memory_order_release); 
x.store(10, memory_order_release);

// 线程2：使用获取语义加载
if (x.load(memory_order_acquire) == 10) {
  assert(y.load(memory_order_acquire) == 20);
  y.store(10, memory_order_release); // 释放语义存储
}

// 线程3：使用获取语义加载
if (y.load(memory_order_acquire) == 10) {
  assert(x.load(memory_order_acquire) == 10);
}

若线程3中的if语句未执行，则断言不会触发，因此只需考虑if语句执行的情况：这意味着线程3对y的加载操作观测到了线程2对y赋值为10的存储操作，而这要求线程2的if语句执行，进而要求线程2对x的加载操作观测到线程1对x的存储值。因此，若线程3的断言被触发，需满足以下条件：

1. 线程1中对x的存储同步于线程2中对x的加载
2. 线程2中对y的存储同步于线程3中对y的加载

由此可得到完整条件：

p1: 线程1中对y的存储先行发生于线程1中对x的存储
p2: 线程1中对x的存储同步于线程2中对x的加载
p3: 线程2中对x的加载先行发生于线程2断言中对y的加载
p4: 线程2断言中对y的加载先行发生于线程2中对y的存储
p5: 线程2中对y的存储同步于线程3中对y的加载
p6: 线程3中对y的加载先行发生于线程3中对x的加载

基于这些条件可进一步推导：

p2 ⇒ p2': 线程1中对x的存储线程间先行发生于线程2中对x的加载
p1 + p2' ⇒ p7: 线程1中对y的存储线程间先行发生于线程2中对x的加载
p2 + p3 ⇒ p8: 线程1中对x的存储线程间先行发生于线程2断言中对y的加载
p1 + p8 ⇒ p9: 线程1中对y的存储线程间先行发生于线程2断言中对y的加载
p5 ⇒ p5': 线程2中对y的存储线程间先行发生于线程3中对y的加载
p4 + p5' ⇒ p10: 线程2断言中对y的加载线程间先行发生于线程3中对y的加载
p5 + p6 ⇒ p11: 线程2中对y的存储线程间先行发生于线程3中对x的加载
p4 + p11 ⇒ p12: 线程2断言中对y的加载线程间先行发生于线程3中对x的加载
p3 + p12 ⇒ p13: 线程2中对x的加载线程间先行发生于线程3中对x的加载
p2' + p13 ⇒ p14: 线程1中对x的存储线程间先行发生于线程3中对x的加载
p14 ⇒ 线程1中对x的存储先行发生于线程3中对x的加载

根据C++标准[intro.races]第18条的规定：

如果原子对象M上的副作用X先行发生于M的值计算B，那么B的求值必须从X或从M的修改顺序中X之后的副作用Y获取值。

在此场景中，x的修改顺序中不存在晚于线程1对x存储的操作，因此线程3对x的加载应读取线程1存储的值。据此分析，线程3的断言在触发时必然成立，未触发则无需考虑。

但GCC原子Wiki的总结指出：

释放/获取模式仅要求参与的两个线程同步。这意味着同步的值对其他线程不具备传递性。线程2的断言必然成立，因为线程1和线程2通过x.load()同步。线程3未参与此次同步，因此当线程2和线程3通过y.load()同步时，线程3的断言可能失败。线程1和线程3之间没有直接的同步关系，因此无法假设x的取值。

然而通过推导得出线程1对x的存储先行发生于线程3对x的加载，二者结论存在矛盾，特此请教该断言是否必然成立。

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