Proving Linearizability Using Reduction

TL;DR

This paper introduces three reduction-based proof methods for verifying linearizability of complex concurrent data structures, simplifying the process by treating certain operations as atomic at a higher abstraction level.

Contribution

The paper presents novel reduction methods that extend Lipton's theory to verify linearizability of sophisticated fine-grained concurrent data structures.

Findings

Successfully verified 11 complex concurrent data structures

Applied methods to challenging structures like Herlihy-Wing queue and lazy list

Methods are intuitive and easy for designers to adopt

Abstract

Lipton's reduction theory provides an intuitive and simple way for deducing the non-interference properties of concurrent programs, but it is difficult to directly apply the technique to verify linearizability of sophisticated fine-grained concurrent data structures. In this paper, we propose three reduction-based proof methods that can handle such data structures. The key idea behind our reduction methods is that an irreducible operation can be viewed as an atomic operation at a higher level of abstraction. This allows us to focus on the reduction properties of an operation related to its abstract semantics. We have successfully applied the methods to verify 11 concurrent data structures including the most challenging ones: the Herlihy and Wing queue, the HSY elimination-based stack, and the time-stamped queue, and the lazy list. Our methods inherit intuition and simplicity of Lipton's reduction, and concurrent data structures designers can easily and quickly learn to use the methods.