用可线性化实现钝化随机并发程序的附加程序
Blunting an Adversary Against Randomized Concurrent Programs with Linearizable Implementations
摘要：
原子共享对象是设计复杂并发程序的一个强大的抽象，它的操作是即时发生的。由于它们并不总是可用的，它们通常被软件实现所取代。将这些实现与它们的原子规范联系起来的一个突出条件是可线性化性，它保留了使用它们的程序的安全属性。然而，线性化并不保留超属性，其中包括随机化程序的概率保证：对手可以大大放大坏结果的概率。这种不受欢迎的行为会妨碍模块化推理，而模块化推理正是使用可线性化对象实现所带来的主要好处。一个更严格的性质，强线性化，确实保持了超性质，但在许多情况下不可能实现。本文提出了一种新的方法来钝化对手的额外的权力，即使在强线性化是无法实现的情况下。我们表明，广泛的一类线性化的实现，包括众所周知的寄存器和快照，可以修改，以近似的概率保证随机程序时，使用原子对象。技术方法是通过重复仔细选择的方法的前缀若干次并且然后随机选择随后使用哪个重复来变换现有可线性化实现的每个方法的算法。我们证明了一个坏的结果的概率随着重复次数的减少，接近使用原子对象时达到的概率。我们的转换应用的实现类包括使用消息传递的共享寄存器的ABD实现和Afek等人使用单写入寄存器的原子快照实现。
英文摘要：
Atomic shared objects, whose operations take place instantaneously, are a powerful abstraction for designing complex concurrent programs. Since they are not always available, they are typically substituted with software implementations. A prominent condition relating these implementations to their atomic specifications is linearizability, which preserves safety properties of the programs using them. However linearizability does not preserve hyper-properties, which include probabilistic guarantees of randomized programs: an adversary can greatly amplify the probability of a bad outcome. This unwelcome behavior prevents modular reasoning, which is the key benefit provided by the use of linearizable object implementations. A more restrictive property, strong linearizability, does preserve hyper-properties but it is impossible to achieve in many situations. This paper suggests a novel approach to blunting the adversary's additional power that works even in cases where strong linearizability is not achievable. We show that a wide class of linearizable implementations, including well-known ones for registers and snapshots, can be modified to approximate the probabilistic guarantees of randomized programs when using atomic objects. The technical approach is to transform the algorithm of each method of an existing linearizable implementation by repeating a carefully chosen prefix of the method several times and then randomly choosing which repetition to use subsequently. We prove that the probability of a bad outcome decreases with the number of repetitions, approaching the probability attained when using atomic objects. The class of implementations to which our transformation applies includes the ABD implementation of a shared register using message-passing and the Afek et al. implementation of an atomic snapshot using single-writer registers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
