The problem here is the [1] // Do stuff [2] Buffer[X]. available = Y There is no explicit nor implicit ordering between 1 and 2, so the compiler or cpu ca

The problem here is the [1] // Do stuff [2] Buffer[X]. available = Y There is no explicit nor implicit ordering between 1 and 2, so the compiler or cpu can reorder them. You need a release barrier between the two. Also while most CPUs preserve the control dependency, not all do (famously Alpha), and certainly not compilers. You would need a consume barrier, except that c++11 consume is only for data dependencies and unimplemented anyway. Edit: with the correct barriers in place, you can prove correctness by similitude to two size 1 SPSC queues used to exchange a mutual exclusion token, with the added quirk that as the queues are never used at the same time, they can actually be physically colocated in memory.