@inproceedings{ba388ccce58e437ba6e5b7289ea68b7f,
title = "Verifying Lock-Free Search Structure Templates",
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{\textquoteright} 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.",
keywords = "future-dependent linearization points, hindsight reasoning, linearizability, lock-free, separation logic, skiplists",
author = "Nisarg Patel and Dennis Shasha and Thomas Wies",
note = "Publisher Copyright: {\textcopyright} Nisarg Patel, Dennis Shasha, and Thomas Wies;; 38th European Conference on Object-Oriented Programming, ECOOP 2024 ; Conference date: 16-09-2024 Through 20-09-2024",
year = "2024",
month = sep,
doi = "10.4230/LIPIcs.ECOOP.2024.30",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Jonathan Aldrich and Guido Salvaneschi",
booktitle = "38th European Conference on Object-Oriented Programming, ECOOP 2024",
}