License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.3.2.4
URN: urn:nbn:de:0030-drops-72850
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7285/
Go back to Dagstuhl Artifacts Series

Delbianco, Germán Andrés ; Sergey, Ilya ; Nanevski, Aleksandar ; Banerjee, Anindya

Concurrent Data Structures Linked in Time (Artifact)

pdf-format:
DARTS-3-2-4.pdf (0.5 MB)

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.

BibTeX - Entry

@Article{delbianco_et_al:DARTS:2017:7285,
  author =	{Germ{\'a}n Andr{\'e}s Delbianco and Ilya Sergey and Aleksandar Nanevski and Anindya Banerjee},
  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},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7285},
  URN =		{urn:nbn:de:0030-drops-72850},
  doi =		{10.4230/DARTS.3.2.4},
  annote =	{Keywords: separation logic, linearization Points, concurrent snapshots, FCSL}
}

Keywords: separation logic, linearization Points, concurrent snapshots, FCSL
Collection: DARTS, Volume 3, Issue 2
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.8
Issue Date: 2017
Date of publication: 20.06.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI