3 ms·
> Would you use a distributed algorithm that didn't come with a correctness proof? That happens all the time in practice. Prior to Kyle Kingsbury's influential
by eternalban 10y ago
> Would you use a distributed algorithm that didn't come with a correctness proof?
That happens all the time in practice. Prior to Kyle Kingsbury's influential blogs on noSQL darlings, for example, it was not even on the geek-pop radar.
And then, quite frankly, there is the gap between implementation and formal description of an algorithm. Incorrect implementation will obviate the guarantees your formal proof is asserting.
- RossBencina 10y ago> 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).