A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects

TL;DR

This paper explores the relationship between linearizable concurrent objects and forward simulation, establishing a lattice structure and providing a new verification method for linearizability based on forward simulation.

Contribution

It introduces a lattice framework for linearizable objects under forward simulation and reduces linearizability checking to forward simulation verification.

Findings

Linearizable objects form a bounded join-semilattice under forward simulation.

Linearizability can be characterized by checking forward simulation with a specific object.

The paper demonstrates simulation relations between various concurrent queue implementations.

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.