Proving that non-blocking algorithms don't block

Alexey Gotsman ( University of Cambridge )

A concurrent data-structure implementation is considered non-blocking if it meets one of three commonly accepted liveness criteria: wait-freedom, lock-freedom, or obstruction-freedom. To date, their proofs for non-trivial algorithms have been only manual pencil-and-paper semi-formal proofs. I will describe the first automatic tool that allows developers to ensure that their algorithms are indeed non-blocking. Our tool uses ideas from rely-guarantee reasoning and separation logic while overcoming the technical challenge of sound reasoning in the presence of interdependent liveness properties. This is joint work with Byron Cook, Matthew Parkinson, and Viktor Vafeiadis.