The Importance of Being Linearizable

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

• Alexey Gotsman, IMDEA Software Institute
• Monday 07 November 2011, 12:45-14:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.