Fear and Loathing in Lock-Free Programming

I agree with this, mostly.

Sometimes the lock free version of a Java program is simpler than the version with locks. For example, I've often written classes where all the state was easy to fit into a single atomicreference.

The real danger comes from writing a lock free program without knowing they type of problems that are hard to solve without locks. Just like cryptography, the greatest danger comes from engineers who know just enough to be dangerous.

Lock free systems are often worth the effort. A classic example is the operating system thesis done by Henry Masslin. http://web.cecs.pdx.edu/~walpole/class/cs510/papers/06.pdf

What is the state of the art in building high assurance lock free components? Are there type systems or proof assistants that are workable?

SPIN is a nice tool for modeling them. You can extract code from a coq model. You can go into the world of dynamic instrumentation to try to verify invariants in implementations.

we were somewhere around a race condition, at the edge of frustration, when the drugs began to take hold...