As I understand case 6, both A and B are initially 1 and can only take on
the value 1, therefore both r1 and r2 can be assumed to be 1.
----- Original Message -----
From: "Sarita Adve" <sadve@cs.uiuc.edu>
To: <javamemorymodel@cs.umd.edu>
Sent: Friday, August 01, 2003 3:29 PM
Subject: RE: JavaMemoryModel: The choice we need to make on test cases 5 and
10
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:49 EDT