Re: [boost] [lockfree] review

Subject: Re: [boost] [lockfree] review
From: Hans Boehm (Hans.Boehm_at_[hidden])
Date: 2011-08-29 17:03:29

Dave Abrahams <dave <at> boostpro.com> writes:

> And that actually supports what I've been saying.  It doesn't really
> matter if a program with data races can observe such a reordering,
> because programs with data races invoke undefined behavior, so they can
> observe the moon being carved open to reveal green cheese.
> 
> > If we change x and y to be atomic variables, and the stores to be 
> > memory_order_relaxed, then an observer can tell the difference.  
> 
> Meaning a data-race-free observer. 
Yes.

> on Fri Aug 26 2011, "Boehm, Hans" <hans.boehm-AT-hp.com> wrote:
> 
> > In my mind, the main way in which sequential consistency differs from the 
> > cheaper acquire/release semantics that Alexander wants is that
> >
> > a) Dekker's algorithm (which by itself isn't that practically 
interesting), 
> > plus a number of real lock-free algorithms (which do matter) don't
> > work.
> 
> Don't work with with SC or with acquire/release semantics?
Don't work with just acquire/release semantics.  Sorry about being unclear.

> 
> > b) In my mind, acquire/release is a far more difficult model to explain to 
non-
> > experts than the model for C++ with only sequentially consistent atomics.  
You 
> > can no longer reason about interleaving thread actions, either for 
purposes of 
> > determining the existence of a data-race, nor when defining what data-race-
> > free programs mean.
> 
> How *do* you reason about data races in that model?
> 
You can clearly reason explicitly in terms of happens-before ordering, as in 
1.10 of the standard.  I think you can also informally reason in a way similar 
to the sequentially consistent model, but you have to consider that atomic 
(release) stores are indefinitely buffered, and only become visible to other 
threads at some later time, but in their original order.  I haven't thought 
enough about the implications this would have on programming rules and 
interface specifications.

The canonical example of how this gets tricky, based on Dekker's example, is 
(thread1_busy, thread2_busy acquire/release atomics, z an ordinary variable, 
everything initially zero/false):

Thread 1:
thread1_busy = true;
if (!thread2_busy) {
    // thread 2 either not busy, or will see that we are
    z = 17;
}

Thread 2:
thread2_busy = true;
if (!thread1_busy) {
    // thread 1 either not busy, or will see that we are
    z = 42;
}

This DOES have a data race in the acquire/release model, i.e. the comments are 
incorrect.  And that race can't be understood in terms of interleaving.  But 
you can understand it if you explicitly reason about buffered stores.

Unfortunately, I think you also need to view unlock operations as getting 
buffered, and occuring at a later time, since the first and fourth operation in

x.store(1, memory_order_release);
m.unlock();
m2.lock();
r1 = y.load(memory_order_acquire);

can become visible out of order.

The acquire/release model is more-or-less what is used by C# volatiles, for 
better or worse.  Some of the Microsoft Research folks have thought about it 
more than I have.

Hans