**Next message:**Bill Pugh: "JavaMemoryModel: Results of discussions with Sarita"**Previous message:**Jan-Willem Maessen: "Re: JavaMemoryModel: Are the volatile semantics strong enough?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

Causality 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.

We start by executing

r2 = y (1)

This is a data race, so we need to show that r2 = y (1) is an

allowable discontinuity. Considering the following Esc:

r2 = y (1)

z = 1

r3 = z (1)

x = r3

r1 = x (1)

y = r1 // This is W; it writes 1 to y

x = r2

So this discontinuity is allowed, so long as W occurs in the

execution we are generating.

Here is the rest of the execution I wish to generate. Each data race read in

the remainder of the execution sees a previous write, so no

additional reasoning is required.

r2 = y (1)

x = r2

r1 = x (1)

y = r1 // This is W; it writes 1 to y

r3 = z (0)

x = r3

z = 1

Since W occurs in the executed we generated, our proof obligation is

satisfied, and the execution is allowed.

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

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

**Next message:**Bill Pugh: "JavaMemoryModel: Results of discussions with Sarita"**Previous message:**Jan-Willem Maessen: "Re: JavaMemoryModel: Are the volatile semantics strong enough?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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