Simplifying proofs of lock-freedom

Speaker: Brijesh Dongol

When: 10:30, Friday, 20 October 2006

Venue: 78-420

A program is non-blocking if it uses non-blocking primitives such as compare-and-swap for synchronisation instead of locks and blocking. A non-blocking program is lock-free if the system as a whole is guaranteed to make progress. The formal definition of lock-freedom is elegant as it closely matches the intuitive notion of lock-freedom, however, it has so far been difficult to work with because of its generality. In this talk, we present techniques for simplifying proofs of lock-freedom. We present a simple example to demonstrate our techniques.

Hospitality: Rob Colvin

Contact: Phil Cook (SSE seminar co-ordinator) (philc@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html