Reader Q&A: Acquire/release and sequential consistency

Reader Ernie Cohen emailed me this morning to ask a question about one slide in my atomic<> Weapons talk from last year’s C++ and Beyond:

In your atomic weapons talk (part 1) (updated 2/15/2013) ,page 18, titled “Sc > Acq/Rel Alone: Some examples”, the first example listed “transitivity/causality”:

T0: g = 1; x = 1;

T1: if (x == 1) y = 1;

T2: if (y == 1) assert(g == 1);

I understood you to mean that the assertion might fail if the loads were simple C++11 acquires and the stores were simple C++ releases. But this works just fine with the weaker memory order; the operations in each thread are related by sequenced-before, the communications between the threads create happens-before, and without consumes happens-before is transitive, so there is a happens-before edge from g = 1 to the assertion. Am I missing something?

[Note: g is an ordinary variable, x and y are std::atomic, and all initially zero as usual.] The motivation behind this example, and the other example on the same slide, was to show that when we specified the C++ memory model and atomics, we had to consider more than individual acquire-release pairs in isolation, but also provide additional guarantees to ensure that the whole program was sequentially consistent (SC).

In the above example, yes, we guarantee that the assertion cannot fail with C++ acquire and release semantics, and making sure the memory model required this transitivity is exactly one of the two key points of this example. As you point out, it requires getting the “right” answer when combining sequenced-before and happens-before.

The second point illustrated here is that it was essential to support cases where the programmer could depend on reasoning based on tests of whether a particular write was read and then making SC assumptions based on the outcome of the test, otherwise the whole program wouldn’t be SC.

For completeness, the other example on the slide showed an additional case where individual pairwise acquire/release alone was insufficient to guarantee SC outcomes unless we added requirements. Here is the example, with x and y std::atomic and initially zero:

T1: x = 1;

T2: y = 1;

T3: if( x == 1 && y == 0 ) print( “x first” );

T4: if( y == 1 && x == 0 ) print( “y first” );

This illustrates the total store order requirement: It must be impossible to print both messages, else the result wouldn’t be SC.

Note that in most cases using (non-SC) memory_order_acquire and memory_order_release explicitly happens to give you SC results, except when they don’t (e.g., Dekker’s fails, and I think the second example above fails as well). And of course other relaxed atomics can allow non-SC results at the drop of a hat.