Repeated snapshots in distributed systems with synchronous communications and their implementation in CSP

AbstractA new version of the Snapshot Algorithm of Chandy and Lamport (1985) is presented. It considers synchronous communications and partially ordered semantics and allows for repeated snapshots. Its implementation in the language CSP is described: it is symmetric, generic and bounded in storage. It yields a symmetric and generic solution to the ‘Distributed Termination Detection’ problem of Francez