jmm05.md

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.