Verifying Lock-Free Search Structure Templates

Nisarg Patel, Dennis Shasha, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication38th European Conference on Object-Oriented Programming, ECOOP 2024
EditorsJonathan Aldrich, Guido Salvaneschi
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959773416
DOIs
StatePublished - Sep 2024
Event38th European Conference on Object-Oriented Programming, ECOOP 2024 - Vienna, Austria
Duration: Sep 16 2024Sep 20 2024

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume313
ISSN (Print)1868-8969

Conference

Conference38th European Conference on Object-Oriented Programming, ECOOP 2024
Country/TerritoryAustria
CityVienna
Period9/16/249/20/24

Keywords

  • future-dependent linearization points
  • hindsight reasoning
  • linearizability
  • lock-free
  • separation logic
  • skiplists

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Verifying Lock-Free Search Structure Templates'. Together they form a unique fingerprint.

Cite this