Substep linearizability eases reasoning about concurrent operations without full atomicity
Substep Linearizability: Relaxing Atomicity While Preserving Sequential Specification
Distributed, Parallel, and Cluster Computing
Summary
When multiple computer programs try to use shared data at the same time, it's hard to make sure they do it correctly. Standard rules require each step to happen all at once, which is sometimes impossible for certain operations. The authors created a new way, called substep linearizability, that relaxes this rule while still keeping things logically consistent. This new method is easier to understand and specify for complex operations, like certain data exchanges and database transactions, making it simpler to build reliable concurrent systems.
What this means in practice
- •For software engineers: Specify and verify concurrency behaviors in complex data structures that cannot be atomically linearized, enabling safer concurrent designs.
- •For database developers: Model and reason about snapshot isolation in transaction management with simplified sequential specifications to improve concurrency control.
Authors
Finn Hackett, Evan Wrench, Ivan Beschastnikh, Yuanhao Wei
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.