@article{gotsman2009proving,
author = {Gotsman, Alexey and Cook, Byron and Parkinson, Matthew J. and Vafeiadis, Viktor},
title = {Proving that non-blocking algorithms don't block},
year = {2009},
month = {January},
abstract = {A concurrent data-structure implementation is considered non-blocking if it meets one of three following liveness criteria: wait-freedom, lock-freedom, or obstruction-freedom. Developers of non-blocking 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.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/proving-that-non-blocking-algorithms-dont-block/},
pages = {16-28},
journal = {SIGPLAN Notices},
volume = {44},
edition = {SIGPLAN Notices},
number = {1},
}