void writer(Tuple tuple) {
tuple.nonVolatileF = 5;
tuple.volatileF = 1;
}
void reader(Tuple tuple) {
int regNV = 0;
int cache = tuple.nonVolatileF;
int regV = tuple.volatileF;
if (regV == 1) { regNV = cache; }
// computation that uses both of the above
}
because `cache` might get assigned before `tuple.nonVolatileF` is set. (The same is true of regV, but I guess the untransformed program had that, so you don't bother). But you said that the JMM guarantees that all reads in C_i - C_(i-1) will see writes in C_(i-1); this means that C_3 which reads `tuple.nonVolatileF` will see the write to that variable in C_2, no? Since you're constructing an execution, why didn't you interleave the execution to make this trivially true? Also, can't you wrap the writer in an atomic block during transformation?
> But you said that the JMM guarantees that all reads in C_i - C_(i-1)
> will see writes in C_(i-1); this means that C_3 which reads
> `tuple.nonVolatileF` will see the write to that variable in C_2, no?
Talking about such things in English is ambiguous. The formal
statement is
"For any read r ∈ C_i −C_(i−1), we have W_i(r) ∈ C_(i−1) and W(r) ∈
C_(i−1)".
A clearer way to state the clause in English is "writes seen by reads
in C_i - C_(i-1) belong to C_(i-1);". I can justify an execution as
long as reads (ultimately) seen any write in the commit previous to
the one it is in, subject to happens before consistency. To prevent
causality loops, the JMM allows a read to see a write that happened
before it in the commit that introduces it. Then, to allow certain
interesting optimizations, the JMM allows us the bait-and-switch the
write a read saw -- "Each read r in C_i − C_(i−1) must see writes in
C_(i−1) in both E_i and E, but may see a different write in E_i from
the one it sees in E.".
The non-volatile read is _allowed_ to see the non-volatile write
(i.e. such an execution exists, this is the question I ask in the
exercise), but it doesn't have to. The transform in question is
illegal because the transformed program allows behavior that the
untransformed program didn't allow -- the transform breaks semantics.
> Since you're constructing an execution, why didn't you interleave
> the execution to make this trivially true?
I don't understand this, make /what/ trivially true? In any case, the
transformed program has a data race, and so observationally it doesn't
need to have a sequentially consistent execution. Specifically, it is
allowed to show behavior that cannot be described by any
interleaving of the instructions streams of the individual threads.
> Also, can't you wrap the writer in an atomic block during
> transformation?
> The non-volatile read is _allowed_ to see the non-volatile write (i.e. such an execution exists, this is the question I ask in the exercise), but it doesn't have to.
And this is why debugging this kind of issue in practice is fun: You have very little or non-obvious guarantees here.
If you think about constructing adversary proofs or decided that your program is a little gnome bound to make you insane, this can be rephrased as: In this example, the nonvolatile read can choose any value of any write as long as it is in a happened before relationship to the nv-read. It might pick every value, every second value, or just that one troublesome valu and never change again.
Thanks for posting this, this looks really interesting.
one note:
>This blog post tries to show how some re-orderings (that may be done in as part of optimizing a Java program for performance) that intuitively seem illegal are, in fact, illegal, by deriving that illegality from directly the JMM spec.
This is a wrong transformation:
because `cache` might get assigned before `tuple.nonVolatileF` is set. (The same is true of regV, but I guess the untransformed program had that, so you don't bother). But you said that the JMM guarantees that all reads in C_i - C_(i-1) will see writes in C_(i-1); this means that C_3 which reads `tuple.nonVolatileF` will see the write to that variable in C_2, no? Since you're constructing an execution, why didn't you interleave the execution to make this trivially true? Also, can't you wrap the writer in an atomic block during transformation?