UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Proving that non-blocking algorithms don't block

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

Full text not available from this repository.

Abstract

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
UCL classification:UCL > School of BEAMS > Faculty of Engineering Science > Computer Science

Archive Staff Only: edit this record