University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > The Importance of Being Linearizable

The Importance of Being Linearizable

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

Specifications of concurrent libraries are commonly given by the well-known notion of linearizability. However, to date linearizability has been no more than a box to be ticked in a paper with a new concurrent algorithm, lest it should get rejected. The notion has not even been defined for realistic settings in which concurrent algorithms usually get used! Recently, we have been trying to show that linearizability is more important than that by generalising it to realistic settings and establishing theorems that allow exploiting it to verify concurrent programs compositionally.

In this talk, I will present our definition of linearizability on the TSO weak memory model (used by Intel processors) and a theorem showing that, while verifying a client using a concurrent library, we can soundly replace the library by another one related to the original library by our generalisation of linearizability.

This is joint work with Sebastian Burckhardt, Madan Musuvathi (Microsoft Research) and Hongseok Yang (University of Oxford, UK).

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity