Concurrent Data Structures Linked in Time (Artifact)

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



PDF
Thumbnail PDF

Artifact Description

DARTS.3.2.4.pdf
  • Filesize: 462 kB
  • 4 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

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)
https://doi.org/10.4230/DARTS.3.2.4

Artifact

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.
Keywords
  • separation logic
  • linearization Points
  • concurrent snapshots
  • FCSL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, , Anindya Banerjee, and Germán Andrés Delbianco. FCSL: Fine-grained concurrent separation logic. URL: http://software.imdea.org/fcsl/.
  2. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Anindya Banerjee, and Germán Andrés Delbianco. Mechanized verification of fine-grained concurrent programs in fine-grained concurrent separation logic: User manual and code commentary. URL: http://software.imdea.org/fcsl/papers/fcsl-manual.pdf.
  3. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In Zhong Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014. Proceedings, volume 8410 of LNCS, pages 290-310. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_16.
  4. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In David Grove and Steve Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pages 77-87. ACM, 2015. URL: http://dx.doi.org/10.1145/2737924.2737964.
  5. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In Jan Vitek, editor, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015. Proceedings, volume 9032 of LNCS, pages 333-358. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_14.
  6. Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 92-110. ACM, 2016. URL: http://dx.doi.org/10.1145/2983990.2983999.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail