Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points. However, relying on linearization points leads to proofs that are implementation-dependent, and thus hinder abstraction and reuse. In this paper we show that one can develop more declarative proofs by foregoing linearization points and instead relying on a technique of axiomatization of visibility relations. While visibility relations have been considered before, ours is the first study where the challenge is to formalize the helping nature of the algorithms. In particular, we show that by axiomatizing the properties of separation between events that contain bunches of help requests, we can extract what is common for high-level understanding of several descriptor-based helping algorithms of Harris et al. (RDCSS, MCAS, and optimizations), and produce novel proofs of their linearizability that share significant components.

翻译：线性化是并发算法的标准正确性准则，通常通过建立算法的线性化点来证明。然而，依赖线性化点会导致与具体实现紧密耦合的证明，从而阻碍抽象与复用。本文表明，通过摒弃线性化点转而采用可见性关系的公理化技术，可以发展出更具声明性的证明。尽管可见性关系此前已有研究，但我们的工作是首次处理算法辅助性形式化挑战的探索。具体而言，通过将包含大量辅助请求的事件分离特性加以公理化，我们能够提取Harris等人提出的多种基于描述符的辅助算法（RDCSS、MCAS及其优化）的高层理解共性，并为其线性化生成共享关键组件的全新证明。