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
AI总结 本文通过前向模拟关系系统研究可线性化对象,证明满足不同活性条件的可线性化对象集合形成有界半格或格,并提出了基于前向模拟的等价刻画和通用构造,用于验证可线性化性。
详情
本文系统研究了可线性化对象与前向模拟之间的联系。我们证明,满足无等待(resp.,无锁或无阻塞)的可线性化对象集合在前向模拟关系下形成有界并半格,而无活性约束的可线性化对象集合在同一关系下形成有界格。因此,前向模拟不仅是可线性化性的证明技术,还诱导了可线性化对象的代数层次结构。作为格结果的一部分,我们通过将关于顺序规范$Spec$的可线性化性检查归约为关于无等待通用构造$\mathcal{U}_{Spec}^{WF}$的前向模拟检查,提出了可线性化性的等价刻画。我们还提出了对象$\mathcal{U}_{Spec}^s$,它简化了$\mathcal{U}_{Spec}^{WF}$,更适合验证。我们证明Herlihy-Wing队列被$\mathcal{U}_{Queue}^s$模拟,其中$Queue$是队列的顺序规范。因此,我们的对象$\mathcal{U}_{Spec}^s$可用于可线性化性的验证。为了展示具体可线性化对象之间的前向模拟关系,我们证明时间戳队列模拟Herlihy-Wing队列,而Herlihy-Wing队列不能模拟时间戳队列。这三个证明均已通过Isabelle/HOL机器验证。
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. a wait-free universal construction $\mathcal{U}_{Spec}^{WF}$. We also propose an object $\mathcal{U}_{Spec}^s$, which simplifies $\mathcal{U}_{Spec}^{WF}$ and is more suitable for verification. We prove that the Herlihy-Wing queue is simulated by $\mathcal{U}_{Queue}^s$ with $Queue$ the sequential specification of the queue. Thus, our object $\mathcal{U}_{Spec}^s$ can be used in the verification of linearizability. To demonstrate the forward simulation relation between concrete linearizable objects, we prove that the time-stamped queue simulates the Herlihy-Wing queue, while the Herlihy-Wing queue cannot simulate the time-stamped queue. All these three proofs have been machine-verified by Isabelle/HOL.