Strongly Linearizable Implementations of Snapshots and Other Types
Strongly Linearizable Implementations of Snapshots and Other Types
复制标题
快照和其他类型的强线性化实现
DOI：
10.1145/3293611.3331632
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Philipp Woelfel
中科院分区：
文献类型：
--
作者：
Sean Ovens;Philipp Woelfel
线性化是共享内存算法正确性条件的黄金标准，历史上被认为是原子性的实际等价物。然而，已经表明，用可线性化的实现替换原子对象会影响随机算法中执行结果的概率分布。因此，可线性化对象并不总是原子对象的合适替代品。一个更严格的正确性条件，称为强线性化，已经被开发出来，并证明是适合于随机算法在一个强自适应对手模型[16]。我们设计了几个新的无锁强线性化的原子寄存器的实现。特别是，我们给出了第一个强线性化的无锁快照实现，使用有界空间。这改进了Denysyuk和Woelfel[14]的无界空间解。作为一个构建块，我们的算法使用一个无锁的强线性化的ABA检测寄存器。我们通过修改Aghazadeh和Woelfel [5]的无等待线性化ABA检测寄存器来实现这个目标，正如我们所示，它不是强线性化的。Aspnes和Herlihy[8]确定了一类具有无等待线性化实现的类型。这些类型要求任何一对操作要么可交换，要么一个覆盖另一个。Aspnes和Herlihy使用原子快照对象给出了此类类型的一般无等待线性化实现。我们证明了这种实现是强线性化的，证明了这个类中的所有类型都有一个无锁的强线性化实现原子寄存器。
Linearizability is the gold standard of correctness conditions for shared memory algorithms, and historically has been considered the practical equivalent of atomicity. However, it has been shown that replacing atomic objects with linearizable implementations can affect the probability distribution of execution outcomes in randomized algorithms. Thus, linearizable objects are not always suitable replacements for atomic objects. A stricter correctness condition called strong linearizability has been developed and shown to be appropriate for randomized algorithms in a strong adaptive adversary model[16]. We devise several new lock-free strongly linearizable implementations from atomic registers. In particular, we give the first strongly linearizable lock-free snapshot implementation that uses bounded space. This improves on the unbounded space solution of Denysyuk and Woelfel[14]. As a building block, our algorithm uses a lock-free strongly linearizable ABA-detecting register. We obtain this object by modifying the wait-free linearizable ABA-detecting register of Aghazadeh and Woelfel [5], which, as we show, is not strongly linearizable. Aspnes and Herlihy[8] identified a wide class of types that have wait-free linearizable implementations. These types require that any pair of operations either commute, or one overwrites the other. Aspnes and Herlihy gave a general wait-free linearizable implementation of such types, employing an atomic snapshot object. We show that this implementation is strongly linearizable, proving that all types in this class have a lock-free strongly linearizable implementation from atomic registers.