release+acquire同步操作是否会破坏happens-before严格偏序关系？

如今很多编程语言都定义了happens-before关系与release+acquire同步操作。

包含这类特性的编程语言包括：

• C/C++11：支持happens-before、release+acquire
• Rust和Swift完全沿用了C/C++内存模型，因此也支持上述特性
• Java：支持happens-before、release+acquire

我想了解release+acquire是否可能违反happens-before：

• 如果存在违反的可能，希望给出对应的示例；
• 如果不可能违反，希望给出简单清晰的原理说明。

什么是release+acquire与happens-before #

Release/acquire会在不同线程之间建立happens-before关系：也就是说，线程1中release操作之前的所有写入，都保证对线程2中acquire操作之后的代码可见：

\     线程1                        /            
  \    --------                       /             
   \   x = 1                         / 此处所有操作  
    \  y = 2                        /  对线程2可见...    
     \ write-release(ready = true) /                
      └───────────────────────────┘                 
                   |                                
                   └─────────────┐ (happens-before) 
                                 V                  
                    ┌─────────────────────────┐     
                   / 线程2                      \    
 ...对以下所有操作可见 /  --------                   \   
               /   read-acquire(ready == true) \  
              /    assert(x == 1)               \ 
             /     assert(y == 2)                \

此外，happens-before是一种严格偏序关系，具备以下特性：

• 传递性：线程2不仅能看到线程1的写入，还能看到线程1可见的所有其他线程的写入；
• 非对称性：要么a happens-before b，要么b happens-before a，二者不可能同时成立。

我认为release/acquire可能破坏happens-before的原因 #

根据IRIW litmus测试的结果，release/acquire可能导致两个线程观察到不同线程的写入顺序不一致：

// 线程1
x.store(1, memory_order_release);
// 线程2
y.store(1, memory_order_release);
// 线程3
assert(x.load(memory_order_acquire) == 1 && y.load(memory_order_acquire) == 0);
// 线程4
assert(y.load(memory_order_acquire) == 1 && x.load(memory_order_acquire) == 0);

上述代码中两个assert都可能通过，意味着线程3和线程4观察到的x、y写入顺序不同。

我原本认为如果是普通变量，这种情况会违反happens-before的非对称性，但因为x和y是原子变量所以是合规的（不过我对此并不确定）
已有相关证明指出这个IRIW示例是合规的。

但我仍然怀疑存在类似IRIW的场景，会导致线程3和线程4观察到普通写入的happens-before顺序不一致，这会破坏happens-before的传递性。

注释1 #

相关技术文档中还有如下表述：

实现需要保证happens-before关系是无环的，必要时需要引入额外的同步（仅当涉及consume操作时才需要，参考Batty等人的研究）

这段描述暗示可能存在happens-before被违反、需要额外同步的场景（“无环”意味着happens-before构成有向无环图，等价于严格偏序关系）。
如果这类场景存在，我希望了解具体的情况。

注释2 #

由于Java允许数据竞争，我也对仅在存在数据竞争时才会发生happens-before违反的场景感兴趣。

编辑1（2021年11月3日） #

举个例子，这里先说明为什么顺序一致性（SC）原子操作不会违反happens-before（如果能给出release/acquire原子操作的同类解释，就可以解答我的问题）。

我所说的“违反happens-before”指的是违反happens-before作为严格偏序关系的公理。
严格偏序关系和*有向无环图（DAG）*是一一对应的。

DAG示例如下（图中不存在环）：

我们可以证明使用SC原子操作时，happens-before图始终是无环的：
SC原子操作的执行存在全局顺序（所有线程观察到的顺序一致），并且满足：

• 该全局顺序和每个线程内部的操作顺序一致；
• 每个SC原子读操作都会读到全局顺序中对应变量的最新SC原子写入。

看如下happens-before图：

线程1    线程2    线程3 
 =======  =======  ======= 
    │        │        │    
   W(x)      │        │    
    ↓        │        │    
   Sw(a) ┐   │       W(y)  
    │    │   │        ↓    
    │    └> Sr(a)  ┌ Sw(b) 
    │        ↓     │  │    
    │       Sr(b)<─┘  │    
    │        ↓        │    
    │       R(x)      │    
    │        ↓        │    
    │       R(y)      │    
    │        │        │    
    V        V        V    

图中规则说明：

• 时间向下流动；
• W(x)和R(x)是普通操作：对x的写入和读取；
• Sw(a)和Sr(a)是SC原子操作：对a的原子写入和读取；
• 每个线程内部的操作遵循程序顺序（C++中也叫sequenced-before顺序）：和代码中的执行顺序一致；
• 线程间的happens-before关系由SC原子操作建立。

可以看到图中的所有箭头始终向下
=> 图中不可能出现环
=> 始终是DAG
=> 不会违反happens-before的公理

同样的证明方法不适用于release/acquire原子操作，因为据我所知release/acquire原子操作不存在全局执行顺序，因此Sw(a)到Sr(a)的HB箭头可能向上，就有可能形成环（我对此并不确定）。

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