Communication-based prevention of useless checkpoints in distributed computations.
A useless checkpoint is a local checkpoint that cannot be part of a consistent global checkpoint. This paper addresses the following problem. Given a set of processes that take (basic) local checkpoints in an independent and unknown way, the problem is to design communication-induced checkpointing protocols that direct processes to take additional local (forced) checkpoints to ensure no local checkpoint is useless. The paper first proves two properties related to integer timestamps which are associated with each local checkpoint. The first property is a necessary and sufficient condition that these timestamps must satisfy for no checkpoint to be useless. The second property provides an easy timestamp-based determination of consistent global checkpoints. Then, a general communication-induced checkpointing protocol is proposed. This protocol, derived from the two previous properties, actually defines a family of timestamp-based communication-induced checkpointing protocols. It is shown that several existing checkpointing protocols for the same problem are particular instances of the general protocol. The design of this general protocol is motivated by the use of communication-induced checkpointing protocols in "consistent global checkpoint"-based distributed applications such as the detection of stable or unstable properties and the determination of distributed breakpoints.
Introduction
A local checkpoint is a snapshot of a local state of a process, a global checkpoint is a set of local
checkpoints, one from each process, and a consistent global checkpoint is a global checkpoint such
that no message sent by a process after its local checkpoint is received by another process before its
local checkpoint. So, the consistency of global checkpoints strongly depends on the flow of messages
exchanged by processes. The determination of consistent global checkpoints is a fundamental problem
in distributed computing and arise in many applications such as detection of stable properties [5, 12,
17], determination of breakpoints [7, 10, 20], detection of unstable properties [2, 6, 11, 13], rollback
recovery upon failure occurences [8, 14, 22], etc.
When processes independently take their local checkpoints there is a risk that no consistent global
checkpoint can ever be formed (except the first one composed of their initial states). This is caused
by the well-known unbounded domino effect [22]. Even if consistent global checkpoints can be formed,
it is still possible that some local checkpoints can never be included in a consistent global checkpoint;
such local checkpoints are called useless.
To prevent useless checkpoints, and thus safely prevent the domino effect, some coordination in
the taking of local checkpoints is required. In the family of coordinated protocols [5, 15], processes use
additional control messages to synchronize their checkpointing activities. This additional synchronization
may result in reduced process autonomy and degraded performance of the underlying application.
These drawbacks have given rise to the development of a family of communication-induced checkpointing
protocols. In this family the coordination is achieved by piggybacking control information on
application messages: no control messages or synchronization is added to the application [8]. More
precisely, processes take local checkpoints independently 1 (called basic checkpoints) and the protocol
directs them to take additional local checkpoints (called forced checkpoints) to ensure that no local
checkpoint becomes useless. Taking a forced checkpoint before each message delivery is a safe strategy
to prevent useless checkpoints but is very inefficient. Given a set of basic checkpoints, the fewer the
forced checkpoints are taken by a communication-induced checkpointing protocol, the better the pro-
tocol. A process decides whether to take a forced checkpoint when a message is received by evaluating
a predicate. This predicate is based on local control variables of the receiving process and on control
values carried by the message. The local control variables managed by a process are a coding of the
causal dependencies appearing in its past. Distinct semantics for these control variables and distinct
definitions of the predicate give rise to different protocols [1, 3, 4, 14, 19, 23, 24, 26].
In this paper, we present a new communication-induced checkpointing protocol that takes as few
forced checkpoints as possible while ensuring no local checkpoint is useless. This protocol is based on
the Z-path (and Z-cycle) theory introduced by Netxer and Xu [21] who showed that a useless checkpoint
exactly corresponds to the existence of a Z-cycle in the distributed computation. At the model level,
our protocol prevents Z-cycles 2 . At the operational level, a sequence number and Lamport timestamp
are associated with each local checkpoint. Moreover, each message piggybacks an integer (Lamport
clock value), a vector of integers (checkpoint sequence numbers) and two boolean vectors (the size
of each vector is n, the number of processes). This protocol is more efficient 3 than past domino-free
communication-induced checkpointing protocols. An interesting feature of the proposed protocol is
the following one: for any local checkpoint A, there is a very easy determination of a consistent global
checkpoint to which A belongs. Moreover, the proposed protocol enjoys a nice genericity property:
if we reduce the size of its control information, or even eliminate some of it altogether, the protocol
1 For example, in the detection of unstable properties such as conjunctions of local predicates, each process takes a
basic checkpoint each time its local predicate becomes true [13].
2 So, in the Manivannan-Singhal's classification [18], this protocol belongs to the ZCF (Z-Cycle-Free) family.
3 When considering the number of forced local checkpoints taken by processes.
4 J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
reduces to already known protocols such as [1, 19, 23]. As a result, our protocol offers a very general
and efficient framework for a family of domino-free communication-induced checkpointing protocols.
The paper is divided into seven sections. Section 2 presents the model of distributed computations,
provides a definition for consistent global checkpoints, and defines Z-paths. Section 3 presents the
design principles of the protocol. Section 4 describes a first version of the protocol and proves its
main property, namely, given a local checkpoint C, there is an easy determination of a consistent
global checkpoint to which C belongs. Then Section 5 reduces the size of data structures used by the
protocol and presents an improved version of it. Finally, Section 6 discusses the protocol: it shows
that it reduces to existing protocols when reducing its control information. Section 7 concludes the
paper.
Distributed Computations, Checkpoints and Z-Paths
2.1 Distributed Computations
A distributed computation consists of a finite set P of n processes fP that communicate
and synchronize only by exchanging messages. We assume that each ordered pair of processes is
connected by an asynchronous, reliable, directed logical channel whose transmission delays are unpredictable
but finite. (Note that channels are not required to be fifo.) Each process runs on a different
processor, processors do not share a common memory, and there is no bound on their relative speeds.
Also, they fail according to the fail-stop model.
A process can execute internal, send 4 and delivery statements. An internal statement does not
involve communication. When P i executes the statement "send(m) to puts the message m into
the channel from P i to P j . When P i executes the statement "deliver(m)", it is blocked until at least
one message directed to P i has arrived, then a message is withdrawn from one of its input channels
and delivered to P i . Executions of internal, send and delivery statements are modeled by internal,
sending and delivery events.
Processes of a distributed computation are sequential; in other words, each process P i produces
a sequence of events e This sequence can be finite or infinite. Every process P i has an
initial local state denoted oe i;0 . The local state oe i;s (s ? 0) results from the execution of the sequence
applied to the intial state oe i;0 . More precisely, the event e i;s moves P i from the local state
oe i;s\Gamma1 to the local state oe i;s . By definition, we say that "e i;x belongs to oe j;s " (sometimes denoted as
Let H be the set of all the events produced by a distributed computation. This computation
is modeled by the partially ordered set b
!), where hb
denotes the well-known Lamport's
happened-before relation [16].
2.2 Local and Global Checkpoints
Local checkpoints. A local checkpoint C is a recorded state (snapshot) of a process. Not every
local state is necessarily recorded as a local checkpoint, so the set of local checkpoints is only a subset
of the set of local states.
Definition 2.1 A communication and checkpoint pattern is a pair ( b
H is a distributed
computation and C b
H is a set of local checkpoints defined on b
C i;x represents the x-th local checkpoint of process P i . The local checkpoint C i;x corresponds to
some local state oe i;s with x - s. Figure 1 shows an example of a checkpoint and communication
4 We assume a process does not send messages to itself.
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 5
pattern 5 . We assume that each process P i takes an initial local checkpoint C i;0 (corresponding to
oe i;0 ), and after each event a checkpoint will eventually be taken.
Ik;1 Ik;2 Ik;3
I j;1

Figure

1: A Checkpoint and Communication Pattern
message m sent by process P i to process P j is called orphan with respect to the ordered pair of
local checkpoints (C i;x ,C j;y ) iff the delivery of m belongs to C j;y (deliver(m) 2 C j;y ) while its sending
event does not belong to C i;x (send(m) 62 C i;x ). An ordered pair of local checkpoints is consistent iff
there are no orphan messages with respect to this pair. For example, Figure 1 shows that the pair
(C k;1 ,C j;1 ) is consistent, while the pair (C i;2 ,C j;2 ) is inconsistent (because of orphan message m 5 ).
Global checkpoints. A global checkpoint is a set of local checkpoints, one from each process. For
example, are two global checkpoints depicted in the Figure 1.
Definition 2.2 A global checkpoint is consistent iff all its pairs of local checkpoints are consistent.
For example, Figure 1 shows that fC i;1 ; C is a consistent global checkpoint, and due to the
inconsistent pair (C i;2 ; C j;2 ), the global checkpoint fC is not consistent.
2.3 Z-Paths and Z-Cycles
The sequence of events occurring at P i between C called a checkpoint interval
and is denoted by I i;x (see Figure 1). The Z-path notion, introduced for the first time by Netzer and
Xu [21], generalizes the notion of a causal path of messages defined by Lamport's happened-before
relation. More precisely :
Definition 2.3 A Z-path exists from local checkpoint A to local checkpoint B if and only if A precedes
B in the same process, or a sequence of messages [m exists such that
1. A precedes send(m 1 ) in the same process, and
2. for each m i is in the same or erlier interval as send(m i+1 ), and
3. delivery(m q ) precedes B in the same process.
In

Figure

is a Z-path from C k;0 to C i;2 ; [m are two Z-paths from C i;2
to C k;2 .
Definition 2.4 In a Z-path [m two consecutive messages m ff and m ff+1 form a Z-pattern
5 This figure uses the usual space-time diagram. Local checkpoints are indicated by black rectangular boxes; the other
local states are not explicitly indicated.
6 J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
In

Figure

1, we can see that [m are two Z-patterns.
Definition 2.5 A Z-path is causal iff it does not include Z-patterns (i.e., the delivery event of each
message (except the last) occurs before the send event of the next message in the sequence). A Z-path
is non-causal iff it is not causal.
A Z-path with only one message is trivially causal. Every non-causal Z-path is the concatenation of
shorter causal Z-paths. In Figure 1, [m is a non-causal Z-path; it is the concatenation
of the causal Z-paths [m 3 ]; [m
Definition 2.6 A Z-path from a local checkpoint C i;x to the same local checkpoint C i;x is called a
Z-cycle. (We say that it involves the local checkpoint C i;x .)
The Z-path [m is a Z-cycle that involves the local checkpoint C k;2 . We can observe that a
Z-cycle always includes a Z-pattern.
2.4 Useless Checkpoints
Definition 2.7 A local checkpoint C i;x is useless iff it cannot belong to any consistent global check-point

The following important characterization of useless checkpoints has been stated in [21]:
Theorem 2.1 (Netzer-Xu 1995) A local checkpoint C i;x is useless iff it is involved in a Z-cycle.
For example in Figure 1, C k;2 is useless. The Z-path [m is a Z-cycle including C k;2 . It
includes the Z-pattern [m The interested reader will find a proof of this theorem in [21] and in
[25].
3 Design Principles of the Protocol
The set C b
of checkpoints taken during the execution of a computation b
H is composed of basic checkpoints
and forced checkpoints. As indicated in the Introduction, why and when a basic checkpoint is
taken depends only on the application (such as for a property detection protocol or a rollback-recovery
protocol). Forced checkpoints are taken by the communication-induced checkpointing protocol to ensure
that no checkpoint is useless. The aim of the protocol we wish to design is to keep low the number
of forced checkpoints. The protocol works by evaluating a predicate upon every message reception
and possibly taking a forced checkpoint (hence the name communication-induced checkpointing pro-
tocol). The predicate is based on past knowledge of the communication and checkpointing patterns,
and forced checkpoints are taken to prevent Z-cycles from forming.
3.1 Basic Idea: A Checkpoint Timestamping Mechanism
With each checkpoint C, let us associate a timestamp denoted C:t. We consider in the following that
the domain of timestamp values is the set of positive integers. The protocol is based on the following
theorem.
Theorem 3.1 (For any pair of checkpoints C j;y and C k;z , such that there is a Z-path from C j;y to
(there is no Z-cycle).
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 7
Proof
if part. Suppose that a Z-cycle exists from C i;x to C i;x . This Z-cycle is a Z-path from C i;x to C i;x .
From the assumption of the theorem, this would imply C i;x :t ! C i;x :t.
only if part. If there is no Z-cycle, then the Z-graph (whose vertices are local checkpoints and paths
are Z-paths) is partially ordered. It follows there a topological sort of the local checkpoints with the
required property. 2 Theorem 3:1
The idea underlying this theorem is that, if we can design a protocol that manages timestamps
and takes forced checkpoints in such a way that timestamps always increase along any Z-path, then
no Z-cycles can possibly form, and no checkpoints will be useless. We assume each process P i has a
local logical clock lc i managed in the following classical way [16]:
ffl Before it takes a (basic or forced) checkpoint, P i increases by 1 its local clock (and associates
the new value with the checkpoint).
ffl Every message m is timestamped with the value of its sender clock (let m:t be the timestamp
associated with m).
ffl When a process P i receives a message, m updates its local clock lc i := max(lc
It follows from this classical mechanism that, if there is a causal Z-path from C j;y to C k;z , then we
have C j;y :t ! C k;z :t. We examine now the case of non-causal Z-paths.
3.2 To Checkpoint or Not to Checkpoint?
Given the previous timestamping mechanism, let us consider the situation depicted in Figure 2.a where
C j;y is a local checkpoint taken by P j before sending m 1 and C k;z is the first checkpoint of P k taken
after the delivery of m 2 . As the sending of m 2 and the delivery of m 1 belong to the same interval of
constitutes a Z-pattern from C j;y to C k;z .
Ck;z
a. b.

Figure

2: Must P i Take a Forced Checkpoint?
When two cases can occur:
In that case, C j;y . Hence, the Z-pattern [m
consistent with the assumption of Theorem 3.1.
In this case, a safe strategy to prevent Z-cycle formation consists of directing P i
to take a forced checkpoint C i;x before delivering m 1 (as shown in Figure 2.b). This "breaks"
so it is no longer a Z-pattern.
This strategy can be implemented in the following way. Each process P i manages a boolean
array sent to i [1::n] in order to know whether the reception of a message creates a Z-pattern;
8 J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
sent to i [k] has the value true iff P i has sent a message to P k since its last checkpoint. Moreover,
manages an array of integers min to i [1::n]; min to i [k] keeps the timestamp of the first message
sent to P k since P i 's last checkpoint. The condition expressed as
sent to i
takes a forced checkpoint if C is true. The next section shows how this safe strategy can
be improved by sharpening the predicate which will cause fewer forced checkpoints to be taken.
3.3 Reducing the Number of Forced Checkpoints
The previous strategy does not utilize the information that P i could have concerning the values of
local clocks of the other processes. For each k(1 - k - n), let us denote by cl i (k) the value of P k 's
local clock as perceived by P i (P i can obtain this knowledge with a classical piggybacking technique
as will be shown in Section 4.1). If obviously cl i the perception of
local clock by P i is only an approximation such that cl i (k) - lc k . Consider again the situation
depicted in Figure 2.a, where message m 1 arrives from P j , creating a Z-pattern with message m 2 sent
to 6 P k . If the following property holds
cl
then the Z-pattern [m consistent with the assumption of Theorem 3.1. Let us consider the
property P in the case where m 1 carries the value of lc j when m 1 is sent,
the first relation C j;y necessarily holds when m 1 is received. So, the property P can be
violated only if, when m 1 is received, m 1 :t ? cl i (k) or if cl i (k) - C k;z :t. It follows that to prevent
the formation of the Z-pattern [m that would violate property P (and consequently that could
possibly be inconsistent with the assumptions of Theorem 3.1), the protocol requires P i to take a
forced checkpoint before delivering m 1 to the application if m 1 :t ? cl i (k) or if cl i
The question now is to determine to which value of cl k the approximation cl i (k) refers. Let us
examine the two possible cases.
Ck;z
Ck;z
a. b.

Figure

3: cl i (k) is a Lower Bound of C k;z :t
i) The value cl i (k) has been brought to P i by a causal Z-path that started from P k before C k;z .
This situation is illustrated in Figure 3 (more precisely, cl i (k) is brought to P i by - 1 in Figure
3.a and by - 2 \Delta [m 1 ] in Figure 3.b). In that case we have cl i consequently, P i
has to take a forced checkpoint only if m 1 :t ? cl i (k).
6 Recall that Ck;z is the first checkpoint taken by Pk after the delivery of m2 .
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 9
ii) The value cl i (k) has been brought to P i by a causal Z-path that started from P k after C k;z . This
situation is illustrated in Figure 4 (more precisely, the relevant causal Z-path is - 1 in Figure 4.a
and is in Figure 4.b; note that both figures can be redrawn as indicated in Figure 5
where -, the causal Z-path that brings to P i the last value of P k 's local clock, is - 1 or - 2 \Delta [m 1 ]).
In that case we have cl i (k) - C k;z :t. This exactly corresponds to the pattern described in Figure
5. So, the problem for P i is to recognize this pattern and take a forced checkpoint if it occurs.
Let C 1 be a predicate describing this pattern occurrence.
a. b.

Figure

4: cl i (k) is not a Lower Bound of C k;z :t
Ck;z

Figure

5: A Causal Z-Path
From this discussion it follows that the previous condition C (which P i tests to know if it should
take a forced checkpoint when it receives a message m 1 ) can be refined into C 0
sent to i [k] - (m cl
The next section shows how to express this predicate with appropriate data structures so it can
be evaluated on-line by each process.
4 A First Version of the Protocol
This section presents a first version of the protocol which is directly obtained from the previous
analysis. (Then, from this version and a few theorems, Section 5 will provide a less costly version of
this protocol.)
4.1 Data Structures
In addition to the arrays sent to i [1::n] and min to i [1::n] previuosly described, every process P i maintains
the following data structures.
Array clock i . Each process P i manages an array clock i [1::n] with the following meaning: clock i
highest value of lc k known by P i (note that clock i [i] is lc i and so we do not require lc i in the following).
This array is initialized to managed as
7 Note that clock i is a vector containing Lamport timestamps.
J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
ffl When it takes a (basic or forced) checkpoint, P i increments clock i [i] by 1 (definition of lc i ).
sends a message m, the current value of clock i is appended to m (let it be m:clock).
receives m from P j , it performs the following updates:
Lamport clock; this statement
updates clock).
Using this data structure, when P i receives a message m 1 , we have cl i
Thus, with these elements, C 0 can be rewritten as
:sent to i [k] -
The next two arrays provide a way to evaluate C 1 .
Array ckpt i . This array is a vector clock that counts how many checkpoints have been taken by
each process. So, ckpt i number of checkpoints taken by P k to P i 's knowledge. This vector clock
is managed in the usual way [9]. Let m:ckpt be the value appended to m by its sender P i (i.e., the
value of the array ckpt i at sending time).
Array taken i . This boolean array is used in conjunction with ckpt i to evaluate C 1 . It has the
following meaning: taken i [k] is true iff there is a causal Z-path from the last checkpoint of P k known
by P i to the next checkpoint of P i , and this causal Z-path includes a checkpoint. It is managed in the
following way:
When P i takes a checkpoint, it sets to true all its entries except the i-th one (taken i [i] always
remains
ffl When it sends a message, P i appends to it the current value of taken i (let m:taken be this
value).
ffl When it receives m, P i updates taken i in the following way in order to maintain its meaning:
docase
With these data structures, the condition C 1 can be expressed in the following way:
When considering Figure 5, the first part of condition C 1 states that there is a causal Z-path (namely,
starting after C i;x and arriving at P i before C i;x+1 , while the second part of C 1 indicates that
some process has taken a checkpoint along this causal Z-path.
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 11
4.2 The Protocol
The protocol executed by each process P i is described in Figure 6. S0, S1 and S2 describe the
initialization, the statements executed by P i when it sends a message, and the statements it executes
when it receives a message, respectively. The procedure take checkpoint is called each time P i takes a
checkpoint (basic or forced). As indicated previously, why and when a basic checkpoint is taken are
not part of the protocol.
procedure take checkpoint is
8k do sent to i [k] := false enddo;
8k do min to i [k] := +1 enddo;
clock
save the current local state with a copy of clock i [i];
i;x be this checkpoint. We have C i;x
initialization
8k do clock i [k] := 0; ckpt i [k] := 0 enddo;
taken i [i] := false;
take checkpoint;
sends a message to Pk
if :sent to i [k] then sent to i [k] := true; min to i [k] := clock i [i] endif;
receives (m; clock; ckpt; taken) from P j
% m:clock[j] is the Lamport's timestamp of m (i.e., m:t) %
sent to i [k] -
then take checkpoint % forced checkpoint %
clock update of the scalar clock lc
do
clock
case
case

Figure

First Version The Protocol
4.3 A Property of the Protocol
The following theorem shows how a consistent global checkpoint C a can be associated with each Lamport
timestamp a. It follows that, given a local checkpoint C i;x timestamped a (i.e., C i;x
can easily be associated with a consistent global checkpoint to which it belongs.
Theorem 4.1 Let a be a Lamport timestamp (a ? 0) and let C a be the global checkpoint (C 1;x
defined in the following way: 8k, C k;x k
is the last checkpoint of P k such that C k;x k
C a is a consistent global checkpoint.
Proof Suppose that C a is not consistent. So, C a contains a pair of checkpoints (C i;x ; C k;z ) such that
there exists a message m 2 sent by P i to P k with send(m 2
12 J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
By assumption, C k;z :t - a (P1). By construction of timestamps, C i;x consequently
Ck;z
I i;x+1

Figure

7: Message m 2 is Orphan with Respect to (C i;x ; C k;z )
Let C i;x+1 be the first checkpoint taken by P i after C i;x and let C k;z \Gamma1 be the last checkpoint taken by
before C k;z (see Figure 7). By assumption, C i;x+1 :t ? a. This assumption, combined with P2, gives
(P3). Moreover, this assumption, combined with P1, gives C k;z :t - C i;x+1
(P4).
Ck;z
Ck;z
b.
a.
Ik;z

Figure

8: Causal and Non-Causal Z-Paths
P3 implies that between the two consecutive local checkpoints C i;x and C i;x+1 , the clock of P i
(namely, clock i [i]) is incremented by at least two. As, by assumption, no local checkpoint is taken
by P i between C i;x and C i;x+1 , this incrementation can occur only if, during the interval I i;x+1 , P i
receives at least one message whose timestamp is equal to C i;x+1 :t \Gamma 1. Let m 1 be the first message
such that deliver(m 1
Figure 8.a),
we have C k;z contradicts P4. Thus the situation is as depicted
in

Figure

8.b. When m 1 arrives, we have:
ffl (because of m 2 ) sent to i
ffl min to i (from P4 and as P j is the sender of
:t, from which we can conclude that m 1 :clock[j] ? min to i [k] (P6).
Recall that condition C 0 tested by P i to know if it has to take a forced checkpoint when it receives
sent to i [k] -
arrives, as shown by P5 and P6, the first two lines of this condition are satisfied.
We show now by a case analysis that a checkpoint is necessarily taken by P i between C i;x and C i;x+1 ,
which contradicts the hypothesis.
ffl Case clock
In that case we have, when m 1 is received, max(clock :t. Combining this
with P4, we get max(clock
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 13
From P5, P6 and P7, it follows that P i has to take a checkpoint between C i;x and C i;x+1 , which
contradicts the hypothesis.
ffl Case clock
there exists a causal Z-path from C k;z to C i;x+1 (the Z-path
in

Figure

4.b). In that case, when m 1 is received we have (m 1
(P8).
From P5, P6 and P8, it follows that P i has to take a checkpoint between C i;x and C i;x+1 , which
contradicts the hypothesis.
ffl Case clock
In this case, there is a causal Z-path - 1 starting from C k;z and arriving at P i after C i;x and
before (this is the situation described in Figure 4.a). Let m 0 be the message ending - 1 that
is received by P i . Note that the message m 0 is received by P i after the sending of m 2 (if this was
not the case, we would have C k;z
at the reception of m 0 we had (see the discussion in Section 3.3):
- sent to i receiving m 0 ).
(because Lamport clocks strictly increase along a causal
Z-path -namely, [m 2 on which a checkpoint has been taken).
is the pattern described in Figure 5 which is
detected by condition C 1 ).
It follows that P i has taken a checkpoint between C i;x and C i;x+1 when it received m 0 , which
contradicts the hypothesis.
Theorem 4:1
5 An Improved Version of the Protocol
This section first proves an invariant of the protocol. Then, this invariant is used to simplify the
condition C 0 and, consequently, to derive a less costly version of the protocol.
5.1 An Invariant
Theorem 5.1 The following assertion I is invariant:
I sent to i [k]
Proof Let i and k be two given process numbers. We must show that the property I(i;
( sent to i [k] during the execution of P i .
To this end, we show: (1) that the property holds at P i initialization (base case) and, (2) that, if the
property holds before an event, then it still holds after its execution (induction). The only events to
be considered are those that can modify the values of variables involved in the property, namely, the
taking of a checkpoint, the sending and the reception of a message, denoted take checkpoint, (S1) and
(S2) in

Figure

6, respectively.
Remind that, from Lamport clocks property, the relation clock i [i] - clock i [k] is always true and,
consequently, for any message m sent by P j , we have m:clock[j] - m:clock[k]. When an event triggers
actions modifying the value of a variable x, we will denote by x its value before the event and by x 0
its value after the event.
14 J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
base case. As sent to i [k] is initialized to the value false, the property initially holds.
induction.
Taking a checkpoint. The property holds at the beginning of each checkpoint interval, since the
array sent to i is reset to false.
Sending of a message by P i to P k . Note that the array clock i is not modified by (S1).
ffl sent to i [k] has the value false (first sending to P k ).
Then, before (S1) min to i thus, after (S1), min to i [k]
clock i [k], we have clock i [i]
after (S1). It follows that I holds after (S1).
ffl sent to i [k] has the value true (not the first sending to P k ).
As arrays clock i and min to i are not modified by this sending, it follows that I still holds after
(S1).
Reception by P i of a message m sent by P j . This can modify the values of clock i [i] and
clock i [k].
If the arrival of m forces P i to take a checkpoint, then I(i; trivially holds after (S2) (as sent to i
is reset to false). So, we have only to examine the case where the arrival of m does not force P i to
take a checkpoint. This means that the condition C 0 of the protocol is not satisfied, i.e.,
If sent to i [k] is false before (S2), as (S2) does not modify this variable, I(i; still holds after (S2).
Thus, we have only to examine the case where one of the two last terms is satisfied. Note that this
implies:
For the ease of the proof, we use the following notations :
ck
We have the following assumptions (A-G):
holds before the event)
ck
ck 0 (property of Lamport clocks)
mck (property of Lamport clocks)
checkpoint is taken)
We must prove the relation (R) c remains true after (S2)).
Two cases have to be considered, according to the two terms of the assumption (G).
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 15
First case: (G1) m - mcj.
From (A) we get c - m, and thus c - mcj. So, (B) reduces to c
From (C), we get max(ck 0 ; m) - max(ck; m), and thus by using successively, (A),
(E), we get: max(ck m). From which we conclude
replacing in (B) c and mcj with
their values defined by (A) and (1), respectively, we get:
which (due to (mcj - max(ck; mck)) (G2)) reduces to:
which (due to (C)) reduces to c
Theorem 5:1
5.2 Simplifying the Condition
The condition used by a process P i to decide whether or not it has to take a forced checkpoint when
it receives a message m, is:
sent to i [k] - (m:clock[j] ? min to i [k])
The following theorem shows that this condition can be simplified.
Theorem 5.2
sent to i [k]
We have C 0 j D.
Proof Let us consider the following set of predicates:
A j sent to i [k]
ffl First we show that C 1
Condition C 1 has been introduced in Section 3.2 to characterizes the situation depicted in Figure
9. Message m (sent by P j ) terminates a causal Z-path [m 0 ]\Delta- 1 \Delta- 2 \Delta[m] that: (1) starts with m 0 after
is about to arrive at P i before C i;x+1 (because
and (3) along this Z-path, a process P l has taken a checkpoint C l;z (because m:taken[i] is true).
As Lamport timestamps do not decrease and do increase when a checkpoint is taken we have:
J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal

Figure

9: What C 1 Characterizes
It follows that: C 1 (sent to i [k] - min to i [k] ! m:clock[j]). With the previous notations:
ffl Now by using classical logic rules, we have:
(definition of C 0 )
(definition of D)
(because, due to invariant I, we have
E) - C 1 (because E is independent of
(definition of D).
Theorem 5:2
5.3 Reducing the Size of Data Structures
Theorem 5.2 shows that the array min to i [1::n] is not used in condition D and consequently can be
suppressed. A finer analysis shows that each array clock i [1::n] can be replaced by a single integer
lc i plus a boolean array greater i [1::n]. This comes from the following two observations. When we
consider D we see that:
ffl The only element of the array clock i that is used by D is clock i [i], i.e., the Lamport clock of P i .
ffl As m:clock[j] - m:clock[k] is always true (remind that m:clock[j] is the highest clock value
known by P j when it sends m), it follows that the subcondition m:clock[j] ? m:clock[k] is
equivalent to m:clock[j] 6= m:clock[k].
It follows that, in each process P i , the array clock i [1::n] can be replaced by a single Lamport
clock lc i (whose value is equal to clock i [i]) plus a boolean array greater i [1::n] whose meaning is the
these new data structures, condition D can be
rewritten as
Consequently, messages have now to piggyback a Lamport clock value and a boolean array instead
of an array of Lamport clock values. The resulting protocol is described in Figure 10. The update of
the integer array clock i is replaced the update of the boolean array greater i . Each process manages
clock and n checkpoint sequence numbers) and 3   n booleans. Each
message piggybacks booleans.
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 17
procedure take checkpoint is
8k do sent to i [k] := false enddo;
save the current local state with a copy of lc
i;x be this checkpoint. We have C i;x
initialization
8k do ckpt i [k] := 0 enddo;
taken i [i] := false; greater i [i] := false
take checkpoint;
sends a message to Pk
sent to i [k] := true;
receives (m; lc; greater;ckpt; taken) from P j
% m:lc is the Lamport's timestamp of m %
then take checkpoint % forced checkpoint %
case
case
docase
enddocase

Figure

10: Final Protocol
6 Discussion
This section discusses the protocol. It shows that it provides a general framework from which existing
protocols can be obtained.
ffl Let us suppress all the data structures except the array sent to i [1::n] which is replaced by a
single boolean sent i with the following meaning: sent sent to i [k]), i.e., sent i is true
iff a message has been sent by P i since its last checkpoint. The protocol becomes drastically
simplified and reduces to the well-known Russell protocol [23] 8 , shown in Figure 11. Russel's
protocol is characterized by the following property. When considering only deliver, send and
checkpoint events, the behavior of each process corresponds to the following regular language:
(deliver   send   checkpoint)
In other words, no deliver event can follow immediately a send event. Of course, this protocol
may take more forced checkpoints (and never less) than the proposed protocol.
ffl Another protocol can be obtained by considering only a subset of the data structures. For
example, when we eliminate the arrays ckpt i [1::n] and taken i [1::n], we obtain a protocol characterized
by the following condition C 00
8 This protocol has been adapted to the context of mobile computing in [1].
J.-M. H'elary & A. Mostefaoui & R. Netzer & M. Raynal
procedure take checkpoint is
do sent i := false enddo;
save the current local state as a local checkpoint;
initialization
take checkpoint;
sends a message to Pk
sent i := true;
send(m) to Pk ;
receives (m) from P j
if sent i then take checkpoint % forced checkpoint % endif;

Figure

11: Russell's Protocol
which may take more forced checkpoints (and never less) than the proposed protocol but requires
messages to piggyback only one integer, namely, m:lc (the value of lc j at the time P j sent m).
ffl We can further simplify the protocol by eliminating the array sent to i [1::n]. We then get the
following condition C 000
These simplications result in the protocol shown in Figure 12, which is a variant of the protocol
described in [4] and of the quasi-synchronous version proposed by Manivannan and Singhal in
[19] 9 .
procedure take checkpoint is
save the current local state with a copy of lc
initialization
take checkpoint;
sends a message to Pk
receives (m; lc) from P j
then take checkpoint % forced checkpoint %

Figure

12: A Variant of Manivannan-Singhal's Quasi-Synchronous Protocol
9 The original quasi-synchronous protocol proposed in [19] differs from this variant in the following way. (1) Each
process takes its basic checkpoints according to some local logical periodicity. (2) In (S2) lc i 'update is done in the then
part, just before calling take checkpoint. (3) Within the procedure take checkpoint, the variable lc i is increased only if
the checkpoint is basic.
Irisa
Communication-Based Prevention of Useless Checkpoints in Distributed Computations 19
New protocols can be designed by considering other simplifications of the basic protocol. This discussion
shows that there is a tradeoff between the number of forced checkpoints that are taken and the
size of control information piggybacked by application messages. In general, the smaller the control
information, the greater the number of forced checkpoints. This raises an interesting question: is the
proposed protocol the optimal one, i.e., is it a communication-induced checkpointing protocol that,
without a priori knowledge of when basic checkpoints are taken, takes the fewest number of forced
checkpoints to ensure that no checkpoint is useless? This optimality question remains an open problem.
Some communication-induced checkpointing protocols use a heuristic approach to prevent useless
checkpoints. In these protocols the condition tested at message reception is not safe in the sense some
basic checkpoints may remain useless. A protocol of this family is described in [26]. Using experimental
results, the authors show that their protocol reduces rollback distance to less than one checkpoint
interval per process and the number of forced checkpoints is only 4% of the number of basic checkpoints.
The proposed protocol encompasses some of these heuristic-based protocols. It is easy to show that
the heuristics used in [26] is a weakening of the condition used
in the proposed protocol.
7 Conclusion
A useless checkpoint is a local checkpoint that cannot be part of a consistent global checkpoint. This
paper has addressed the following important problem. Given a set of processes that take (basic)
local checkpoints in an independent and unknown way, we have designed a communication-induced
checkpointing protocol that directs processes to take (as few as possible) additional local (forced)
checkpoints to ensure that no local checkpoint is useless.
Our protocol is general and efficient. It has also been shown to take fewer forced checkpoints than
existing protocols solving the same problem. These improvements were obtained by using control
information composed booleans (n being the number of processes). It has
also been shown that the size of this control information can be reduced (or even eliminated) at the
price of additional forced checkpoints. So, the protocol can easily be tuned for any desired control-
information-overhead / performance tradeoff.
The design of this protocol has been motivated by the wide use of communication-induced check-pointing
protocols in applications that require consistent global checkpoints, such as the detection of
stable or unstable properties, rollback-recovery, and determination of distributed breakpoints.



--R

Checkpointing Distributed Application on Mobile Computers

Independent Checkpointing and Concurrent Rollback for Recovery - An Optimistic Approach
A Distributed Domino-Effect Free Recovery Algorithm
Determining Global States of Distributed Sys- tems
Consistent Detection of Global Predicates.
Distributed Checkpoint Detection in Message-Passing Programs
A Survey of Rollback-Recovery Protocols in Message-Passing Systems
Logical Time in Distributed Computing Systems.
Proc 10th IEEE Int.
Detection of Strong Unstable Predicates in Distributed Programs.
Detection of Stable Properties in Distributed Ap- plications
Efficient Distributed Detection of Conjunction of Local Predicates in Asynchronous Computations.
A Scheme for Coordinated Execution of Independently Designed Recoverable Distributed Processes
Checkpointing and Rollback-Recovery for Distributed Systems

Information Processing Letters

A Low Overhead Recovery Technique Using Quasi-Synchronous Check- pointing
Breakpoint and Halting in Distributed Programs.
Necessary and Sufficient Conditions for Consistent Global Snapshots
System Structure for Software Fault-Tolerance
State Restoration in Systems of Communicating Processes
Lazy Checkpoint Coordination for Bounding Rollback Propagation.
Consistent Global Checkpoints That Contain a Given Set of Local Checkpoints
Adaptive Independent Checkpointing for Reducing Rollback propagation.
--TR
Checkpointing and rollback-recovery for distributed systems
On distributed snapshots
Detection of stable properties in distributed applications
Logical Time in Distributed Computing Systems
Consistent detection of global predicates
Necessary and Sufficient Conditions for Consistent Global Snapshots
Distributed snapshots
A unified framework for the specification and run-time detection of dynamic properties in distributed computations
Adaptive recovery for mobile environments
Detection of Strong Unstable Predicates in Distributed Programs
Distributed breakpoint detection in message-passing programs
Consistent Global Checkpoints that Contain a Given Set of Local Checkpoints
Theoretical Analysis for Communication-Induced Checkpointing Protocols with Rollback-Dependency Trackability
Rollback-dependency trackability
Evaluations of domino-free communication-induced checkpointing protocols
Time, clocks, and the ordering of events in a distributed system
Checkpointing distributed applications on mobile computers
Communication-Induced Determination of Consistent Snapshots
On-the-Fly Detection of Conjunctions of Local Predicates in Distributed Computations
A low-overhead recovery technique using quasi-synchronous checkpointing

--CTR
Jiang Wu , Yi Luo , D. Manivannan, An enhanced model-based checkpointing protocol, Proceedings of the 25th conference on Proceedings of the 25th IASTED International Multi-Conference: parallel and distributed computing and networks, p.332-337, February 13-15, 2007, Innsbruck, Austria
Gyung-Leen Park , Hee Youn Yong, A New Approach for High Performance Computing Systems with Various Checkpointing Schemes, The Journal of Supercomputing, v.33 n.1, p.65-78, July      2005
Emmanuelle Anceaume , Jean-Michel Hlary , Michel Raynal, Tracking immediate predecessors in distributed computations, Proceedings of the fourteenth annual ACM symposium on Parallel algorithms and architectures, August 10-13, 2002, Winnipeg, Manitoba, Canada
Adnan Agbaria , Hagit Attiya , Roy Friedman , Roman Vitenberg, Quantifying rollback propagation in distributed checkpointing, Journal of Parallel and Distributed Computing, v.64 n.3, p.370-384, March 2004
J. M. Hlary , A. Mostefaoui , M. Raynal, Interval consistency of asynchronous distributed computations, Journal of Computer and System Sciences, v.64 n.2, p.329-349, March 2002
B. Gupta , S. K. Banerjee, A Roll-Forward Recovery Scheme for Solving the Problem of Coasting Forward for Distributed Systems, ACM SIGOPS Operating Systems Review, v.35 n.3, p.55-66, July 1 2001
Jichiang Tsai, On Properties of RDT Communication-Induced Checkpointing Protocols, IEEE Transactions on Parallel and Distributed Systems, v.14 n.8, p.755-764, August
fault-tolerance;checkpointing protocols;asynchronous distributed system