Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification

Abstract

Linearizability is a standard correctness condition for concurrent objects. It takes a correct by construction sequential specification of a concurrent data structure, and produces a composable specification under atomic interleavings of operations. However, some operations like atomic exchangers are not specifiable atomically, making it difficult to reason compositionally about their specifications. Interval linearizability is the state of the art in relaxing linearizability's constraints. Formally it is a powerful framework, but it requires an interval-sequential specification of the target data structure, which we show is challenging to correctly generate or understand, even for simple operations on a single concurrent register. We propose substep linearizability, which we show is equivalent to interval linearizability using X-CCorrectness, a relaxed concurrency framework we created to compare existing linearizability semantics. We show that substep linearizability's sequential specifications are suitable for previously infeasible specification tasks, while being comparable in complexity to linearizability's sequential specifications. For evaluation, we model an atomic exchanger, a popular non-linearizable queue structure, and snapshot isolation between database transactions.