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.