Blunting an Adversary Against Randomized Concurrent Programs with Linearizable Implementations
Blunting an Adversary Against Randomized Concurrent Programs with Linearizable Implementations
复制标题
通过可线性化的实现来削弱对手对抗随机并发程序的能力
DOI：
10.1145/3519270.3538446
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Welch, Jennifer
中科院分区：
文献类型：
--
作者：
Attiya, Hagit;Enea, Constantin;Welch, Jennifer
原子共享对象的操作即时发生，是设计复杂并发程序的强大抽象。因为它们并不总是可用的，所以它们通常被软件实现所取代。将这些实现与它们的原子规范相关联的一个突出条件是可线性化，它保留了使用它们的程序的安全属性。然而，线性化并不保留超性质，其中包括随机化程序的概率保证：对手可以通过操纵操作实现中的事件顺序来极大地放大坏结果的概率，例如不终止。这种不受欢迎的行为阻止了模块化推理，而模块化推理是使用可线性化对象实现所提供的主要好处。一种更具限制性的性质，即强线性化，确实保持了超性质，但在许多情况下是不可能实现的。这篇论文提出了一种新的方法来钝化对手的额外力量，即使在无法实现强线性化的情况下也能发挥作用。我们证明了一大类可线性化的实现，包括众所周知的用于寄存器和快照的实现，可以被修改以接近使用原子对象时随机程序的概率保证。技术方法是通过多次重复精心选择的操作前缀，然后随机选择随后要使用的重复，来转换现有可线性化实现的每个操作的算法。我们证明了坏结果的概率随着重复次数的增加而减小，接近使用原子对象时所获得的概率。我们的转换适用的实现类包括使用消息传递的共享寄存器的ABD实现，Afek等人。使用单写入器寄存器实现原子快照，Vitanyi和Awerbuch使用单写入器寄存器实现多写入器寄存器，以色列和LI使用单读取器寄存器实现多读取器寄存器，所有这些都广泛用于易崩溃的异步系统。
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, such as nontermination, by manipulating the order of events inside the implementations of the operations. 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 approach the probabilistic guarantees of randomized programs when using atomic objects. The technical approach is to transform the algorithm of each operation of an existing linearizable implementation by repeating a carefully chosen prefix of the operation 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, the Afek et al. implementation of an atomic snapshot using single-writer registers, the Vitanyi and Awerbuch implementation of a multi-writer register using single-writer registers, and the Israeli and Li implementation of a multi-reader register using single-reader registers, all of which are widely used in asynchronous crash-prone systems.
登录
查看更多内容
DOI：
10.1145/3293611.3331632
发表时间：
2019
期刊：
Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing
影响因子：
--
作者：
Sean Ovens;Philipp Woelfel
通讯作者：
Philipp Woelfel
异步硬件的原子共享寄存器访问
DOI：
10.1109/sfcs.1986.11
发表时间：
1986
期刊：
27th Annual Symposium on Foundations of Computer Science (sfcs 1986)
影响因子：
--
作者：
P. Vitányi;B. Awerbuch
通讯作者：
B. Awerbuch
DOI：
10.1145/2332432.2332508
发表时间：
2012
期刊：
Proceedings of IEEE 27th International Symposium on Fault Tolerant Computing
影响因子：
--
作者：
Maryam Helmi;Lisa Higham;Philipp Woelfel
通讯作者：
Philipp Woelfel
线性化实现不足以满足随机分布式计算
DOI：
10.1145/1993636.1993687
发表时间：
2011
期刊：
ArXiv
影响因子：
--
作者：
W. Golab;Lisa Higham;Philipp Woelfel
通讯作者：
Philipp Woelfel
DOI：
10.1145/3465084.3467925
发表时间：
2021
期刊：
Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing
影响因子：
--
作者：
V. Hadzilacos;Xing Hu;S. Toueg
通讯作者：
S. Toueg