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

[Boehm, Hans]

> -----Original Message-----
> From: Paul E. McKenney [mailto:paulmck at linux.vnet.ibm.com] 
> Sent: Friday, June 15, 2007 10:54 AM
> To: Boehm, Hans
> Cc: C++ threads standardisation; Nick Maclaren
> Subject: Re: [cpp-threads] Slightly revised memory model 
> proposal (D2300)
> 
> On Fri, Jun 15, 2007 at 09:09:39AM -0700, Hans Boehm wrote:
> > 
> > to flickering.  I believe the version of the example that I posted:
> > 
> > > > Thread 1:
> > > > store_relaxed(&x, 1);
> > > >
> > > > Thread 2:
> > > > store_relaxed(&x, 2);
> > > >
> > > > Thread 3:
> > > > r1 = load_acquire(&x); (1)
> > > > r2 = load_acquire(&x); (2)
> > > > r3 = load_acquire(&x); (1)
> > > >
> > is already allowed to flicker under the D2300 rules.
> 
> 1.10p8 says:
> 
> 	An evaluation A happens before an evaluation B if:
> 
> 	* A is sequenced before B and either A performs an acquire
>           operation or B performs a release operation; or
> 	* A synchronizes with B; or
> 	* for some evaluation X, A happens before X and X 
> happens before B. 
> 
> The first bullet applies to all pairs of Thread 3's 
> assignments, since each of those statements performs an 
> acquire operation.
> 
> 1.10p6 says:
> 
> 	All modifications to a particular atomic object M occur in some
> 	particular total order, called the modification order 
> of M. [Note:
> 	The modification orders reflect the order in which updates to a
> 	single variable become globally visible. In the case of relaxed
> 	atomic operations, both assignments to and reads from the object
> 	may effectively be locally reordered, so the modification order
> 	may only be very indirectly observable. Repeated load_acquire
> 	operations on the same atomic object must observe some subset
> 	of the updates in modification order. -end note ]
> 
> Therefore, both thread 1's and thread 2's assignments should 
> happen only once with respect to any given thread.
> 
> So, why doesn't the combination of 1.10p6 and 1.10p8 prohibit 
> store flickering?  What am I missing here?

The short answer is that the note is in error.  I will fix it.  The note
does not follow from the binding parts of the proposal, as it should.
Modification order affects visibility only in that it affects
synchronizes-with (which we are about to remove) and as described in
1.10p10.  Since the stores don't happen before anything, 1.10p10 does
not apply.

> 
> >                                                      And 
> looking back 
> > at Sarita's example, weakening this doesn't seem to help.  (The 
> > example that we should really have been discussing would 
> have had release stores.
> > That's the one that's currently constrained by the 
> modification order 
> > rule.  And having that flicker does seem dubious.)
> > 
> > I think the kind of flickering that we already allow is 
> unavoidable if 
> > we assume that unpaired acquires behave like relaxed operations.
> 
> If I read 1.10p8 correctly, unpaired acquires still have some 
> strong semantics over those of relaxed operations.

They currently do have some, as a result of the precedes definition.  As
I said in my last message, I think those need to disappear, too.
Otherwise we again end up with low-level atomics interfering with lock
elimination, which I don't think is acceptable.

> > The D2300 proposal doesn't change this, but it does move to 
> the weaker 
> > synchronizes-with model, as Paul points out below.
> > 
> > I think I agree with Paul's general direction for the rest of this, 
> > but I need to think more about the details.  I think we want to aim 
> > for
> > 
> > - Basically the D2300 model, but
> > - some way to strengthen 1.10p7 to explicitly add 
> "synchronizes-with"
> > relationships for certain later reads, if the intervening 
> operatons on 
> > that variable were all RMW ops.
> 
> If "all RMW ops" becomes "all non-relaxed RMW ops", then I 
> believe that we are in agreement.

Why not relaxed operations?  If a fetch_add_relaxed(..., 0) is performed
between the store and the load,which should that affect
synchronizes-with?

Another revision of D2300 is coming up ...

Hans