Visibility Reasoning for Concurrent Snapshot Algorithms

TL;DR

This paper leverages visibility relations to create modular, reusable proofs for concurrent snapshot algorithms, enhancing understanding and formal verification of their correctness.

Contribution

It introduces a modular proof framework using visibility relations for multiple concurrent snapshot algorithms, capturing their core properties formally.

Findings

Proof components are shared across algorithms

Visibility relations effectively formalize intuitive properties

Framework improves modularity and reusability of proofs

Abstract

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.