IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2014 > Parametrised Linearisability

Andrea Cerone

Tuesday, April 8, 2014

11:00am Meeting room 302 (Mountain View), level 3

Andrea Cerone, Post-doctoral Researcher, IMDEA Software Institute

Parametrised Linearisability

Abstract:

Many concurrent libraries are parameterised, meaning that they implement generic algorithms that take another library as a parameter. In such cases, the standard way of stating the correctness of concurrent libraries via linearisability is inapplicable. We generalise linearisability to parameterised libraries and investigate subtle trade-offs between the assumptions that such libraries can make about their environment and the conditions that linearisability has to impose on different types of interactions with it. We prove that the resulting parameterised linearisability is closed under instantiating parameter libraries and composing several non-interacting libraries, and furthermore implies observational refinement. These results allow modularising the reasoning about concurrent programs using parameterised libraries and confirm the appropriateness of the proposed definitions. We illustrate the applicability of our results by proving the correctness of a parameterised library implementing flat combining.