RE: JavaMemoryModel: New Unified JMM Description

From: Boehm, Hans (hans.boehm@hp.com)
Date: Tue Apr 13 2004 - 16:50:45 EDT


Bill -

That's right. My only real issue here is that this part of the
specification is very subtle, and that subtlety
is currently too easy to miss. I was initially confused by it, and
I suspect Jerry may also have misread it.

And that is compounded a bit by the otherwise minor mistake on the
bottom of page 24, which Jeremy already acknowledged.

Hans

> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Tuesday, April 13, 2004 1:41 PM
> To: Boehm, Hans
> Cc: javamemorymodel@cs.umd.edu; 'Jerry Schwarz'; 'sadve@cs.uiuc.edu';
> 'Jeremy Manson'
> Subject: Re: JavaMemoryModel: New Unified JMM Description
>
>
>
> On Apr 13, 2004, at 2:39 PM, Boehm, Hans wrote:
>
> > I think I may have been (or maybe still am) confused on a similar
> > point, so maybe this helps.
> >
> > The problem with section 7.6 seems to be that it's not immediately
> > apparent that you can justify
> > a sequentially consistent execution.
> >
> > If we have
> >
> > Thread 1
> > x = 1;
> > r1 = x;
> >
> > Thread 2
> > x = 2;
> > r2 = x;
> >
> > Let's say I want to justify r1 = r2 = 2.
> >
> > Clearly I can put x = 1 and x = 2 in C1.
> >
> > I can clearly add r2 = x with W2(r2=x) = (x=2) in C2, since
> > the write x = 2 happens-before the read into r2.
> >
> > But I think I can only add r1 = x to C3 with W3(r1=x) = (x=1) .
> > This is very counterintuitive, but OK, since I can still have
> > W(r1=x) = (x=2).
> >
> > If I'm interpreting this correctly, there at least needs to be
> > a footnote explaining the significance of the "i-1" in rule 5.
> >
> > Hans
> >
> >
>
> You do seem to be interpreting it correctly.
>
> The point is that you first have to justify a read r occurring
> in an execution E_i in which it sees a write that happens before it.
>
> But then, in both E and E_j, j > i, r is allowed to see a different
> write.
>
> As you describe above.
>
> So it seems that you did deduce that you could justify a sequentially
> consistent
> execution, but you found the way it works counterintuitive. Is that
> correct?
> We'll try to explain it better.
>
> By the way, you could have committed both reads in E2, since
> in both E2
> and E
> they see writes that were committed in E1.
>
> Bill
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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