Value load rule of same address

java

Consider the case that two threads write to the same memory address, what will be the result if reading the variable twice consecutively?

concurrent write

4 outcomes if enumerate all combinations: (x → y means x precedences y in memory order)

  1. x1 =2, x2 =2. Easy to reason about. b1 → a1 → a2 → a3.
  2. x1 = 3, x2 = 3. Easy to reason about. a1 → b1 → a2 → a3.
  3. x1 = 2, x2 =3. Interleaving execution. a1 → a2 → b1 → a3.
  4. x1 = 3, x2 = 2. Reorder a1 and a2. b1 → a2 → a1 → a3. Is this allowed since StoreLoad order is not enforced in weak memory models like TSO ? It looks like the second load reads an old value, whereas previous load has already got a new value which is impossible if in single thread case.

case #4 is not possible. Although it’s weak memory model, reading same memory address is enforced by the rule that value loads the latest store value before it in memory order or program order. But program order takes precedence.

case #4

Explain:

  1. a1 executes but write to write buffer.
  2. b1 writes memory.
  3. a2 executes but read the value of write buffer, so x1 = 2.
  4. a1 flushes to memory.
  5. a3 executes but read the memory value, so x2 = 2.

Due to writer buffer, a2 will not read the memory but bypass the value from the buffer. So there won’t be the case that a2 reads 2 even b1 executes in advance.

Let’s verify this in java with jcstress. jcstress is a lib provided by openjdk to verify the behavior of multithread program

import org.openjdk.jcstress.annotations.Actor;
import org.openjdk.jcstress.annotations.JCStressTest;
import org.openjdk.jcstress.annotations.Outcome;
import org.openjdk.jcstress.annotations.State;
import org.openjdk.jcstress.infra.results.II_Result;

import static org.openjdk.jcstress.annotations.Expect.*;

@JCStressTest
@Outcome(id = {"2, 2"}, expect = ACCEPTABLE, desc = "2, 2")
@Outcome(id = {"3, 3"}, expect = ACCEPTABLE, desc = "3, 3")
@Outcome(id = {"2, 3"}, expect = ACCEPTABLE_INTERESTING, desc = "buffer -> memory")
@Outcome(id = {"3, 2"}, expect = FORBIDDEN, desc = "memory-> buffer")
@State
public class WriteTest {
  int x = 0;
  int x1 = 0, x2 = 0;

  @Actor
  public void actor1(II_Result r) {
    x = 2;
    x1 = x;
    x2 = x;
    r.r1 = x1;
    r.r2 = x2;
  }

  @Actor
  public void actor2() {
    x = 3;
  }
}

The output:

one iteration

test report

3, 2 never occurs in all forks of all iterations.

Support me