Fear and Loathing in Lock-Free Programming
1–6 of 6 posts
Re: Fear and Loathing in Lock-Free Programming
#2we were somewhere around a race condition, at the edge of frustration, when the drugs began to take hold...
Re: Fear and Loathing in Lock-Free Programming
#3Lock 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
Re: Fear and Loathing in Lock-Free Programming
#4What is the state of the art in building high assurance lock free components? Are there type systems or proof assistants that are workable?
Re: Fear and Loathing in Lock-Free Programming
#5What 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.
Re: Fear and Loathing in Lock-Free Programming
#6I 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.