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

[Paul E. McKenney]

On Tue, Jun 26, 2007 at 07:32:38PM -0000, Boehm, Hans wrote:
>  
> 
> > -----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.

I have to ask...  If A and B are non-atomic ("neither is atomic"),
are we really making any guarantees whatsoever?

> > 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.

Peter Dimov's example should work with PPC (due to B-cumulativity, FWIW)
-- in other words, on PPC the assertion should never fail.  Including the
example for reference, just to make sure we are talking about the same
example:  ;-)

T1: x=1; fetch_add_release(&v,1);
T2: y=1; fetch_add_release(&v,1);
T3: if (load_acquire(&v)==2) assert (x+y==2);

Note that x & y need not be atomic, as there are no data races.

We can get a formal analysis from the PPC architects, if that would
be useful.

						Thanx, Paul

> 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
> > > 
> > 
> 
> --
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk
> http://www.decadentplace.org.uk/cgi-bin/mailman/listinfo/cpp-threads