Document Open Access Logo

Verifying Lock-Free Search Structure Templates (Artifact)

Authors Nisarg Patel , Dennis Shasha , Thomas Wies

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.10.2.15.pdf
  • Filesize: 453 kB
  • 2 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
  • Theory of computation → Shared memory algorithms
Keywords
  • skiplists
  • lock-free
  • separation logic
  • linearizability
  • future-dependent linearization points
  • hindsight reasoning

Metrics

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

Abstract

We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris' support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.

Cite As Get BibTex

Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/DARTS.10.2.15

Author Details

Nisarg Patel
  • New York University, NY, USA
Dennis Shasha
  • New York University, NY, USA
Thomas Wies
  • New York University, NY, USA

Funding

This work is funded in parts by NYU Wireless and by the United States National Science Foundation under grants CCF-2304758, 1840761, 2304758, and 25-74100-F1202. Further funding came from an Amazon Research Award Fall 2021. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not reflect the views of Amazon.

Artifact

  MD5 Sum: c6be28b5f055d3388227d32bd080121c (Get MD5 Sum)

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Related Article

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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact