DROPS

Document

Concurrent Data Structures Linked in Time (Artifact)

Authors: Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract

This artifact provides the full mechanization in FCSL of the developments in the companion paper, "Concurrent Data Structures Linked in Time". In the latter, 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 illustrate the method by verifying (mechanically in FCSL) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients. FCSL is the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning.

Cite as

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{delbianco_et_al:DARTS.3.2.4,
  author =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  title =	{{Concurrent Data Structures Linked in Time (Artifact)}},
  pages =	{4:1--4:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.4},
  URN =		{urn:nbn:de:0030-drops-72850},
  doi =		{10.4230/DARTS.3.2.4},
  annote =	{Keywords: separation logic, linearization Points, concurrent snapshots, FCSL}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2017.8

Concurrent Data Structures Linked in Time

Authors: Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

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.

Cite as

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{delbianco_et_al:LIPIcs.ECOOP.2017.8,
  author =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  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 =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.8},
  URN =		{urn:nbn:de:0030-drops-72558},
  doi =		{10.4230/LIPIcs.ECOOP.2017.8},
  annote =	{Keywords: Separation logic, Linearization Points, Concurrent snapshots, FCSL}
}

Search Results

Documents authored by Delbianco, Germán Andrés

Concurrent Data Structures Linked in Time (Artifact)

Abstract

Cite as

Concurrent Data Structures Linked in Time

Abstract

Cite as

Thanks for your feedback!

Could not send message