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并采用所谓可见性关系的公理化方法，来发展声明式的线性化证明。尽管先前已有人针对时间戳栈研究过可见性关系，但我们的研究首次展示了如何系统且直观地从栈的顺序规约中推导出公理化方法。除了可见性关系之外，一种新颖的可分离性关系也随之出现，用于泛化过程调用的实时优先顺序。可见性和可分离性关系为时间戳栈提供了自然的定义，并促成了一种新颖的证明方法，即将算法简化为一种时间戳原子生成的精简形式。