Re: JavaMemoryModel: The choice we need to make on test cases 5 and 10

From: Joseph Bowbeer (jozart@csi.com)
Date: Fri Aug 01 2003 - 18:41:38 EDT


I would vote to disallow 5 and 10.

In both cases it looks like the compiler has jumped to a conclusion that
should not have been reached.

Concerning case 1, this is the kind of analysis that I would expect to be
associated with some switch (like -o) or some high-end product (like DashO),
but that I may not want applied to every app that I run in a JVM.

----- Original Message -----
From: "Bill Pugh" <pugh@cs.umd.edu>
To: <javamemorymodel@cs.umd.edu>
Sent: Friday, August 01, 2003 12:46 PM
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



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