Linearizability with Ownership Transfer

7 years 8 months ago
Linearizability with Ownership Transfer
Abstract. Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type. This is inappropriate for common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection. In this paper, we present the first definition of linlity that lifts this limitation and establish an Abstraction Theorem: while proving a property of a client of a concurrent library, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. We also prove that linearizability with ownership transfer can be derived from the classical one if the library does not access some of data structures transferred to it by the c...
Alexey Gotsman, Hongseok Yang
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Authors Alexey Gotsman, Hongseok Yang
Comments (0)