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.

翻译：本文系统性地研究了可线性化对象与前向模拟之间的联系。我们证明了满足无等待性（相应地，无锁性或无障碍性）的可线性化对象集合在前向模拟关系下构成一个有界并半格，且无活性约束的可线性化对象集合在同一关系下构成一个有界格。作为格结构结论的一部分，我们通过将相对于顺序规约$Spec$的可线性化性检验归约为对象$\mathcal{U}_{Spec}$的前向模拟检验，提出了可线性化性的等价刻画。为展示可线性化对象间的前向模拟关系，我们证明了相对于同一顺序规约强可线性化且满足无等待性（相应地，无锁性、无障碍性）的对象可相互模拟，并证明了时间戳队列可模拟Herlihy-Wing队列。我们还证明了Herlihy-Wing队列可被$\mathcal{U}_{Spec}$模拟，因此我们的可线性化性等价刻画可用于可线性化性验证。