Document Open Access Logo

Verifying Lock-Free Search Structure Templates (Artifact)

Authors Nisarg Patel , Dennis Shasha , Thomas Wies

PDF
Thumbnail PDF

Artifact Description

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

Document Identifiers

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.

Cite AsGet 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

Artifact

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.

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.

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

Related Article

  • Nisarg Patel, Dennis Shasha, and Thomas Wies, "Verifying Lock-Free Search Structure Templates", in 38th European Conference on Object-Oriented Programming (ECOOP 2024), LIPIcs, Vol. 313, pp. 30:1-30:28, 2024. https://doi.org/10.4230/LIPIcs.ECOOP.2024.30
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact