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
-----Original Message-----
From: owner-javamemorymodel@cs.umd.edu [mailto:owner-javamemorymodel@cs.umd.edu]On Behalf Of Sarita Adve
Sent: Tuesday, April 13, 2004 10:19 AM
To: 'Jerry Schwarz'; 'Jeremy Manson'; javamemorymodel@cs.umd.edu
Subject: RE: JavaMemoryModel: New Unified JMM Description
Jerry,
This is intentional. Can you explain why you think it is problematic, I am likely missing your concern?
I am in the process of writing up an "inuition for the model" document, but have had several digressions trying to determine the best way to motivate and justify it.
Sarita
-----Original Message-----
From: owner-javamemorymodel@cs.umd.edu [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of Jerry Schwarz
Sent: Monday, April 12, 2004 11:01 PM
To: Jeremy Manson; javamemorymodel@cs.umd.edu
Subject: Re: JavaMemoryModel: New Unified JMM Description
I finally had a chance to look at this in some detail and there is something that I think must be wrong.
Specifically the rules for committing actions include the following (apologies for ASCII notation)
1. Ci is a subset of Ai
6. For any read r in Ai - C(i-1) we have Wi(r) happens-before r
These imply that for any r in Ci - C(i-1) there will need to be a happens-before relationship between the read and the write that it sees.
This is obviously not intended so either (1) or (6) is misstated. My hypothises is that 6 is supposed to apply only to volatile reads, but I'm not terribly confident of that.
At 12:38 PM 4/5/2004, Jeremy Manson wrote:
Hi folks,
After much consultation from a lot of you, Bill, Sarita and I have put together a new description of the memory model. It is different from, but equivalent to, the last description. We feel that this one is cleaner, and probably easier to understand.
Victor Luchangco deserves particular credit for his input; his formalization of our model heavily influenced our new document.
As far as the semantics go, even after a great deal of scrutiny and email back-and-forth, no one was able to take Bill up on his $100 bounty, so we are fairly confident in the new model. There are a couple of tweaks to our treatment of one or two corner cases, but they do not make a substantive difference to the model.
Information about the new description is on the same web page:
http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/
Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
------------------------------- 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:01:03 EDT