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
j
receives message m
ij
that precedes the marker on channel C
ij
, it acts
as follows:
• If process p
j
has not taken its snapshot yet, then it includes m
ij
in its recorded snapshot.
Otherwise, it records m
ij
in the
state of the channel C
ij
. 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
network.
