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

[Boehm, Hans]

In order not to leave this hanging for everyone else:

Sarita and I talked about this a bit.

The difficulty with starting with SC for race-free programs is that it's
not really possible to define the notion of a race in the absence of
some semantics for low level atomics, since "data-race-free in an SC
execution" is no longer quite the right notion.

Canonical example:

Thread 1:
	x.store_relaxed(1);
	r1 = y.load_relaxed();
	if (r1 == 0) z = 17;

Thread 2:
	y.store_relaxed(1);
	r2 = x.load_relaxed();
	if (r2 == 0) z = 42;

(Or use the variant with acquire/release instead of relaxed.)

This has no race in an SC interpretation, but has to be viewed as having
a race.

Low-level atomics really do complicate matters.

On the other hand, I think this can actually be repaired with the
addition of one more clause to 1.10p10.

In spite of one (somewhat enlightening) false start, I still believe
that, and hope to post more shortly.

Hans

> -----Original Message-----
> From: Sarita V Adve [mailto:sadve at cs.uiuc.edu] 
> Sent: Tuesday, June 26, 2007 1:16 PM
> To: Boehm, Hans; C++ threads standardisation
> Subject: RE: [cpp-threads] Slightly revised memory model 
> proposal (D2300)
> 
> 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
> > > > 
> > > 
> > 
>