A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909993128689664 |
|---|---|
| author | Wang, Chao Li, Ruijia Zhou, Yang Wu, Peng Lv, Yi Liao, Jianwei Woodcock, Jim Liu, Zhiming |
| author_facet | Wang, Chao Li, Ruijia Zhou, Yang Wu, Peng Lv, Yi Liao, Jianwei Woodcock, Jim Liu, Zhiming |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_11646 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects Wang, Chao Li, Ruijia Zhou, Yang Wu, Peng Lv, Yi Liao, Jianwei Woodcock, Jim Liu, Zhiming Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory 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. |
| title | A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects |
| topic | Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2601.11646 |