RE: JavaMemoryModel: Examples similar to tests 5 and 10

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Sat Jan 10 2004 - 08:25:56 EST


>
> So a value is out of thin air in M/P
> only if there
> exists a proof that a write of the value did not occur.

Note that the write of the value that is read (i.e., 1) does occur. It is
the write of 2 that occurs in one example and doesn't in another. But in
both examples, in the actual execution, nobody reads the value 2. So why
should it matter whether the write of 2 occurs or not.

> BTW, in the quoted code below, I've changed T4, which seemed
> to have been
> garbled in transmission (at least in the version I received). Perhaps
> Sarita could confirm that I've correctly stated it.

Yes, it is correctly stated.

Sarita

>
> Sylvia.
>
> >Example 1: Initially all variables are 0
> >
> >T1
> >r1=X
> >if (r1==1)
> > Z=1
> >
> >T2
> >r2=Z
> >if (r2==1 || r2==2)
> > X=1
> >
> >T3
> >Z=2
> >
> >Result: r1=r2=1
> >
> >
> >Example 2: Initially all variables are 0
> >
> >T1
> >r1=X
> >if (r1==1)
> > Z=1
> >
> >T2
> >r2=Z
> >if (r2==1 || r2==2)
> > X=1
> >
> >T3
> >Y = 1
> >
> >T4
> >r4 = Y
> >if (r4 == 1)
> > Z = 2
> >
> >Result: r1=r2=1, r4 = 0
>
> -------------------------------
> JavaMemoryModel mailing list -
> http://www.cs.umd.edu/~pugh/java/memoryModel
>

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



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