Verifying Lock-free Search Structure Templates

TL;DR

This paper introduces verified lock-free search structure templates, providing modular, mechanized proofs of linearizability for a broad class of concurrent data structures using Iris logic.

Contribution

It offers a modular verification framework for lock-free search structures and mechanizes a novel method for reasoning about future-dependent linearization points.

Findings

Mechanized proofs of linearizability for list and skiplist-based structures

A new method using hindsight arguments reduces proof effort

Flexible verification covering various data structure designs

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.