At 11:20 AM -0500 8/7/02, Sarita Adve wrote:
>Bill/Jeremy,
>
>Here's a data-race-free program that I think may not appear SC with your
>model, as written at the moment. Please let me know if I misunderstood
>something:
>
>
>Comments?
No, we do not allow K = 2, X = 1, Y = 1. See theorem 4.1, and the
below explanation.
>However, I don't see how your current model will prohibit the above
>result: Thread 4's read of Y legitimately returns the value 1 in the
>execution where K=1 wins. So I suppose it is allowed to return Y == 1 in
>the execution where K=2 wins as well?
The only execution order you are thinking of has thread 4 executing
if (Y = 1) {
X = 1;
}
before thread 3 executes
If ((X == 1) || (K == 1)){
Y = 1
}
In order for the read of Y by thread 4 to see the value 1, it would
have to be a prescient unsynchronized read. But a PUR must be
validated by an execution trace containing a data race in which the
read sees the value seen by the PUR.
In other words, unless there exists a PUR-free execution trace of P
that contains a data race, no PURs can be validated and no execution
traces of P containing PURs are valid.
Bill
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:41 EDT