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）来证明。然而，线性化点常阻碍抽象，并且对于某些算法（如时间戳栈）而言，甚至不清楚如何识别其线性化点。本文展示了如何通过摒弃线性化点，转而采用所谓可见性关系的公理化方法，来开发线性化的可声明证明。尽管可见性关系此前已被用于时间戳栈，但本研究首次展示了如何系统且直观地从栈的顺序规约中推导出公理化方法。除了可见性关系之外，一种新颖的可分离性关系随之出现，用于泛化过程调用的实时优先关系。可见性与可分离性关系对时间戳栈具有自然的定义，并催生了一种新颖的证明方法，该方法将算法简化为一种简化形式，其中时间戳以原子方式生成。