RE: JavaMemoryModel: Our latest trial balloon

From: Bill Pugh (
Date: Thu Aug 22 2002 - 21:57:44 EDT

At 10:42 AM -0500 8/21/02, Sarita Adve wrote:
>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?

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.

JavaMemoryModel mailing list -

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