Proving that non-blocking algorithms don't block

A concurrent data-structure implementation is considered nonblocking if it meets one of three following liveness criteria: waitfreedom, lock-freedom, or obstruction-freedom. Developers of nonblocking algorithms aim to meet these criteria. However, to date their proofs for non-trivial algorithms have been only manual pencil-and-paper semi-formal proofs. This paper proposes the first fully automatic tool that allows developers to ensure that their algorithms are indeed non-blocking. Our tool uses rely-guarantee reasoning while overcoming the technical challenge of sound reasoning in the presence of interdependent liveness properties. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms Languages, Theory, Verification Keywords Formal Verification, Concurrent Programming, Liveness, Termination

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis
• Keywords: Concurrent Data-structure Implementation, Keywords Formal Verification, Pencil-and-paper Semi-formal Proofs, POPL 2009, Programming Languages