Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder abstraction, and for some algorithms such as the timestamped stack, it is unclear how to even identify their LPs. In this paper, we show how to develop declarative proofs of linearizability by foregoing LPs and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for the timestamped stack, our study is the first to show how to derive the axiomatization systematically and intuitively from the sequential specification of the stack. In addition to the visibility relation, a novel separability relation emerges to generalize real-time precedence of procedure invocation. The visibility and separability relations have natural definitions for the timestamped stack, and enable a novel proof that reduces the algorithm to a simplified form where the timestamps are generated atomically.

翻译：线性化是并发算法的标准正确性准则，通常通过确立算法的线性化点（LP）来证明。然而，LP往往阻碍抽象化，且对于某些算法（如时间戳栈）而言，甚至难以明确识别其LP。本文展示如何通过摒弃LP并采用所谓可视关系的公理化方法，来开发线性化的声明式证明。尽管时间戳栈的可视关系此前已有研究，但本文首次系统性地展示了如何从栈的顺序规约中直观推导出其公理化体系。除可视关系外，一种新颖的可分性关系随之出现，用于泛化过程调用的实时优先顺序。可视关系与可分性关系对时间戳栈具有天然的定义，并催生了一种新颖的证明方法——将算法简化为时间戳原子生成的形式。