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

[Sarita V Adve]

Just a subtle additional point (after thinking a little more about our
conversation) -

I am assuming there is still a need to convey a simple model to the
"masses" who will use locks and SC atomics (and not relaxed atomics).
And that there isn't yet a simple enough alternative to "SC for DRF
programs" for this purpose.

If the above is true, then doesn't it follow that we have to define
data-race-free in an SC-centric way? It then seems to follow that the
example below should not be classified as drf. One possible simple (not
necessarily best and not yet proven correct) way to do that is to say
that programs with relaxed atomics (in SC executions) are not considered
drf. Then immediately such programs require reasoning with the more
complex model, but that's the cost of using relaxed-atomics. There may
be other options as well that articulate limited uses of relaxed-atomics
that also allow using SC-centric drf definition.

In summary, the point I am making is that if a data race is not defined
in terms of SC executions, then we lose a lot of what we were after (at
least in several previous discussions). In yet other words, if people
restricting themselves to sc atomics have to reason with the complex
model anyway, then it isn't clear that the distinction between relaxed
and sc atomics is driven by "ease-of-use."

Please let me know if I missed something in our conversation.

Sarita

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