Search code examples
concurrencymemory-modeljava-memory-model

JMM: show that happens-before relation is stronger that RA causality

New memory ordering where added in JDK9, so I'm digging into Release/Acquire mode. It introduce causality constraint:

If access A precedes interthread Release mode (or stronger) write W in source program order, then A precedes W in local precedence order for thread T
If interthread Acquire mode (or stronger) read R precedes access A in source program order, then R precedes A in local precedence order for Thread T.

As far as I see, the best way to show distinguish between R/A and Volatile modes is 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) |
|-----------|-----------|--------------|--------------|

If getM/setM is getAcquire/setRelease result (r1, r2, r3 ,r4) = (1, 0, 1, 0) is allowed;

If getM/setM is getVolatile/setVolatile result (r1, r2, r3 ,r4) = (1, 0, 1, 0) is forbidden;

My main target is to show that causality (from RA) != happens-before (in terms of JLS)

To show it I want to proof that for IRIW-volatile case result (1, 0, 1, 0) is forbidden using only happens-before (without using sequential consistency):

            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 |
|----------|----------|----------|----------|

Result of execution: (r1, r2, r3, r4) = (1, 0, 1, 0)

Happens-before orderings:

  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: We don't know it yet now, it's just some permutation of tuple (a, b, c, d, e, f), let's imagine it as array of 6 elements (SO array);

Synchronized-with is order defined for some SO-subsequent actions), so:
if A -sw→ B then A appears before B in SO array

SO is consistent with Program Order, so:
if A -po→ B then A appears before B is SO array

Happens-before is transitive closure of SW and PO, so:
if A -hb→ B then A appears before B is SO array

Due to happens-before orderings №1, №2 we have:
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

This means that last element in SO-array is f or d
If last element is f than we have a appears before f is SO, this means a -sw→ f, this causes a -hb→ f: inconsistency with happens-before ordering №3

(for case when last element is d the reasoning is similar)

This means that result (1, 0, 1, 0) is not possible here.

Is it proof correct?
Is it correct way to show that happens-before relation from JLS is not equivalent of causality RA constraint and you can't use term happens before for RA chains?

Solution

  • Yes, your proof is correct (at least as I can see).
    Yes, IRIW is clear and simple example that demostrates differences between Release/Acquire and Volatile modes.

    You can also use this in your proof: volatile read always returns the latest volatile write to that variable in synchronization order.
    Here is the quote from the JLS:

    17.4.7. Well-Formed Executions

    We only consider well-formed executions. An execution E = < P, A, po, so, W, V, sw, hb > is well formed if the following are true:

    ...

    1. The execution obeys synchronization-order consistency.

      For all volatile reads r in A, it is not the case that either so(r, W(r)) or that there exists a write w in A such that w.v = r.v and so(W(r), w) and so(w, r).

    The rest is similar to your proof:

    • so is a total order consistent with po => either d or f must be the last action in so
    • in either case there will be a volatile write of 1 to the same variable before the volatile read in so => the volatile read must return 1

    Also it's important to mention that even though the article you quoted is written by the author of JDK 9 Memory Order Modes, it's not official documentation.
    This means that at any moment the implementation of the Memory Order Modes might be changed from what's described in the article.
    The the only real guarantees are given in the official documentation, and AFAIK today it is just this javadoc.