Visibility Reasoning for Concurrent Snapshot Algorithms

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 into components of increasing level of abstraction, using type-theoretic notions of signatures and functors (i.e., dependent $\Sigma$ and $\Pi$ types) as interfaces. The proofs are modular because 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.