关于C++原子操作中多组循环依赖条件是否可同时成立的技术求证

我最近在啃C++原子操作的内存模型时，碰到了几个绕人的例子，自己有一些直观的判断，但不确定怎么从标准的形式化规则（比如修改顺序、标准措辞）去严谨证明，也对其中涉及的“无中生有”值的规则有疑问，想和大家一起探讨：

第一个例子：单向依赖的条件互斥 #

先看第一个例子：

std::atomic<int> x = 1;
// 线程1
int expected = 1;
if (x.compare_exchange_strong(expected, 0, relaxed, relaxed) == true) { // #1
    x.store(2, relaxed);  // #2
}
// 线程2
int expected = 2;
if (x.compare_exchange_strong(expected, 3, relaxed, relaxed) == true) {  // #3
}

我能确定的是：不可能出现#3读到#2写入的值，但#1返回false的情况。我的直观证明很简单：#2只有在#1的条件为真（也就是#1返回true）时才会被执行，所以逻辑上不可能同时出现#1返回false、#3返回true的情况。

但我想知道，有没有更严谨的形式化证明方式？比如从C++标准中关于原子操作的修改顺序、内存可见性的正式措辞出发，去推导这个结论的必然性？

第二个例子：循环依赖与“无中生有”值的困惑 #

再看第二个例子，这里的逻辑就没那么直观了：

std::atomic<int> x = 2;
std::atomic<int> y = 0;
// 线程1
if (x.exchange(2, Relaxed) == 1) { // #1
  y.store(1, Relaxed); // #2
}
// 线程2
if (y.exchange(2, Acquire) == 1) { // #3
    x.store(1, Release); // #4
}

如果套用第一个例子的逻辑，会发现形成了循环：

• #1返回true，意味着它读到了#4写入的1；
• #4只有在#3返回true时才会执行；
• #3返回true，意味着它读到了#2写入的1；
• #2又只有在#1返回true时才会执行。

但从内存序的角度看，#4是Release操作，#1是Relaxed的exchange，两者之间没有同步关系；#2是Relaxed的store，#3是Acquire的exchange，也没有强制的同步约束。这时候我就懵了：这种循环依赖的情况，两个条件会不会同时成立？

我查了C++标准里的相关内容，里面提到：

实现应确保不会计算出循环依赖于自身计算的“无中生有”值。

但这里用的是should（应该）而不是shall（必须），属于非强制的推荐性规则。那是不是意味着，这个例子里存在#1和#3同时返回true的可能性？

第三个衍生例子：混合内存序的循环依赖 #

最后还有个衍生的例子，同样是循环依赖，但混用了Acquire/Release和Relaxed内存序：

std::atomic<int> v = {0};
// 线程1
if (v.load(acquire) == 1) { // #1
   v.store(2, release);  // #2
}
// 线程2
if (v.load(relaxed) == 2) { // #3
   v.store(1, relaxed);  // #4
}

这个例子里，会不会出现#1和#3都返回true的情况？

备注：内容来源于stack exchange，提问作者xmh0511