previous up next
Go backward to B.4 State Program
Go up to B Distributed Snapshots
RISC-Linz logo

B.5 Verification

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 [6]. 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.

  • Correctness Theorem
  • Invariants
  • Program Properties
  • Termination
  • Time Complexity

  • Maintainer: Wolfgang Schreiner
    Last Modification: October 1, 1998

    previous up next