License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.8
URN: urn:nbn:de:0030-drops-72558
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7255/
Delbianco, Germán Andrés ;
Sergey, Ilya ;
Nanevski, Aleksandar ;
Banerjee, Anindya
Concurrent Data Structures Linked in Time
Abstract
Arguments about correctness of a concurrent data structure are
typically carried out by using the notion of linearizability and
specifying the linearization points of the data structure's
procedures. Such arguments are often cumbersome as the linearization
points' position in time can be dynamic (depend on the interference,
run-time values and events from the past, or even future), non-local
(appear in procedures other than the one considered), and whose
position in the execution trace may only be determined after the
considered procedure has already terminated.
In this paper we propose a new method, based on a separation-style
logic, for reasoning about concurrent objects with such linearization
points. We embrace the dynamic nature of linearization points, and
encode it as part of the data structure's auxiliary state, so that it
can be dynamically modified in place by auxiliary code, as needed when
some appropriate run-time event occurs. We name the idea
linking-in-time, because it reduces temporal reasoning to spatial
reasoning. For example, modifying a temporal position of a
linearization point can be modeled similarly to a pointer update in
separation logic. Furthermore, the auxiliary state provides a
convenient way to concisely express the properties essential for
reasoning about clients of such concurrent objects. We illustrate the
method by verifying (mechanically in Coq) an intricate optimal
snapshot algorithm due to Jayanti, as well as some clients.
BibTeX - Entry
@InProceedings{delbianco_et_al:LIPIcs:2017:7255,
author = {Germ{\'a}n Andr{\'e}s Delbianco and Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee},
title = {{Concurrent Data Structures Linked in Time}},
booktitle = {31st European Conference on Object-Oriented Programming (ECOOP 2017)},
pages = {8:1--8:30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-035-4},
ISSN = {1868-8969},
year = {2017},
volume = {74},
editor = {Peter M{\"u}ller},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7255},
URN = {urn:nbn:de:0030-drops-72558},
doi = {10.4230/LIPIcs.ECOOP.2017.8},
annote = {Keywords: Separation logic, Linearization Points, Concurrent snapshots, FCSL}
}
|
Keywords: |
|
Separation logic, Linearization Points, Concurrent snapshots, FCSL |
|
Collection: |
|
31st European Conference on Object-Oriented Programming (ECOOP 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
16.06.2017 |
