Simple Executions of Snapshot Implementations

TL;DR

This paper introduces a mathematical formulation for verifying snapshot algorithms' correctness and identifies a property called schedule-basedness, simplifying the verification process for these concurrent algorithms.

Contribution

It provides a new formulation of linearizability for snapshot algorithms and introduces schedule-based algorithms, reducing the complexity of correctness proofs.

Findings

Linearizability can be characterized by specific mathematical functions.

Most published snapshot algorithms are schedule-based.

Focusing on schedule-based algorithms simplifies correctness verification.

Abstract

The well known snapshot primitive in concurrent programming allows for n-asynchronous processes to write values to an array of single-writer registers and, for each process, to take a snapshot of these registers. In this paper we provide a formulation of the well known linearizability condition for snapshot algorithms in terms of the existence of certain mathematical functions. In addition, we identify a simplifying property of snapshot implementations we call "schedule-based algorithms". This property is natural to assume in the sense that as far as we know, every published snapshot algorithm is schedule-based. Based on this, we prove that when dealing with schedule-based algorithms, it suffices to consider only a small class of very simple executions to prove or disprove correctness in terms of linearizability. We believe that the ideas developed in this paper may help to design automatic verification of snapshot algorithms. Since verifying linearizability was recently proved to be EXPSPACE-complete, focusing on unique objects (snapshot in our case) can potentially lead to designing restricted, but feasible verification methods.