Re: JavaMemoryModel: SC for DRF programs with Bill/Jeremy's new approach?

From: Bill Pugh (
Date: Wed Aug 07 2002 - 22:19:57 EDT

At 11:20 AM -0500 8/7/02, Sarita Adve wrote:
>Here's a data-race-free program that I think may not appear SC with your
>model, as written at the moment. Please let me know if I misunderstood

No, we do not allow K = 2, X = 1, Y = 1. See theorem 4.1, and the
below explanation.

>However, I don't see how your current model will prohibit the above
>result: Thread 4's read of Y legitimately returns the value 1 in the
>execution where K=1 wins. So I suppose it is allowed to return Y == 1 in
>the execution where K=2 wins as well?

The only execution order you are thinking of has thread 4 executing

if (Y = 1) {
        X = 1;

before thread 3 executes

If ((X == 1) || (K == 1)){
        Y = 1

In order for the read of Y by thread 4 to see the value 1, it would
have to be a prescient unsynchronized read. But a PUR must be
validated by an execution trace containing a data race in which the
read sees the value seen by the PUR.

In other words, unless there exists a PUR-free execution trace of P
that contains a data race, no PURs can be validated and no execution
traces of P containing PURs are valid.

JavaMemoryModel mailing list -

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