UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Concurrent Data Structures Linked in Time

Delbianco, GA; Sergey, I; Nanevski, A; Banerjee, A; (2017) Concurrent Data Structures Linked in Time. In: Muller, P, (ed.) Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). (pp. 8:1-8:30). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik: Dagstuhl, Germany. Green open access

[thumbnail of LIPIcs-ECOOP-2017-8.pdf]
Preview
Text
LIPIcs-ECOOP-2017-8.pdf - Published Version

Download (816kB) | Preview

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.

Type: Proceedings paper
Title: Concurrent Data Structures Linked in Time
Event: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
ISBN-13: 9783959770354
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.ECOOP.2017.8
Publisher version: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.8
Language: English
Additional information: Copyright © Germán Andrés Delbianco and Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee; licensed under Creative Commons Attribution 3.0 Unported license (CC-BY) (https://creativecommons.org/licenses/by/3.0/).
Keywords: Separation logic, Linearization Points, Concurrent snapshots, FCSL
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
URI: https://discovery.ucl.ac.uk/id/eprint/10030727
Downloads since deposit
9Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item