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

Concurrent Data Structures Linked in Time (Artifact)

Delbianco, GA; Sergey, I; Nanevski, A; Banerjee, A; (2017) Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Series , 3 (2) 4:1-4:4. 10.4230/DARTS.3.2.4. Green open access

DARTS-3-2-4.pdf - Published version

Download (473kB) | Preview


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.

Type: Article
Title: Concurrent Data Structures Linked in Time (Artifact)
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/DARTS.3.2.4
Publisher version: http://dx.doi.org/10.4230/DARTS.3.2.4
Language: English
Additional information: Copyright © The authors; licensed under Creative Commons Attribution 3.0 Germany (CC BY 3.0 DE) (https://creativecommons.org/licenses/by/3.0/de/).
Keywords: separation logic, linearization points, concurrent snapshots, FCSL
UCL classification: UCL
UCL > Provost and Vice Provost Offices
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/10046702
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item