Verifying Lock-free Search Structure Templates

TL;DR

This work develops template algorithms for lock-free concurrent search structures (lists and skiplists) and provides modular, mechanized proofs of linearizability using Iris. It parameterizes skiplists by height $L$, traversal style (eager vs lazy), node implementations, and higher-level maintenance order, enabling a single verification to cover many variants. A central technical advance is the formalization of hindsight reasoning within Iris, along with a general framework for relating hindsight-based specifications to client-level atomic specifications via prophecy variables and a helping protocol. The authors demonstrate substantial proof-effort reductions (e.g., a 53% reduction in a multicopy template) and verify unbounded-height skiplists, contributing a scalable approach to the formal verification of complex lock-free data structures with practical impact for correctness guarantees in concurrent systems.

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.

Figures (18)

• Figure 1: Skiplist with four levels. A node that is marked (logically deleted) at a level is shaded gray at that level. The red line indicates the path taken by a traversal searching for key $42$.
• Figure 2: The template algorithm for lock-free skiplists. The template can be instantiated by providing implementations of traverse and the helper functions markNode, createNode and changeNext. The markNode$\,i\;\mathit{c}$ attempts to mark node $\mathit{c}$ at level $i$ atomically, and fails if $\mathit{c}$ has been marked already. createNode$\,k\,h\,\mathit{cs}$ creates a new node $\mathit{e}$ of height $h$ containing $k$, and whose next pointers are set to nodes in array $\mathit{cs}$. Finally, changeNext$\,i\,\mathit{p}\,\,\mathit{c}\,\,\mathit{cn}$ is a CAS operation attempting to change the next pointer of $\mathit{p}$ from $\mathit{c}$ to $\mathit{cn}$. changeNext$\,i\,\mathit{p}\,\,\mathit{c}\,\,\mathit{cn}$ succeeds only if $\mathsf{mark}(\mathit{p}, i) = \mathit{false}$ and $\mathsf{next}(\mathit{p}, i) = \mathit{c}$. Other functions used here include randomNum to generate a random number and maintenance operations associated with insert and delete. maintainanceOp_del marks node $\mathit{c}$ at the higher levels, while maintainanceOp_ins inserts a new node $\mathit{e}$ at the higher levels.
• Figure 3: The maintenance operations for the skiplist. The $\textnormal{getHeight}\,\mathit{c}$ helper function returns $\mathsf{height}(\mathit{c})$. The permute function generates a permutation of $[1 \dots (h-1)]$ as an array.
• Figure 4: The eager traversal for the skiplist template. findNext$\,i\,k\,\,\mathit{c}$ returns a pair $(\mathsf{next}(\mathit{c}, i), \mathsf{mark}(\mathit{c}, i))$. The $\textnormal{getKey}\,\mathit{c}$ helper function returns $\mathsf{key}(\mathit{c})$.
• Figure 5: Sequential specification of a search structure. $k$ refers to the operation key, $C$ and $C'$ to the abstract state before and after operation $\mathtt{op}$, respectively, and $\mathit{res}$ is the return value of $\mathtt{op}$.