The Path to Durable Linearizability

TL;DR

This paper introduces a versatile, modular proof technique for establishing durable linearizability in persistent concurrent data structures, addressing a gap in formal correctness proofs for complex algorithms.

Contribution

It presents a general, powerful, modular, and incremental proof method for verifying durable linearizability across diverse persistent algorithms.

Findings

The technique can handle complex persistent algorithms in the literature.

It enables reuse of existing linearizability proofs.

Applied to various versions of a persistent set, including the link-free set.

Abstract

There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of \emph{durable linearizability} (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.