JMM中Happens-before与RA因果性差异及证明正确性问询

JDK9新增了新的内存排序机制，我正在研究其中的Release/Acquire（RA）模式，该模式引入了causality（因果性）约束：

若线程T的源代码顺序中，访问A先于线程间Release模式（或更强模式）写操作W，则在T的本地优先顺序中A先于W；
若线程T的源代码顺序中，线程间Acquire模式（或更强模式）读操作R先于访问A，则在T的本地优先顺序中R先于A。

我认为区分RA与Volatile模式的最佳方式是IRIW测试：

int x = 0
                  int y = 0
|-----------|-----------|--------------|--------------|
| Thread 1  | Thread 2  |   Thread 3   |   Thread 4   |
|-----------|-----------|--------------|--------------|          
| setM(x,1) | setM(y,1) | r1 = getM(x) | r3 = getM(y) |
|           |           | r2 = getM(y) | r4 = getM(x) |
|-----------|-----------|--------------|--------------|

若getM/setM为getAcquire/setRelease，则结果(r1, r2, r3 ,r4) = (1, 0, 1, 0)是允许的；若getM/setM为getVolatile/setVolatile，则该结果是被禁止的。

我的核心目标是证明RA的causality（因果性）≠ JLS定义的happens-before。

为此，我尝试仅用happens-before（不使用顺序一致性）证明Volatile的IRIW案例中结果(1, 0, 1, 0)是被禁止的：

volatile int x = 0;
            volatile int y = 0;
|----------|----------|----------|----------|
| Thread 1 | Thread 2 | Thread 3 | Thread 4 |
|----------|----------|----------|----------|
|a: x = 1  |b:  y = 1 |c: r1 = x |e: r3 = y |
|          |          |d: r2 = y |f: r4 = x |
|----------|----------|----------|----------|

执行结果：(r1, r2, r3, r4) = (1, 0, 1, 0)

Happens-before顺序 #

1. T1.W(x,1) -hb→ T3.R(x):1 -hb→ T3.R(y):0
2. T2.W(y,1) -hb→ T4.R(y):1 -hb→ T4.R(x):0
3. T1.W(x,1) -not hb→ T4.R(x):0
4. T2.W(y,1) -not hb→ T3.R(y):0

同步顺序（Synchronization Order） #

同步顺序是元组(a, b, c, d, e, f)的某种排列，可视为包含6个元素的数组（SO array）。

同步伴随（Synchronized-with） #

同步伴随为某些同步顺序后续操作定义了顺序：
if A -sw→ B then A appears before B in SO array

程序顺序（Program Order） #

同步顺序与程序顺序一致：
if A -po→ B then A appears before B is SO array

Happens-before的定义 #

Happens-before是同步伴随与程序顺序的传递闭包：
if A -hb→ B then A appears before B is SO array

根据Happens-before顺序1、2，可得：

• a appears before c is SO array
• c appears before d is SO array
• b appears before e is SO array
• e appears before f is SO array

这意味着SO数组的最后一个元素是f或d：

• 若最后一个元素是f，则SO数组中a在f之前，即a -sw→ f，进而导致a -hb→ f，这与Happens-before顺序3矛盾；
• 若最后一个元素是d，同理可推出b -hb→ d，与Happens-before顺序4矛盾。

由此可知该结果(1, 0, 1, 0)不可能出现。

问题 #

1. 上述证明是否正确？
2. 用此方式证明JLS的happens-before关系与RA的因果性约束不等价、且不能将happens-before用于RA链是否正确？

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