[cpp-threads] Slightly revised memory model proposal (D2300)

[Boehm, Hans]

> -----Original Message-----
> From: Sarita V Adve [mailto:sadve at cs.uiuc.edu] 
> Sent: Tuesday, June 26, 2007 11:06 AM
> To: Boehm, Hans; C++ threads standardisation
> Subject: RE: [cpp-threads] Slightly revised memory model 
> proposal (D2300)
> 
> Hans,
> 
> It was good to see you at FCRC.
> 
> (1) There are a few comments from the previous round that are 
> still not addressed here. For example, the definition of 
> "consistent" does not seem sufficient to guarantee SC for 
> some reasonable (non-controversial?) classes of programs. I 
> assume you want
> T1: if (A==1) B=1;
> T2: if (B==1) A=1
> to be considered as data-race-free and so appear SC 
> (initially A, B are 0 and neither is atomic). However, I 
> don't see anything in the consistency definition that will 
> preclude both T1 and T2 reading 1 and writing 1. This has 
> nothing to do with any definition of happens-before since SC 
> executions of this program do not have any conflicting accesses. 
I see the problem.  We attempted to address this in ancient versions of
the model but somehow this got lost.  Thanks for catching it (again).

We are sort of addressing the corresponding issue for relaxed atomics,
after Jeremy pointed it out.  But this form is clearly even more
important.

I will either post a revision or give you a call after thinking about it
a bit.

> 
> There are other issues, but may be moot in case I am 
> misunderstanding your intent for the above. Perhaps it will 
> be easier to talk on the phone since this has come up a few times?
> 
> (2) Has someone verified from IBM architects that Peter 
> Dimov's fetch_add example actually works with PPC? Otherwise, 
> that's a lot of complexity in the new synchronizes-with 
> definition for no return. Sorry to not have got back to you 
> and others on this aspect earlier, but I am not sure the 
> current modification is the best one for this (need IBM's 
> answer before further discussion on this).
Good question.  There are some other cases currently under discussion
where I also don't fully understand the hardware constraints.  It's
unclear whether this should apply to "relaxed" RMW operations.  My
feeling is that we should provide whatever guarantees we can without
making this much more complicated still, or making it effectively
unimplementable on common hardware.

Hans

> 
> Sarita
> 
> 
> > -----Original Message-----
> > From: Boehm, Hans [mailto:hans.boehm at hp.com]
> > Sent: Thursday, June 21, 2007 9:23 PM
> > To: C++ threads standardisation
> > Cc: Sarita V Adve
> > Subject: RE: [cpp-threads] Slightly revised memory model proposal 
> > (D2300)
> > 
> > Here are the latest revisions of:
> > 
> > The D2300 memory model.  I sort of followed Lawrence's 
> semi-suggestion 
> > and included sc stores (not loads) with RMW operations in defining 
> > synchronizes with.  I also cleaned up the discussion of race-free 
> > executions in a way that I think is necessary, but may 
> require Clark 
> > to clean up after my standardese again.
> > 
> > Some text (mm_rules) to be included in the atomics proposal 
> to explain 
> > how it meshes with the memory model.
> > 
> > The sequential consistency proof updated to reflect the 
> memory model 
> > revisions, and hopefully fixing some other issues.
> > 
> > Further bug reports would be appreciated.  The C++ paper 
> deadline is 
> > officially tomorrow.
> > 
> > Hans
> > 
>