On Register Linearizability and Termination
On Register Linearizability and Termination
复制标题
寄存器线性化和终止
DOI：
10.1145/3465084.3467925
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
S. Toueg
中科院分区：
文献类型：
--
作者：
V. Hadzilacos;Xing Hu;S. Toueg
众所周知，对于确定性算法，可线性化的对象可以像原子对象一样使用。然而，正如Golab、希格姆和Woelfel所指出的，如果我们用只能线性化的对象替换原子对象，那么一个使用原子对象的随机算法可能会失去一些属性。目前还不知道可能丢失的属性是否包括终止的所有重要属性（概率为1）。在本文中，我们首先表明，一个随机算法确实可以失去其终止属性，如果我们取代原子寄存器，它使用线性化的。Golab等人还引入了强线性化，并证明了强线性化对象可以像原子对象一样使用，即使是随机算法：它们可以替换原子对象，同时保持算法的正确性，包括终止性。不幸的是，在一些重要的情况下，不可能实现强线性化。特别地，Helmi、希格姆和Woelfel展示了一大类“非平凡”对象，包括MWMR寄存器，不具有来自SWMR寄存器的强线性化实现。因此，我们提出了一种新类型的寄存器线性化，称为写强线性化，这是严格强于（平原）线性化，但严格弱于强线性化。这种中间类型的线性化具有一些期望的性质。我们证明了一些随机算法，未能终止与线性化寄存器，工作与写强线性化的。换句话说，存在可线性化性不足但可写入强线性化性的情况。与上述不可能性结果相反，我们证明了写强线性化MWMR寄存器是可以从SWMR寄存器实现的。而著名的ABD实现的SWMR寄存器在消息传递系统是不是强线性化，我们表明，它实际上是写强线性化。事实上，我们证明，任何线性实现的SWMR寄存器必须写强线性化，但这不是MWMR寄存器的情况。
It is well-known that, for deterministic algorithms, linearizable objects can be used as if they were atomic objects. As pointed out by Golab, Higham, and Woelfel, however, a randomized algorithm that works with atomic objects may lose some of its properties if we replace the atomic objects that it uses with objects that are only linearizable. It was not known whether the properties that can be lost include the all-important property of termination (with probability 1). In this paper, we first show that a randomized algorithm can indeed lose its termination property if we replace the atomic registers that it uses with linearizable ones. Golab et al. also introduced strong linearizability, and proved that strongly linearizable objects can be used as if they were atomic objects, even for randomized algorithms: they can replace atomic objects while preserving the algorithm's correctness properties, including termination. Unfortunately, there are important cases where strong linearizability is impossible to achieve. In particular, Helmi, Higham, and Woelfel showed a large class of "non-trivial'' objects, including MWMR registers, do not have strongly linearizable implementations from SWMR registers. Thus we propose a new type of register linearizability, called write strong-linearizability, that is strictly stronger than (plain) linearizability but strictly weaker than strong linearizability. This intermediate type of linearizability has some desirable properties. We prove that some randomized algorithms that fail to terminate with linearizable registers, work with write strongly-linearizable ones. In other words, there are cases where linearizability is not sufficient but write strong-linearizability is. In contrast to the impossibility result mentioned above, we prove that write strongly-linearizable MWMR registers are implementable from SWMR registers. While the well-known ABD implementation of SWMR registers in message-passing system is not strongly linearizable, we show that it is actually write strongly-linearizable. In fact, we prove that any linearizable implementation of SWMR registers is necessarily write strongly-linearizable, but that this is not case for MWMR registers.