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