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

[Paul E. McKenney]

On Thu, Jun 28, 2007 at 01:37:28AM -0500, Sarita V Adve wrote:
> > -----Original Message-----
> > From: Paul E. McKenney [mailto:paulmck at linux.vnet.ibm.com] 
> > Sent: Wednesday, June 27, 2007 12:56 PM
> > To: C++ threads standardisation
> > Cc: Sarita V Adve
> > Subject: Re: [cpp-threads] Slightly revised memory model 
> > proposal (D2300)
> > 
> > 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?
> 
> Yes, we do want to make guarantees here. We don't want the reads of A or
> B to return 1. The program does not have data races (or relaxed atomics)
> in any SC execution. I think it would be hard to reason about a model
> that does not make this guarantee.

But if A and B are non-atomic, we aren't even guaranteeing that
simple loads and stores will be indivisible operations.  Why would
we be making SC guarantees about variables that don't provide even
the very weak guarantees provided by relaxed atomics?  Shouldn't the
developer be using atomic variables in multithreaded situations
exactly so that the program wil be easy to reason about?

Or are A and B really intended to be atomic variables?

> > > > 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.
> 
> Thanks. We should probably hold off on the formal analysis at this point
> (I'm inclined to believe it is ok myself). The last version of the C++
> document included an SC store along with the RMW stuff in the
> synchronizes-with clause. I am doubtful that including the store there
> is correct for PPC, and Hans was going to think about it. We can hold
> off going to the architects until then and perhaps until convergence on
> this last point on the form of the spec.

Fair enough!

						Thanx, Paul

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