jmm05.md

I think JMM-05 (https://github.com/jeehoonkang/memory-model-explorer/blob/master/test/jmm-05.test) should be allowed, as contrary to the decision JMM people (and we) made. Here is a series of "standard" optimizations that lead JMM-05 into a program that can clearly output the designated outcome.

Series of Optimizations

By some global analysis, deduce that r2 should be 0 or 1. Thus transform thread 2 into:
```
r2 = y;
if (r2) {
  x = 1
} else {
  x = 0
}
```

Sequentialize thread 2 and (3 || 4). Then threads 2, 3, 4 is merged into:

r2 = y;
if (r2) {
  x = 1
} else {
  x = 0
};
((z = 1) || (r3 = z; x = r3))

Put (z = 1) || (r3 = z; x = r3) into two branches.

r2 = y;
if (r2) {
  x = 1;
  ((z = 1) || (r3 = z; x = r3))
} else {
  x = 0;
  ((z = 1) || (r3 = z; x = r3))
}

Sequentialize (z = 1) || (r3 = z; x = r3) (differently for each branch):

r2 = y;
if (r2) {
  x = 1;
  r3 = z; x = r3; z = 1
} else {
  x = 0;
  z = 1; r3 = z; x = r3
}

Deduce that r3 in the else branch is 1, and replace x = r3 with x = 1:

r2 = y;
if (r2) {
  x = 1;
  r3 = z; x = r3; z = 1
} else {
  x = 0;
  z = 1; r3 = z; x = 1
}

Reorder x = 1 in the else branch and merge it with x = 0:

r2 = y;
if (r2) {
  x = 1;
  r3 = z; x = r3; z = 1
} else {
  x = 1;
  z = 1; r3 = z
}

Put x = 1 out of the if/else, and reorder it with r2 = y:

x = 1;
r2 = y;
if (r2) {
  r3 = z; x = r3; z = 1
} else {
  z = 1; r3 = z
}

Then a sequential execution can result in r1 = r2 = 1, r3 = 0.

Context

The current rule for the forward edge (src and tgt should be in the same thread) is clearly wrong: it does not support, for e.g., sequentialization. So I tried to find an alternative rule for the forward edge, but I failed to make one for 3+ days. Finally I found a rule, but it does not predict JMM-05 correctly. I translated a sketch-of-proof for the sequentialization of the rule into the JMM-05 example, and got the above series of optimizations.

If we agree to allow JMM-05, then it would be much easier to make a rule for forward edges: no constraint at all (except for coherence rules for rf)! Before jumping into that conclusion, I would like to ask your opinion for the above reasoning.

jeehoonkang/jmm05.md

Series of Optimizations

Context