Linearizable implementations do not suffice for randomized distributed computation
Linearizable implementations do not suffice for randomized distributed computation
复制标题
线性化实现不足以满足随机分布式计算
DOI：
10.1145/1993636.1993687
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Philipp Woelfel
中科院分区：
文献类型：
--
作者：
W. Golab;Lisa Higham;Philipp Woelfel
线性化是算法设计者的黄金标准，用于从使用相同对象的原子版本的相应算法的正确性推断使用实现的共享对象的分布式算法的正确性。我们表明，线性化不足以达到这个目的时，过程可以利用随机化，我们讨论了存在的替代正确性条件。本文的主要贡献如下：1.各种示例表明，使用对象的公知的可线性化实现（例如，快照）代替原子对象可以改变对手能够生成的结果的概率分布。在某些情况下，一个不经意的对手可以创建一个概率分布的结果与实现的算法，线性化的对象，甚至没有一个强大的对手可以生成相同的算法与原子对象。2.定义了一个新的共享对象实现的正确性条件，称为强不可实现性。我们证明，一个强大的对手（即，立即看到每次抛硬币的结果的人）在原子对象被强线性化实现替换时没有获得额外的能力。一般来说，没有严格较弱的正确性条件足以确保这一点。我们还表明，强线性化是一个本地的和可组合的属性。3.相反的情况下，强大的对手，一个自然较弱的对手（一个不能看到一个进程的抛硬币，直到其下一个操作的共享对象），我们证明，没有相应的一般正确性条件。具体地说，任何可线性化的计数器实现都称为终止。来自原子寄存器和加载链接/存储条件对象的、满足自然局部性属性的计数器，必然给予较弱的对手比原子计数器更大的能力。
Linearizability is the gold standard among algorithm designers for deducing the correctness of a distributed algorithm using implemented shared objects from the correctness of the corresponding algorithm using atomic versions of the same objects. We show that linearizability does not suffice for this purpose when processes can exploit randomization, and we discuss the existence of alternative correctness conditions. This paper makes the following contributions: 1. Various examples demonstrate that using well-known linearizable implementations of objects (e.g., snapshots) in place of atomic objects can change the probability distribution of the outcomes that the adversary is able to generate. In some cases, an oblivious adversary can create a probability distribution of outcomes for an algorithm with implemented, linearizable objects, that not even a strong adversary can generate for the same algorithm with atomic objects. 2. A new correctness condition for shared object implementations, called strong inearizability, is defined. We prove that a strong adversary (i.e., one that sees the outcome of each coin flip immediately) gains no additional power when atomic objects are replaced by strongly linearizable implementations. In general, no strictly weaker correctness condition suffices to ensure this. We also show that strong linearizability is a local and composable property. 3. In contrast to the situation for the strong adversary, for a natural weaker adversary (one that cannot see a process' coin flip until its next operation on a shared object) we prove that there is no correspondingly general correctness condition. Specifically, any linearizable implementation of counters called terminating. from atomic registers and load-linked/store-conditional objects, that satisfies a natural locality property, necessarily gives the weak adversary more power than it has with atomic counters.