削弱对手对具有线性化实现的随机并发程序的攻击能力

原子共享对象其操作瞬时发生，是设计复杂并发程序的强大抽象。由于它们并非总可用，通常用软件实现来替代。将这些实现与其原子规范关联的一个显著条件是线性化（linearizability），它保留了使用它们的程序的安全性质。然而线性化不保留超性质（hyper-properties），其中包括随机程序的概率保证：对手可大幅放大坏结果的概率。这种不受欢迎的行为阻碍了模块化推理，而模块化推理正是使用线性化对象实现所提供的关键益处。更具限制性的性质——强线性化（strong linearizability）——确实保留超性质，但在许多情况下无法实现。本文提出了一种削弱对手额外能力的新方法，即便在强线性化不可实现的情况下也有效。我们表明，广泛的线性化实现类，包括著名的寄存器和快照实现，可被修改以在使用原子对象时逼近随机程序的概率保证。技术途径是变换现有线性化实现的每个方法之算法，通过多次重复该方法精心选择的前缀，然后随机选取后续使用的重复。我们证明坏结果的概率随重复次数增加而下降，逼近使用原子对象时所达到的概率。我们的变换所适用的实现类包括使用消息传递的 ABD 共享寄存器实现，以及使用单写者寄存器的 Afek 等人原子快照实现。