Go backward to B.4 State Program
Go up to B Distributed Snapshots
We will prove the correctness of the program shown above; this is not a proof of the Chandy-Lamport algorithm that solves a much more general problem . However, by focusing on our application, the proof becomes more concrete and its relationship to the program more direct.
In this section, we wil use the following typed variables:
m a message c a channel, identified with the array of messages in it i,j indices of network nodes k an index of a message in c, 0 <=k < c.length h an index of a channel in a set s, 0 <=k < s.getSize()
Furthermore, we will denote by di >= 0 the initial value of depositi and by n the number of nodes in the network.