UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Proving that non-blocking algorithms don't block

Gotsman, A; Cook, B; Parkinson, M; Vafeiadis, V; (2009) Proving that non-blocking algorithms don't block. ACM SIGPLAN Notices , 44 (1) pp. 16-28.

Full text not available from this repository.


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.

Type: Article
Title: Proving that non-blocking algorithms don't block
URI: http://discovery.ucl.ac.uk/id/eprint/1378178
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item