**Next message:**Bill Pugh: "JavaMemoryModel: Possible weakening of Manson/Pugh model"**Previous message:**Bill Pugh: "JavaMemoryModel: Results of discussions with Sarita"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

Causality test case 7:

Initially, x = y = z = 0

Thread 1:

r1 = z

r2 = x

y = r2

Thread 2:

r3 = y

z = r3

x = 1

Behavior in question: r1 = r2 = r3 = 1.

We must allow this behavior, because simple reordering of independent

statements could move the read of z last in thread 1, and the write

to x first in thread 2.

After those movements, SC execution could give us r1 = r2 = r3 = 1.

This execution is not allowed in SC-3.

Say it is allowed. We need to start with either r1 = z (1) or r3 = y

(1) in SC order.

Say we start with r1 = z (1). In order to show that this

discontinuity is legal in SC-3, we need to show that in all SC

extensions of this execution, 1 will be written to z. However, since

we cannot guarantee the ordering of the writes and reads to either x

or y, we cannot make this guarantee. For example, it does not occur in

r1 = z (1)

r3 = y (0)

r2 = x (0)

z = r3

x = 1

y = r2

Alternatively, we could start with r3 = y (1). We need to show that

in all SC extensions of this execution, 1 will be written to y.

Unfortunately, it doesn't occur in this SC extension:

r3 = y (1)

r1 = z (0)

r2 = x (0)

y = r2

z = r3

x = 1

So this behavior is not allowed by SC-3.

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

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

**Next message:**Bill Pugh: "JavaMemoryModel: Possible weakening of Manson/Pugh model"**Previous message:**Bill Pugh: "JavaMemoryModel: Results of discussions with Sarita"**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
*