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
experts than the model for C++ with only sequentially consistent atomics. You can no longer reason about interleaving thread actions, either for
non- 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