What are the C++11 memory ordering guarantees in this corner case?

Signal fences don't provide the necessary guarantees (well, not unless 'thread 2' is a signal hander that actually runs on 'thread 1').

To guarantee correct behavior we need synchronization between threads, and the fence that does that is std::atomic_thread_fence.

Let's label the statements so we can diagram various executions (with thread fences replacing signal fences, as required):

while (true) {    auto a_local = a.fetch_add(1, std::memory_order_relaxed); // A    std::atomic_thread_fence(std::memory_order_acq_rel);      // B    b.fetch_add(1, std::memory_order_relaxed);                // C}

auto b_local = b.load(std::memory_order_relaxed);             // Xstd::atomic_thread_fence(std::memory_order_acq_rel);          // Yauto a_local = a.fetch_add(1, std::memory_order_relaxed);     // Z

So first let's assume that X loads a value written by C. The following paragraph specifies that in that case the fences synchronize and a happens-before relationship is established.

29.8/2:

A release fence A synchronizes with an acquire fence B if there exist atomic operations X and Y, both operating on some atomic object M, such that A is sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value written by X or a value written by any side effect in the hypothetical release sequence X would head if it were a release operation.

And here's a possible execution order where the arrows are happens-before relations.

Thread 1: A₁ → B₁ → C₁ → A₂ → B₂ → C₂ → ...                ↘Thread 2:    X → Y → Z

If a side effect X on an atomic object M happens before a value computation B of M, then the evaluation B shall take its value from X or from a side effect Y that follows X in the modification order of M. — [C++11 1.10/18]

So the load at Z must take its value from A₁ or from a subsequent modification. Therefore the assert holds because the value written at A₁ and at all later modifications is greater than or equal to the value written at C₁ (and read by X).

Now let's look at the case where the fences do not synchronize. This happens when the load of b does not load a value written by thread 1, but instead reads the value that b is initialized with. There's still synchronization where the threads starts though:

30.3.1.2/5

Synchronization: The completion of the invocation of the constructor synchronizes with the beginning of the invocation of the copy of f.

This is specifying the behavior of std::thread's constructor. So (assuming the thread creation is correctly sequenced after the initialization of a) the value read by Z must take its value from the initialization of a or from one of the subsequent modifications on thread 1, which means that the assertions still holds.

This example gets at a variation of reads-from-thin-air like behavior. The relevant discussion in the spec is in section 29.3p9-11. Since the current version of the C11 standard doesn't guarantee dependences be respected, the memory model should allow the assertion to be fired. The most likely situation is that the compiler optimizes away the check that a_local>=0. But even if you replace that check with a signal fence, CPUs would be free to reorder those instructions.You can test such code examples under the C/C++11 memory models using the open source CDSChecker tool.The interesting issue with your example is that for an execution to violate the assertion, there has to be a cycle of dependences. More concretely:

The b.fetch_add in thread one depends on the a.fetch_add in the same loop iteration due to the if condition. The a.fetch_add in thread 2 depends on b.load. For an assertion violation, we have to have T2's b.load read from a b.fetch_add in a later loop iteration than T2's a.fetch_add. Now consider the b.fetch_add the b.load reads from and call it # for future reference. We know that b.load depends on # as it takes it value from #.

We know that # must depend on T2's a.fetch_add as T2's a.fetch_add atomic reads and updates a prior a.fetch_add from T1 in the same loop iteration as #. So we know that # depends on the a.fetch_add in thread 2. That gives us a cycle in dependences and is plain weird, but allowed by the C/C++ memory model. The most likely way of actually producing that cycle is (1) compiler figures out that a.local is always greater than 0, breaking the dependence. It can then do loop unrolling and reorder T1's fetch_add however it wants.

After reading all the responses so far and combing through the standard myself, I don't think it can be shown that the code is correct using only the standard.

And unless you admit that non atomic operations are magically safer and more ordered then relaxed atomic operations (which is silly) and that there is one semantic of C++ without atomics (and try_lock and shared_ptr::count) and another semantic for those features that don't execute sequentially, you also have to admit that no program at all can be proven correct, as the non atomic operations don't have an "ordering" and they are needed to construct and destroy variables.

Or, you stop taking the standard text as the only word on the language and use some common sense, which is always recommended.