Alexey Gotsman ; Hongseok Yang - Linearizability with Ownership Transfer

lmcs:931 - Logical Methods in Computer Science, September 9, 2013, Volume 9, Issue 3 -
Linearizability with Ownership Transfer

Authors: Alexey Gotsman ; Hongseok Yang

    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 linearizability 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. This allows abstracting from the details of the library implementation while reasoning about the client. 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 client.

    Volume: Volume 9, Issue 3
    Published on: September 9, 2013
    Accepted on: June 25, 2015
    Submitted on: February 15, 2013
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1145/2796550
    • 10.1145/2796550
    • 10.1145/2796550
    • 10.1145/2796550
    A Comparative Survey
    Dongol, B ; Derrick, J ;

    3 Documents citing this article


    Consultation statistics

    This page has been seen 485 times.
    This article's PDF has been downloaded 180 times.