RE: JavaMemoryModel: Our latest trial balloon

From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Aug 22 2002 - 21:57:44 EDT


At 10:42 AM -0500 8/21/02, Sarita Adve wrote:
>Bill,
>
>I like the backward slices formalism, but don't quite see how this
>handles the cannonical out-of-thin-air values example (the one where two
>threads read/write x/y and return 42)? Is there a more developed version
>I should wait for, or am I missing something here?
>
>Sarita

Sorry, yes a more detailed version is coming. Jeremy and I are trying
to get all the proofs done before we distribute a more detailed
version; as usual, working through the proofs is forcing us to fine
tune things.

For the example you mention:

Initially, A = B = 0

Thread 1:
r1 = A
B = r1

Thread 2:
r2 = B
A = r2

Execution trace:

r1 = A (sees 42)
B = r1
r2 = B
A = r2

The read r1 = A (seeing 42) needs to be validated by a backwards
closed subtrace that guarantees the write of 42 to A will occur. And
no such subtrace exists.

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



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