Proving that non-blocking algorithms don't block

Alexey Gotsman (University of Cambridge)

Info

Date	5th November 2008 (week 4, Michaelmas Term 2008)
Time	11:30
Place	Room 441, Oxford University Computing Laboratory

Abstract

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.