I have the same concern with Sarita regarding test 6.
One line of thought is this (another view of Sarita's concern):
If r1=A=1 and r2=B=1 is a legal outcome of the execution, then one
doesn't really care about the second if statement in t2 since it'll never
be carried out in this particular execution. So this second if statement
shouldn't affect the legality of the trace. As a result, it should be
treated in the same way as if the 2nd if statement doesn't exist.
- Jason
On Fri, 1 Aug 2003, Sarita Adve wrote:
> I haven't been able to discuss this with Bill/Jeremy yet.
>
> I was beginning to get sold on the property that Bill has used to argue
> against allowing test 5. However, it seems to me that allowing test 6
> violates that property:
>
> Initially A = B = 1
>
> Thread 1
> r1 = A
> if (r1 == 1)
> B = 1
>
> Thread 2
> r2=B
> if (r2 == 1)
> A = 1
> if (r2 == 0)
> A = 1
>
> Behavior in question: r1 == r2 == 1 allowed?
>
> To reason that r1 == r2 == 1 is allowed, we must look at the last if
> statement in thread 2, which may not have executed at this point. In fact,
> if we take away the last if statement, we have a case where we know we don't
> want the above behavior.
>
> Prohibiting test 6 is not a choice because it will prohibit fusing the two
> if statements. But I don't feel good about violating this property. I hope I
> am missing something about test 6.
>
> Sarita
>
>
> > -----Original Message-----
> > From: owner-javamemorymodel@cs.umd.edu
> > [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> > Sent: Friday, August 01, 2003 2:47 PM
> > To: javamemorymodel@cs.umd.edu
> > Subject: JavaMemoryModel: The choice we need to make on test
> > cases 5 and 10
> >
> >
> > The choice on test cases 5 and 10 seems to be one of the key issues
> > for the core memory model.
> >
> > http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
> >
> >
> > Test case 5:
> > Initially, x = y = z = 0
> >
> > Thread 1:
> > r1 = x
> > y = r1
> >
> > Thread 2
> > r2 = y
> > x = r2
> >
> > Thread 3
> > z = 1
> >
> > Thread 4
> > r3 = z
> > x = r3
> >
> > Behavior in question: r1 == r2 == 1, r3 == 0.
> >
> >
> > Let me lay out some pro and con.
> >
> > === Why we should allow the behavior in test case 5 ===
> >
> > A compiler or architecture might want to perform the
> > following transformation:
> >
> > * I predict that I will read 1 from x, so that r1 will be 1.
> >
> > * I want to speculatively assume that I do read 1 from x,
> > and speculative perform actions that depend upon that read.
> >
> > * If, when I read x, I find that I did not read 1, I promise
> > to unwind and restart all of the speculative actions that
> > depended upon r1=1. Note that these speculative actions are
> > scattered across multiple threads.
> >
> > OK, while this transformation sounds appealing, we can't apply it in
> > all cases. In particular, it allows test case 4.
> >
> > To fix this, we need to modify the transformation as follows.
> >
> > * In order to speculatively assume that I do read 1 from x,
> > I must show that there exists some non-prescient
> > execution in which I do read 1 from x.
> >
> > With this modification, the behavior in test case 4 is prohibited,
> > while the behavior in test cases 5 and 10 are allowed.
> >
> > === Why we should forbid the behavior in test case 5 ===
> >
> > I think there are lots of reasons, but here is one I feel
> > particularly compelling:
> >
> > * In order to understand how a particular execution happened,
> > it should
> > suffice to examine the code that did happen. You shouldn't have
> > to examine whether some code that you know didn't execute might
> > form a race with the code that did execute.
> >
> > * In particular, look at the code in test case 10. Is the following
> > behavior reasonable:
> >
> > Initially, x = y = z = 0
> >
> > Thread 1:
> > r1 = x (1)
> > if (r1 == 1)
> > y = 1
> >
> > Thread 2
> > r2 = y (1)
> > if (r2 == 1)
> > x = 1
> >
> > Thread 3
> > z = 1
> >
> > Thread 4
> > r3 = z (0)
> > if (r3 == 1)
> > ###### // we know it didn't execute, so we aren't going to
> > look at it
> >
> > Behavior in question: r1 == r2 == 1, r3 == 0
> >
> > In the code that (is visible) / (did execute), the
> > accesses to x and y are
> > correctly synchronized. So it becomes difficult to
> > understand how the system
> > introduced data races on x and y and got behavior similar
> > to that of
> > test case 4 which we thought we had ruled out.
> >
> > -------------------------------
> > JavaMemoryModel mailing list -
> > http://www.cs.umd.edu/~pugh/java/memoryModel
> >
>
>
> -------------------------------
> JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT