面向方面的可线性化证明

并发数据结构的可线性化通常通过依赖于识别所谓线性化点的整体模拟论证来证明。遗憾的是，此类证明无论是手动还是自动，往往都很复杂，并且难以扩展到高级的非阻塞并发模式，例如帮助机制和乐观更新。作为回应，我们提出了一种更模块化的方法来检查并发队列算法的可线性化，该方法不涉及识别线性化点。我们将针对队列规范证明可线性化的任务简化为建立四个基本性质，每个性质都可以通过更简单的论证独立证明。作为我们方法的演示，我们验证了 Herlihy and Wing 队列，这是一种通过模拟证明难以验证的算法。