Consistency as a Branching Time Notion

Superposed on a distributed computation, a snapshot algorithm computes a global state, the so-called snapshot, consistent with the underlying computation. On intuive grounds it can be argued that the snapshot is a global state which would have been obtained when processes would have been frozen at the time their local states were recorded (their checkpoints). This interpretation is stronger than consistency as it also considers the nondeterministic behaviour of processes up to their checkpoints. In this paper, we provide a formal setup to study the latter interpretation. In particular, we introduce the notion of a freeze bisimulation which allows us to express the above intuition formally as progressive bi-consistency. This definition does not only capture branching time behaviour but also applies to snapshot algorithms that compute a partial snaphshot and of which the intermediate behaviour is of equal interest as the final snapshot (eg in case of approximations or eventual consistency). We establish fundamental properties of progressive bi-consistency which includes a theorem similar to the CAP theorem for distributed databases: it is impossible to have a partial snapshot algorithm which computes a minimal number of checkpoints, is progressively bi-consistent and non-inhibiting at the same time. We illustrate our results by evaluating snapshot algorithms modelled in Milner's process algebra CCS. This includes the seminal algorithms by Chand/Lamport [9] and Lai/Yang [14] and a recent snapshot algorithm for data stream processing systems [8].