A Forward Simulation-Based Hierarchy of Linearizable 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. Thus, forward simulation is not only a proof technique for linearizability but also induces an algebraic hierarchy of linearizable objects. 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 w.r.t. an object ${\mathcal{U}}_{Spec}$.