Linearizability with Ownership Transfer

Cited 2 time in webofscience Cited 0 time in scopus
  • Hit : 130
  • Download : 0
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.
Publisher
TECH UNIV BRAUNSCHWEIG
Issue Date
2013
Language
English
Article Type
Article
Citation

LOGICAL METHODS IN COMPUTER SCIENCE, v.9, no.3

ISSN
1860-5974
DOI
10.2168/LMCS-9(3:12)2013
URI
http://hdl.handle.net/10203/225277
Appears in Collection
CS-Journal Papers(저널논문)
Files in This Item
There are no files associated with this item.
This item is cited by other documents in WoS
⊙ Detail Information in WoSⓡ Click to see webofscience_button
⊙ Cited 2 items in WoS Click to see citing articles in records_button

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0