Re: JavaMemoryModel: Interaction between the memory model and exc eptions, Tread.stop()

From: Vijay Saraswat (vijay@saraswat.org)
Date: Fri Apr 09 2004 - 08:11:46 EDT


Boehm, Hans wrote:

>As far as I can tell, requiring the precise exception model for Thread.stop()
>

I am not worried about Thread.stop(). Lets ignore it -- its deprecated
after all.

Let me make the high-level argument of my previous message concrete. I
hope this helps to better communicate my worry.

Consider Test Case 6Ex, a variant of test case 6.
----------------------------------------------------
Causality test case 6Ex

Initially, x = y = 0, z = null

Thread 1
r1 = x
if r1 == 1
  y = 1

Thread 2
r2 = y
if (r2 == 1)
  x=1
z = comp()
r4 = z.a
if (r2 == 0)
  x=1

Behavior in question: r1 == r2 == 1

----------------------------------------------

Here, comp() is some terminating computation and the compiler cant
establish after the assignment to z that z is not null.

Should the behavior be allowed?

We are looking to set up requirements here. So I am looking for an
argument that is not based on one model or another but sets up
requirements for the models to satisfy.

A more complicated test would be one in which x is passed into comp, and
an exception is conditionally thrown. Lets just work it out with inline
conditionals first:
----------------------------------------------------
Causality test case 6Ex1

Initially, x = y = 0, z = null

Thread 1
r1 = x
if r1 == 1
  y = 1

Thread 2
r2 = y
if (r2 == 1) {
  x = 1
  z = new Z()
}
r4 = z.a
if (r2 == 0)
  x=1

Behavior in question: r1 == r2 == 1

----------------------------------------------

Note that when we say "behavior in question" we mean "on termination",
and this includes normal and abrupt termination.

So how do we argue this case?

Now lets throw in some exception handlers:
----------------------------------------------------
Causality test case 6Ex1.1

Initially, x = y = 0, z = null

Thread 1
r1 = x
if r1 == 1
  y = 1

Thread 2
r2 = y
try {
 if (r2 == 1) {
   x = 1;
    z = new Z();
}
 r4 = z.a
} catch (Exception z) {
}
if (r2 == 0)
  x = 1

Behavior in question: r1 == r2 == 1

----------------------------------------------

Now lets put the out of order write in the exception handler:

---------------------------------------------------
Causality test case 6Ex1.2

Initially, x = y = 0, z = null

Thread 1
r1 = x
if r1 == 0
  y = 1

Thread 2
r2 = y
try {
 if (r2 == 1) {
    x = 1
   z = new Z()
}
 r4 = z.a
} catch (Exception z) {
   if (r2 == 0)
     x = 1
}

Behavior in question: r1 == r2 == 1

----------------------------------------------

And lets go back and modify 6Ex1 to get 6Ex2, 6Ex2.1, 6Ex2.2 etc:

---------------------------------------------------
Causality test case 6Ex2

Initially, x = y = 0, z = null

Thread 1
r1 = x
if r1 == 1
  y = 1

Thread 2
r2 = y
if (r2 == 1)
  x = 1
if (r2 != 1)
  z = new Z();
r4 = z.a
if (r2 == 0)
  x = 1

Behavior in question: r1 == r2 == 1

----------------------------------------------

As I said before: just put some potentially exception raising
instructions in the middle of the cross loop in which a read observes a
non hb-ordered write. (And try/catches as well...)

What principle should be used to answer such cases?

I am afraid one does need to reason about the interaction of exceptions
with the memory model.

Best,
Vijay

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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