> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Wednesday, August 07, 2002 9:20 PM
> To: Sarita Adve; Jeremy Manson; javamemorymodel@cs.umd.edu;
> jsr-133-eg@jcp.org
> Subject: Re: JavaMemoryModel: SC for DRF programs with
> Bill/Jeremy's new approach?
>
>
> 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.
Ok, but now consider the case where Flag3 is not volatile. Also,
consider a slighthly transformed program where we "specialize" the code
for Thread 3 to separately reflect the cases when X==1 or K==1.
So, here's the original code again, but with Flag3 not volatile.
K, Flag1, Flag2 are volatile; initially all variables are 0
Thread 1
K = 1
Flag1 = 1
Thread 2
K = 2
Flag2 = 1
Thread 3
While ((Flag1 != 1) && (Flag2 != 1) {;}
If (K != 1) Flag3 = 1
If ((X == 1) || (K == 1)){
Y = 1
}
If (K == 1) Flag3 = 1
Thread 4
While ((Flag1 != 1) && (Flag2 != 1) {;}
While (Flag3 != 1) {;}
If (Y == 1) {
X = 1
}
Here's the "specialized" code for Thread 3 (all other threads run the
same as in the original).
Thread 3
While ((Flag1 != 1) && (Flag2 != 1) {;}
If (K != 1) Flag3 = 1
If ((X == 1)
Y = 1
If (K == 1) {
Y = 1
Flag3 = 1
}
I think your model will allow K = 2, X = 1, Y = 1 for the original code
(with non-volatile Flag3) but not for the specialized code. If so, I
don't think this is a good idea, since you are effectively prohibiting
the compiler from transforming the specialized code to the original.
This is also an issue with my model - it has to be handled by using the
right state information to control the register assignment in the
construction of P-R. In your model, I think this would need to be
handled by associating path information with GUIDs.
Sarita
P.S. Is there a reason to cc messages to the jsr-133-eg list? Isn't it a
subset of javamemorymodel?
-------------------------------
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