Are you saying this one isn't correct? Confused what point you're trying to make.
Certain architectures have different semantics when it comes to that ordering so something that works on x86 for instance might explode on PPC or ARM. If you want to verify that the algorithms are correct you basically have to do static analysis and the only way you'll do that is if you have access to the microcode and register models(I.E. you make CPUs).
[edit]
To put this into practical terms I spent some time working with a popular game engine that used a lockfree queue at it's core rendering path. It wasn't until 2 or 3 titles had shipped on this engine that it was discovered that there was a bug in the lockfree algo. We're talking trillions of operations under many different threading and context switching loads and at least 3 different CPU architectures.
The code in the OP does use memory fences. Are you implying that their implementation are incorrect?
Generally if there's not a huge organization putting their reputation(and $$$) on the line there is going to be bugs.
Most of the time if you're going lockfree for performance reasons there's usually much large gains to be found in your cache usage or overall architecture.
This argument applies to any hard problem, so it doesn't seem valid. Whether there's an important bug in a project depends on someone's skill and on how much time they've dedicated to it, and it's hard to know how skilled or dedicated someone is.
The entire problem of rolling your own security code is that you will never know if you messed it up.
For functional code this is only an issue with silent corrupted data.
In addition the error class is a mean one: doesn't happen often statistically and difficult to reproduce and as such can be very expensive to track down.
I have no issue with hard problems but the accountability for concurrency issues is gnarly. I've had driver issues look like concurrency bugs and concurrency bugs look like driver issues. If you feel the need to take on concurrency you better have the schedule budget for it or be willing to throw it away.
In the absence of formal proof think 50+ machines. You basically setup a lab to run 24/7 and a/b with a hope that you repro.
Same technique works for really gnarly intermittent driver bugs.
It's still no guarantee but at least you get in the same range assuming the execution profile is diverse and robust.