  Visibility relations have been proposed by Henzinger et al. as an abstraction
for proving linearizability of concurrent algorithms that obtains modular and
reusable proofs. This is in contrast to the customary approach based on
exhibiting the algorithm's linearization points. In this paper we apply
visibility relations to develop modular proofs for three elegant concurrent
snapshot algorithms of Jayanti. The proofs are divided by signatures into
components of increasing level of abstraction; the components at higher
abstraction levels are shared, i.e., they apply to all three algorithms
simultaneously. Importantly, the interface properties mathematically capture
Jayanti's original intuitions that have previously been given only informally.
