A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects
Chao Wang, Ruijia Li, Yang Zhou, Peng Wu, Yi Lv, Jianwei Liao, Jim Woodcock, Zhiming Liu
TL;DR
The paper investigates the structural relationship between linearizable concurrent objects and forward simulation, revealing that sets of linearizable objects with liveness constraints form a bounded join-semilattice, while the unconstrained case forms a bounded lattice. It introduces a universal forward-simulation object $\mathcal{U}_{Spec}$ and proves an equivalent characterization of linearizability: $\llbracket \mathcal{O},n \rrbracket \preceq_{(c,r)} \llbracket \mathcal{U}_{Spec},n \rrbracket$ iff $\mathcal{O}$ is linearizable w.r.t. $Spec$ for $n$ processes, enabling verification via forward simulation. The framework defines least upper bounds and greatest lower bounds (LUB/GLB) across classes, and locates strongly linearizable objects within the semilattice, showing they reside at the maximal or minimal elements corresponding to the canonical universal constructions. Case studies demonstrate concrete connections: the time-stamped queue simulates the Herlihy-Wing queue, and HWQ is simulated by $\mathcal{U}_{Queue}$, illustrating practical verification pathways. These results provide a principled, lattice-based approach to understanding and verifying linearizability across diverse concurrent objects.
Abstract
In this paper, we systematically investigate the connection between linearizable objects and forward simulation. We prove that the sets of linearizable objects satisfying wait-freedom (resp., lock-freedom or obstruction-freedom) form a bounded join-semilattice under the forward simulation relation, and that the sets of linearizable objects without liveness constraints form a bounded lattice under the same relation. As part of our lattice result, we propose an equivalent characterization of linearizability by reducing checking linearizability w.r.t. sequential specification $Spec$ into checking forward simulation by an object $\mathcal{U}_{Spec}$. To demonstrate the forward simulation relation between linearizable objects, we prove that the objects that are strongly linearizable w.r.t. the same sequential specification and are wait-free (resp., lock-free, obstruction-free) simulate each other, and we prove that the time-stamped queue simulates the Herlihy-Wing queue. We also prove that the Herlihy-Wing queue is simulated by $\mathcal{U}_{Spec}$, and thus, our equivalent characterization of linearizability can be used in the verification of linearizability.