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

[Sarita V Adve]

Ok. I am concerned there may be a fundamental problem with the current
specification approach (given all of the other goals). I refer to the
approach of describing the model as an all-encompassing definition of
"consistent" and then showing that this definition implies SC for drf
programs. I think that any such definition of "consistent" is likely to
be too strong (e.g., it will prohibit aggressive speculation related
optimizations) or too weak (it will allow examples like the one below). 

An approach that could work given all of the other goals is to define
the model as "SC for data-race-free programs" + "something" catered to
relaxed atomics. The latter "something" would be an expanded form of
happens-before consistency, expanded to include intended ordering for
relaxed atomics (it does not have to take into account examples like the
one below, which are tricky to capture due to the data/control
dependence stuff). Unfortunately, without more formal PPC spec, it seems
difficult to formalize this latter ordering in a meaningful way. 

Sarita
 

> -----Original Message-----
> From: Boehm, Hans [mailto:hans.boehm at hp.com] 
> Sent: Tuesday, June 26, 2007 2:33 PM
> To: Sarita V Adve; C++ threads standardisation
> Subject: RE: [cpp-threads] Slightly revised memory model 
> proposal (D2300)
> 
>  
> 
> > -----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
> > > 
> > 
>