  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.
