Let me explain in detail why case 4 is not allowed when combining the read
value rules for locals.
> t1 t2
> R(x,r1,1) R(y,r2,1)
> W(y,r1) W(x,r2)
Let's apply read value rule to R(x,r1,1), it says there exists a latest
previous write on x with value 1. Keep in mind that we are currently
validating R(x,r1,1), so r1=x=1 is not committed at this point. That is,
the available assignment of r1 is still r1=0 (init value).
Now, the only candidate write on x with value 1 is W(x,r2). Since this
write uses r2, a write of r2 is needed, which must be R(y,r2,1) due to
read value rules of locals.
Is R(y,r2,1) legal? W(y,r1) is the only eligible candidate if r1
can be 1. This is a use of r1, so what are the available values of r1 at
this point? The only thing available is the init value 0.
Therefore, the trace is not allowed.
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:48 EDT