RE: JavaMemoryModel: The choice we need to make on test cases 5 a nd 10

From: Boehm, Hans (hans_boehm@hp.com)
Date: Fri Aug 01 2003 - 19:44:27 EDT


I agree with Bill's and Jeremy's choices for all the test cases other
than 5 and 10. (I even agree if A and B are initially zero in test
case 6, as I assume they were supposed to be. )

I don't really care very much about 5 and 10.

On one side, intuitively they should be disallowed for the reasons
given in the web page, and because it's harder to reason about some programs
if they are allowed. But I have a hard time coming up with a real program
for which it matters.

On the other side, there's some argument that a compiler should, aside
from introducing extra reads and writes, be allowed to make favorable
scheduling assumptions when compiling synchronization-free code, i.e.
effectively assume that there are no races. This is a bit of a generalization
of the rules about compiling synchronization free code in a single thread.

If you buy that, the compiler, while compiling x = r3, could reason that since
there is no synchronization, it's safe to assume that thread 3 gets scheduled first,
and z will be one. Thus r3 can be assumed to be one, and hence x = r3 can be
optimized to x = 1. There is no rule against stupidly failing to optimize r3 = z
in the same way. (Or perhaps it ends up getting scheduled in some other context
in which z is cheaper to load then the constant one.) Thus we could conceivably
justify transforming thread 4 to:

x = 1;
r3 = z;

which clearly makes the result possible.

As far as I'm concerned, the arguments in both directions are rather weak. I'd
be happy to decide based on simplicity of the model.

Hans

> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Friday, August 01, 2003 12: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



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT