Linearizability with ownership transfer

DOI10.1007/978-3-642-32940-1_19MaRDI QIDQ5891776zbMATH OpenOpenAlexFDO

Authors Alexey Gotsman, Hongseok Yang

Publication date 25 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1308.2507

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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 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.

Recommendations

• Linearizability with ownership transfer
• Higher-order linearisability
• Higher-order linearisability
• Concurrent Library Correctness on the TSO Memory Model
• A generic logic for proving linearizability

Cited in

(8)

• A perspective on specifying and verifying concurrent modules
• A generic logic for proving linearizability
• Higher-order linearisability
• Proving linearizability using partial orders
• Higher-order linearisability
• Parameterised linearisability
• Linearizability with ownership transfer
• Steps in modular specifications for concurrent modules (invited tutorial paper)

This page was built for publication: Linearizability with ownership transfer

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5891776)