2026-07-22T06:49:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20879 2024-09-12T05:48:35Z ddc:004 open_access

Verifying Lock-Free Search Structure Templates Patel, Nisarg Shasha, Dennis Wies, Thomas skiplists lock-free separation logic linearizability future-dependent linearization points hindsight reasoning 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nisarg Patel and Dennis Shasha and Thomas Wies 2024 Is Part Of LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2024.30 urn:nbn:de:0030-drops-208797 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.30 eng https://creativecommons.org/licenses/by/4.0/legalcode