Marker receiving rule for process pj On receiving a marker along channel C: if p j has not recorded its state then Record the state of C as the empty set Execute the “marker sending rule” else Record the state of C as the set of messages received along C after p j , s state was recorded and before p j received the marker along C Correctness • To prove the correctness of the algorithm, it is shown that a recorded snapshot satisfies
conditions C1 and C2.
• Since a process records its snapshot when it receives the first marker on any incoming
channel, no messages that follow markers on the channels incoming to it are recorded
in the process’s snapshot.
• Moreover, a process stops recording the state of an incoming channel when a marker is
received on that channel.
• Due to FIFO property of channels, it follows that no message sent after the marker on
that channel is recorded in the channel state. Thus, condition C2 is satisfied.
• When a process p
receives message m
that precedes the marker on channel C
, it acts
• If process p
has not taken its snapshot yet, then it includes m
in its recorded snapshot.
Otherwise, it records m
in the state of the channel C
. Thus, condition C1 is satisfied.
Complexity • The recording part of a single instance of the algorithm requires O(e) messages and
O(d) time, where e is the number of edges in the network and d is the diameter of the