> there is the gap between implementation and formal description of an algorithm. Incorrect implementation will obviate the guarantees your formal proof is asse

> there is the gap between implementation and formal description of an algorithm. Incorrect implementation will obviate the guarantees your formal proof is asserting. Agree. One aspect of this wrt implementing lock-free algorithms in C++: Usually the academic papers assume a sequentially consistent memory model, so when you're implementing the algorithm you have to work out how to place the memory barriers correctly (a potentially non-trivial task, as other comments on this page demonstrate).