Deepanker Aggarwal
email: deepanker10027@iiitd.ac.in

Astrid Kiehn
email: astrid@iiitd.ac.in

Analyzing Mutable Checkpointing via Invariants

Keywords: snapshot, checkpointing, consistency, distributed computing

de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The on-the-fly calculation of a snapshot, a consistent global state, is a known means to enhance fault tolerance and system diagnosis of distributed systems. Coordinated snapshot algorithms exchange coordination messages to orchestrate the checkpointing. One of these is mutable checkpointing ( [START_REF] Cao | On coordinated checkpointing in distributed systems. Parallel and Distributed Systems[END_REF][START_REF] Cao | Mutable checkpoints: a new checkpointing approach for mobile computing systems[END_REF][START_REF] Cao | Checkpointing with mutable checkpoints[END_REF]) which aims at a reduced coordination overhead -both in number of checkpoints to be taken and coordination messages to be sent. It is known from [START_REF] Cao | On coordinated checkpointing in distributed systems. Parallel and Distributed Systems[END_REF] that there is no algorithm which minimizes the number of checkpoints without blocking processes. To avoid the blocking, in mutable checkpointing, local checkpoints may be taken which may be discarded later. The presence of such checkpoints and an additional feature to further reduce the number of coordination messages hinder an easy analysis of the algorithm. With this paper we equip mutable checkpointing with a precise formal model and make it amenable to a formal analysis. We establish an invariant to obtain deeper insight into the intermediate behavior of the algorithm and prove consistency of the final snapshot. The model can further be used as a common ground for qualitative comparisons of snapshot algorithms. We give such a comparison with the conceptually different blocking queue algorithm [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF] which, as mutable checkpointing, had been set up to reduce the coordination overhead.

Unlike other coordinated snapshot algorithms (eg. Chandy/ Lamport's seminal algorithm [START_REF] Chandy | Distributed snapshots: determining global states of distributed systems[END_REF]), mutable checkpointing algorithms do not monotonously build up the snapshot with the underlying computation. In mutable checkpointing, checkpoints of local states may be taken from which the underlying computation had already progressed. The computation of the snapshot, thus, involves forward and backward reasoning and the correctness of the algorithm, the consistency of the final snapshot, is not obvious. The proofs provided in the literature [START_REF] Cao | On coordinated checkpointing in distributed systems. Parallel and Distributed Systems[END_REF][START_REF] Cao | Mutable checkpoints: a new checkpointing approach for mobile computing systems[END_REF][START_REF] Cao | Checkpointing with mutable checkpoints[END_REF] are based on contradiction, use absence of orphans (messages recorded as received but not as being sent) as consistency notion, and lack a formal model. The formal proof provided in this paper is based on an invariant which characterizes the snapshot partially computed. We use a stronger but well-accepted notion of consistency [START_REF]Distributed Algorithms for Message-Passing Systems[END_REF]: reachability within the partial order representing the underlying distributed computation. It implies the absence of orphans.

In case of a snapshot algorithm the invariant should explain how the snapshot gradually builds up on course of the underlying computation. For a global state S of the underlying computation, the invariant should provide the snapshot calculated so far. We call the latter the potential snapshot psn(S) of S. For a snapshot algorithm which simply freezes local processes at certain points of their computation, the potential snapshot consists of these checkpoints and the current states of the none-frozen processes. In mutable checkpointing, local processes may be frozen to states -the so-called mutable checkpoints -from which they had already progressed. Reachability of psn(S) can therefore not simply be obtained from a simultaneous progression of psn(S) and S. We solve this problem by extracting a set of global states from S of which each corresponds to a different prediction of which of the mutable checkpoints will be frozen. These states collectively define the psn(S). We then show how each of the states in psn(S) progresses together with S, where the progress may be partial, only, due to the frozen processes. Using this result we provide a direct proof for the consistency of the final snapshot. The potential snapshot, however, -or more precisely the predicted states of it -, in general, are shown not to be consistent. This implies that if the run of a mutable checkpointing algorithm needs to be interrupted then the entire checkpointing needs to be started afresh.

The proof is based on the specification of the operational behavior of what we consider the essence of mutable checkpointing. We extracted it from the pseudocode given in [START_REF] Cao | Checkpointing with mutable checkpoints[END_REF] by removing all details not related to the basic concept of taking a mutable checkpoint upon receiving a flagged message for the first time (and before a checkpoint) -where the flag indicates that the sender had taken a checkpoint or a mutable checkpoint. In this way we obtained a concise description of the core of mutable checkpointing which we see as another contribution of this paper.

With this formal model and analysis we relate mutable checkpointing to the blocking queue algorithm introduced in [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF]. In fact, this paper can be seen as a companion paper as it deploys the proof technique developed there (however, setting up the invariant for mutual checkpointing was a much more demanding task). Having fixed the underlying computation, the two snapshot algorithms can directly be compared due to the same underlying formal model. We show that the respective final snapshots, in general, are incomparable and discuss the differences between the algorithms.

The paper is structured as follows. Basic terminology is introduced in Section 2, followed by a short description of mutable checkpointing in Section 3. Section 4 specifies the operational behavior of the algorithm defined in terms of predicates and rules. The rules we deduced from the pseudocode of [START_REF] Cao | Checkpointing with mutable checkpoints[END_REF] where we abstracted away as many details as possible to get the essence of mutable checkpointing. In Section 5 we introduce the potential snapshot, show its progression with the underlying computation and prove the consistency of the final snapshot. Section 6 gives the comparison with the blocking queue algorithm of [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF]. The conclusion is given in Section 7.

Preliminaries

We assume a finite number of processes P 1 , ..., P n which communicate solely by message passing via FIFO channels C ij . Channel C ij leads from P i to P j and for each pair of processes there is such a unidirectional channel. Channels are assumed not to lose or reorder messages. There is no assumption on the state space of processes.

A state S = (p 1 , . . . , p n , Chan) of a distributed computation is given by the histories (events performed so far) of the local processes and the current contents of the channels where Chan : {C ij | i, j ≤ n, i = j} → MSG * and p i ∈ Events * . To ease readability, for a global state S we attach S as a superscript to the histories and channels and abbreviate Chan(C ij ) S by C S ij . In the initial state S 0 , p S0 i = ε, and C S0 ij = ε for all i, j. A distributed computation is a sequence

π = S 0 e1 -→ S 1 e2 -→ S 2 • • • e k -→ S k
where each S i is obtained from updating S i-1 according to the semantics of event e i . We also write π = S 0 → * S k to mention the initial and final states of π, explicitly.

The notion of consistency of a state with a computation π is best understood in terms of π's space-time diagram (its partial order representation, see [START_REF] Kshemkalyani | Distributed Computing: Principles, Algorithms, and Systems[END_REF], [START_REF]Distributed Algorithms for Message-Passing Systems[END_REF] or [START_REF] Babaoglu | Consistent global states of distributed systems: Fundamental concepts and mechanisms[END_REF]). A state is consistent with π if it is a cut of π closed under the happens-before ordering in the space-time diagram. Equivalently, a consistent state S of π can be characterized by that all local histories of S are prefixes of the corresponding histories of π's final state S k , and if a message occurs as received in a history of S then it also needs to occur as having been sent in a history (that is there are no orphans).

Snapshot algorithms are superimposed on a distributed computation π on course of which a state consistent with π is to be calculated. We will only describe the behavior of the snapshot algorithm which, if it is non blocking, should allow for send and receive events induced by the underlying computation at any point of time. All other events of the snapshot algorithm are coordination events.

Mutable Checkpoint Algorithms

Mutable checkpoint algorithms are coordinated snapshot algorithms which reduce the coordination overhead (compared to [START_REF] Chandy | Distributed snapshots: determining global states of distributed systems[END_REF]) by combining message flags (indicating whether messages have been sent before of after a checkpoint, cf. [START_REF] Lai | On distributed snapshots[END_REF]) with the new concept of mutable checkpoints. Mutable checkpoints are taken on a tentative basis (on volatile storage) and are only finalized (on non-volatile storage) when the need for a local checkpoint has been confirmed.

The Algorithm in Short

The initiating process requests the processes it depends on (from which it had received a message) to take a checkpoint. Any process receiving such a request takes a checkpoint and propagates the request further to the -up to its knowledge -so far uninformed processes it itself depends on. After a process has taken a checkpoint all the messages sent out by this process carry a flag (bb=1). A process which hasn't received a checkpoint request but a message with flag (bb=1), takes a mutable checkpoint indicating that it must convert the current local state to a checkpoint, if in future it receives a checkpoint request. This is done before the received message is processed and only if it hadn't taken a mutable checkpoint earlier. Under certain progress assumptions, all processes which, in principle, need to take a checkpoint will finally have done so and this completes phase I of the algorithm. Phase II would deal with the confirmation that the checkpointing is complete and the dissemination of this information to the local processes. However, in this paper we only investigate phase I.

With minor modifications the algorithm has widely been published see [START_REF] Cao | On coordinated checkpointing in distributed systems. Parallel and Distributed Systems[END_REF][START_REF] Cao | Mutable checkpoints: a new checkpointing approach for mobile computing systems[END_REF][START_REF] Cao | Checkpointing with mutable checkpoints[END_REF], our reference algorithm is [START_REF] Cao | Checkpointing with mutable checkpoints[END_REF]. We specify the operational behavior of the algorithm in terms of predicates and transition rules which an implementation would need to satisfy. To be able to focus on the essence of mutable checkpointing, in the translation we omitted everything related to earlier checkpointing and a feature to reduce the number of coordination messages further (the sent i condition). We also assume that the initiating process is always P 1 and as in [START_REF] Cao | Checkpointing with mutable checkpoints[END_REF] do not consider concurrent checkpointing. Finally, all details relating to termination (the completion of taking checkpoints) of phase I are omitted.

The Algorithm in Detail

Rule numbers in brackets refer to corresponding rules given in the next section.

1. As part of their computations, processes send messages to each other which come attached with a flag (Rules 1.1 and 1.2). If the flag is set, this indicates that the sending process has already taken its checkpoint (instantly or belated via a mutable checkpoint).

2. Every process maintains a dependency vector which provides all the processes it depends on. A process P i depends on process P j if P i has received a message from P j . This is a dynamic notion of dependency as at the time of initiation of the checkpointing all dependencies may not be known. The checkpointing will involve all processes which are dependent in a transitive way. Say at the time of initiation, the checkpointing process P 1 depends on P 2 and P 3 , and P 3 depends on P 4 . Then, P 4 needs to be included in the checkpointing. 3. The initiator takes its checkpoint and sends the checkpoint request to the processes it depends on using its dependency vector. It attaches the dependency vector to its request (Rule 3). 4. If a process P j receives a checkpoint request from a process P i then either of the following will happen:

-If it has already taken a checkpoint (cp taken j is true), then the request is ignored (Rule 4.1). -If it has not taken a checkpoint but has taken a mutable checkpoint (mcp taken j is true), then by receiving the request it converts the mutable checkpoint into a checkpoint. This conversion is not explicitly modeled but from now on cp taken j will be true. Further, P j propagates the checkpoint request to processes as follows. For each process P k on which P i does not depend on, but on which P j depended when it took the mutable checkpoint, P j sends a request to P k (P i has already sent a request to the processes on which it depends, Rule 4.2). -If it has neither taken a checkpoint or a mutable checkpoint, then it takes a checkpoint and propagates the request as in the previous case (Rule 4.3). 5. If a process P j removes a message (with attached flag) from a channel then either of the following will happen:

-If the received message has flag 0, then P j processes the message (Rule 2.1, Rule 2.2). If this happens before a mutable checkpoint or checkpoint is taken, then P j depends on P i and the dependency vector might need to be updated (Rule 2.1). -If the flag is 1 and P j has already taken a checkpoint, then P j processes the message (Rule 2.3). -If the flag is 1 and P j has neither taken a checkpoint nor mutable checkpoint, then it takes a mutable checkpoint and immediately after that processes the message (Rule 2.4). Taking the mutable checkpoint and processing the message is one atomic action. -If the flag is 1 and P j has taken a mutable checkpoint but not a checkpoint, then P j processes the message (Rule 2.5).

The Operational Behavior of Mutable Checkpointing

We specify the algorithm's behavior by a set of predicates and rules describing how the global state of the system changes with a transition. The rules of the following format:

Rule No. Preconditions Event Postconditions

If a global state S satisfies the precondition of a rule, then the event may occur and S is updated to T as specified in the field of postconditions. The occurrence of event e is written as

S e -→ T . So a distributed computation π = S 0 e1 -→ S 1 e2 -→ S 2 • • • e k
-→ S k is a sequence of such events where each of the transitions is justified by one of the rules. In some of the rules (Rules 1.2 and 2.2) the preconditions are split into two rows. These should be read as a disjunction, that is, each of these rules presents two rules with the same event name and postconditions. The possible events and messages of the mutable checkpointing algorithm are given by the following table. mcp taken i process P i takes a mutable checkpoint cp taken i P i takes the checkpoint send ij (.)

P i adds a message to channel C ij rec ij (.) P j receives a message or checkpoint request from channel C ij cpr i , dep the message that P i has taken a checkpoint with attached dependency vector msg, bb a message and attached flag

In the algorithm every local process maintains a dependency vector dep in which it keeps the dependencies to other processes: dep j (i) = 1 if P j has received a message from P i before a mutable checkpoint has been taken. This dependency vector can be retrieved from the history of a process at any state. However, for clarity we explicitly mention it in the semantics.

The first element of a channel is at the rightmost position and provided by first and the remainder by rem. We use the simple dot to separate letters in a word. For the concatenation of words we use •. If an event occurs in the history of a process at state S then we state this as a predicate event S i . For example, ¬mcp taken S i stands for that mcp taken i does not occur in the history p S i . It represents that P i has not taken a mutable checkpoint so far. The cp taken S i predicate, however, is more general as it also needs to cover the conversion of a mutable checkpoint to a (proper) checkpoint. Hence, cp taken S i if and only if either cp taken i occurs in the history of P i or mcp taken S i and rec ji ( cpr j , dep ) S for some j.

Rules are grouped according to their functionality.

Main Results

We here define the potential snapshot and show how it progresses with the underlying computation. With this invariant result we will show the reachability of the snapshot finally calculated.

As already discussed, in mutable checkpointing the potential snapshot psn(S) extracted from an intermediate state S of the underlying computation cannot simply be a global state containing the current local checkpoints. At S there is

No Preconditions Event Postconditions 1.1 ¬cp taken S i S send ij ( msg,0 ) -→ T p T i = p S i .send ij ( msg, 0 ) ¬mcp taken S i C T ij = msg, 0 .C S ij 1.2 cp taken S i S send ij ( msg,1 ) -→ T p T i = p S i .send ij ( msg, 1 ) mcp taken S i C T ij = msg, 1 .C S ij 2.1 first(C S ij ) = msg, 0 S rec ij ( msg,0 ) -→ T p T j = p S j .recij( msg, 0 ) ¬mcp taken S j C T ij = rem(C S ij ) ¬cp taken S j dep T j (i) = 1 2.2 first(C S ij ) = msg, 0 S rec ij ( msg,0 ) -→ T p T j = p S j .recij( msg, 0 ) mcp taken S j C T ij = rem(C S ij ) first(C S ij ) = msg, 0 cp taken S j 2.3 first(C S ij ) = msg, 1 S rec ij ( msg,1 ) -→ T p T j = p S j .recij( msg, 1 ) cp taken S j C T ij = rem(C S ij ) 2.4 first(C S ij ) = msg, 1 S rec ij ( msg,1 ) -→ T p T j = p S j .mcp taken j .recij( msg, 1 ) ¬cp taken S j C T ij = rem(C S ij ) ¬mcp taken S j 2.5 first(C S ij ) = msg, 1 S rec ij ( msg,1 ) -→ T p T j = p S j .recij( msg, 1 ) ¬cp taken S j C T ij = rem(C S ij ) mcp taken S j 3 ¬cp taken S 1 S cp taken 1 -→ T p T 1 = p S 1 .cp taken 1 C T 1k = cpr 1 , dep S 1 .C S 1k for all k > 1 with dep S 1 (k) = 1 4.1 first(C S ij ) = cpr i , dep S rec ij ( cpr i ,dep ) -→ T p T j = p S j .recij( cpr i , dep ) cp taken S j C T ij = rem(C S ij ) 4.2 S cp taken j -→ T p T j = p S j .recij( cpr i , dep ).cp taken j first(C S ij ) = cpr i , dep C T ij = rem(C S ij ) ¬cp taken S j C T jk = cpr j , dep ∨ dep S j .C S jk ¬mcp taken S j for all k with dep(k) = 0, dep S j (k) = 1 4.3 S rec ij ( cpr i ,dep ) -→ T p T j = p S j .recij( cpr i , dep ) first(C S ij ) = cpr i , dep C T ij = rem(C S ij ) ¬cp taken S j C T jk = cpr j , dep ∨ dep S j .C S jk mcp taken S j for all k with dep(k) = 0, dep S j (k) = 1
Table 1. Rules 1.1, 1.2: A message can be sent at any time and the attached flag shows whether this happened before (bb=0) or after (bb=1) a checkpoint or mutable checkpoint was taken. Rules 2.1-2.5: A mutable checkpoint is taken if the flag of the received message is 1 and the receiving process has neither taken a checkpoint nor a mutable checkpoint so far. Rule 3: We assume that the checkpointing will always be initiated by P1. It sends the checkpoint request to all the processes it depends on and takes the checkpoint as part of one atomic action. Rules 4.1-4.3: Receiving, setting and propagating a checkpoint request is modeled as one atomic event. This event comprises of removing the request from the channel, taking the checkpoint and propagating the request and causal dependencies to the concerned processes. These are the processes on which the receiving process depends but which are not listed in the dependency array received with the incoming request. In case a mutable checkpoint had been taken, it is converted to a permanent one (this, however, is not explicitly modeled).

no clarity whether a mutable checkpoint should be considered as a checkpoint or simply be discarded since the future computation steps cannot be foreseen.

In psn(S) all options have to be simultaneously considered. Accordingly, psn(S) is a set of global states of which each corresponds to a different prediction with respect to the final conversion of mutable checkpoints to (proper) checkpoints. The formal definitions are given next. Note that all projection functions used in this paper are summarized in Figure 1. The freeze function allows one to cut down the history of individual processes to the point where they have taken a mutable checkpoint or a checkpoint. These points we call freeze points. In order to freeze a process P i all events after the freeze point need to be deleted from the history. In general, the freezing of P i may effect process P j as the latter may have received a message from P i sent after its freeze point. Processes that may be frozen are those in M CP (S) while those in CP (S) must be frozen if a freezing is to be conducted.

M CP (S) = {P i | mcp taken S i and ¬cp taken S i } CP (S) = {P i | cp taken S i }
Due to the various freezing options we obtain the set of potential snapshots:

P SN (S) = {f (A, S) | CP (S) ⊆ A ⊆ M CP (S) ∪ CP (S)}
Each f (A, S) provides a potential snapshot at state S of which the processes in A are frozen.

f (A, S) =< p f (A,S) 1 , p f (A,S) 2 , . . . , p f (A,S) n , Chan f (A,S) > p f (A,S) i = p S i ↓ mcp,cp P i ∈ A p S i | A rem bb=1 P i / ∈ A Chan f (A,S) = {C f (A,S) ij | 1 ≤ i, j ≤ n and i = j} C f (A,S) ij =            C S ij | bb=0 o rev(p j ↑ i mcp,cp,bb=0 ) P i , P j ∈ A C S ij | bb=0 P i ∈ A, P j / ∈ A C S ij o rev(p j ↑ i mcp,cp ) P i / ∈ A, P j ∈ A C S ij P i / ∈ A, P j / ∈ A
where C ij removes all the coordination messages from the channel and rev reverses the string. Note that we do not explicitly remove the flag (which are used for coordination reasons only) from a message, but this is implied whenever coordination messages are removed.

To show the simultaneous progression of psn(S) with S e -→ S each of the states in psn(S) needs to be considered with respect to its corresponding move. If a mutable checkpoint has to be frozen then those states in psn(S) which had not predicted this are discarded. This means that the size of psn(S) can shrink. It will, however, grow with every new mutable checkpoint taken as the ↓mcp,cp It is applied to the local history of a process and yields the string of send and receive events before mcp taken or cp taken in their respective order. Only one of the latter events can occur in a history. | A rem bb=1 It is applied to the local history of a process not in A and removes all coordination messages and all messages with flag 1 received from a process in A. ↑ i mcp,cp It is applied to the local history of a process Pj and yields the string of messages in recij( msg, bb ) events after mcp taken or cp taken in their respective order. Only one of the latter events can occur in a history. ↑ i mcp,cp,bb=0 It is applied to the local history of a process Pj and yields string of messages in recij( msg, 0 ) events after mcp taken or cp taken in their respective order. Only one of the latter events can occur in a history. | j sent It is applied to the local history of a process Pi and yields the string of messages occurring in send ij ( msg, bb ) events in their respective order. | bb=0 This projection is applied to strings of messages, only. It removes from the string all coordination messages and messages with attached flag 1. concerned process will now have to be considered as progressing and as frozen, simultaneously. The next lemma describes this progression in detail.

Lemma 1. Let S 0 -→ * S and S e -→ S where e is an event of P i , i ∈ {1, . . . , n}. Then for all freeze sets A of S the following holds:

1. P i ∈ A implies f (A, S) = f (A, S ) 2. P i / ∈ A implies
. f (A, S) e -→ f (A, S ) ii. f (A, S) = f (A ∪ {P i }, S ) if ¬mcp taken S i (e) e i = rec ji ( msg, 1 ), P j ∈ A, and i. f (A, S) = f (A, S ) ii. f (A, S) = f (A ∪ {P i }, S ) if ¬mcp taken S i 3. p f (A ,S ) k = p S k if P k / ∈ A , ¬ mcp taken S k , ¬ cp taken S k and A is a freeze set of S
where A ∪ {P i } is a freeze set of the respective state whenever given as an argument to the freeze function.

Proof. By induction on the number of transitions leading from S 0 to S. If there is no transition then S 0 = S and A = ∅. Of item 2. only 2.(a) and 2.(c) apply which can be easily verified, and item 3. is trivial. Now suppose the induction hypothesis applies to S 0 → * S and there is one more transition S e -→ S . We have to explore all freeze sets of the relevant state and all the possible transitions.

We sketch two cases, for all others we refer to [START_REF] Aggarwal | Analyzing Mutable Checkpointing via Invariants (full version)[END_REF]. Proof of item 2.(c) for Rule 4.2. Rule 4.2 deals with the case e = cp taken i , first(C S ji ) = cpr j , dep , ¬cp taken S i and ¬mcp taken S i . Let A be a freeze set of S.

p f (A∪{Pi},S ) i = p S i ↓ mcp,cp = p S i .rec ji ( cpr j , dep .cp taken i ) ↓ mcp,cp = p S i def. ↓ mcp,cp = p f (A,S) i ind. hyp. 3.
The proofs for the other p k , k = i, and the channels are similar. Proof of item 3. for Rule 4.2. Let A be a freeze set of S . Then A \ {P i } is a freeze set of S, and by induction hypthesis 2.(c),

f (A \ {P i }, S) = f (A , S ). Let P k / ∈ A , ¬ mcp taken S k and ¬ cp taken S k . p f (A ,S ) k = p f (A \{Pi},S) k ind. hyp. 2.(c), already established = p S k ind. hyp. 3. = p S k
Note again, that in the lemma notationally we did not distinguish between a message with or without flag. However, in all events performed by a frozen process the flags have been removed. Similarly, in the next lemma denotes the prefix relation up to messages with or without flags. We further do not distinguish between S 0 and f (∅, S). Lemma 2 summarizes the invariant property of reachable states relevant for the consistency proof of the final snapshot. It is an immediate corrollary of Lemma 1 and the basic definitions.

Lemma 2. Let π : S 0 → * S. If A is a freeze set of S then S 0 → * f (A, S) and (1)
p f (A,S) k p S k for P k ∈ A, (2)
p f (A,S) k = p S k for P k / ∈ A, ¬ mcp taken S k and ¬ cp taken S k , (3) p
f (A,S) k = p S k | A rem bb=1 for P k / ∈ A, mcp taken S k or cp taken S k .
Lemma 2 shows that each f (A, S) is reachable. This, however, does not mean that f (A, S) is consistent with π since events of frozen processes are removed from the history and may create "holes". One may argue that the states to be considered here should be those with all none-frozen processes reset to their initial states. This would avoid the "hole" problem. For an arbitrary set of processes I, I ⊆ {P 1 , . . . , P n }, the reset of I at S is defined by

p r (I ,S ) i = p S i if P i / ∈ I, ε otherwise and C r (I ,S ) ij =    C S ij P i , P j / ∈ I, p S i | j sent P j ∈ I, ε P i ∈ I.
In general, r (I , S ) is not a consistent state. This is always the case if a process in I had sent a message to a process not in I and this message had been received before the resetting. It would become an orphan. This problem does not occur if S is the final state of a computation with completed checkpointing. The checkpointing is complete if there is no coordination message in any of the channels (recall that taking a checkpoint and propagating it further is an atomic event). The final snapshot T is defined by resetting all processes that have not taken a checkpoint at S to their starting point. So, in this case I = CP (S), the complement set of CP (S).

Theorem 1. Let π be a distributed computation from S 0 to S with completed checkpointing. Then the final snapshot T obtained by resetting to the initial state all processes that have not taken a checkpoint at S is consistent with π.

Proof. The final snapshot is defined by T := r (CP (S ), f (CP (S ), S )). The histories of T are given by

p T i = p f (CP (S),S) i if P i ∈ CP (S), ε otherwise.
By Lemma 2 we know that f (CP (S), S) is reachable from S 0 as CP (S) is a freeze set of S. So there is a computation

π = S 0 e1 -→ U 1 e2 -→ . . . em -→ U m = f (CP (S), S).
Let I stand for CP (S). From π we extract the computation which restricts to events performed by processes not in I, only.

S 0 ẽ1 -→ r (I , U 1 ) ẽ2 -→ . . . ẽm -→ r (I , U m )
where r (I , U t ) ẽt+1 -→ r (I , U t+1 ) stands for r (I , U t ) = r (I , U t+1 ) if e t+1 is an event of a process in I, and for r (I , U t ) ẽt+1 -→ r (I , U t+1 ) otherwise. For the former case there is nothing to prove, so consider the case e t+1 is performed by a process outside I. Again, if e t+1 is not of the form rec ij (msg) where P i ∈ I, P j ∈ CP (S), the transition can obviously be performed. for the case e t+1 = rec ij (msg), P i ∈ I, P j ∈ CP (S) we show that it cannot occur. So suppose there was such an event, then

p Ut+1 j = p Ut j .rec ij (msg) p Ut j .rec ij (msg) p f (CP (S),S) j by Rule 2.1 (1)
This implies rec ij ( msg, 0 ) is in the history of p S j (by ( 1) and ( 2)) and occurs before mcp taken S i or cp taken S i (by ( 1) and ( 3)). Hence, by Rule 2.1, dep S j (i) = 1. Thus, since P j had taken a checkpoint after the receive event it had also sent a cpr j to P i . Now, as P i ∈ I, this event had not been received and must therefore be in C S ji . This, however, contradicts that the checkpointing was complete. Like mutable checkpointing, the blocking queue algorithm in [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF] aims at a reduced coordination overhead. It assumes the same system model. The main difference is that the receipt of flagged messages which would lead to mutable checkpoints are buffered in so-called blocking queues and are not processed until the necessary checkpoints have been taken. This can be viewed as blocking channels or blocking processes partially. Mutable checkpointing neither blocks channels nor processes but, in general, it takes mutable checkpoints which if not converted to checkpoints need to be discarded after completion of the checkpointing (i.e. after phase I). A garbage collection is not required in the blocking queue algorithm, but the blocking queues need to be cleared. The snapshots determined by the two algorithms over the same underlying computation, in general, are incomparable. That is, it is not the case that a checkpoint taken in mutable computing is always equal or earlier than the corresponding checkpoint in the blocking queue setting, or vice versa. It may even happen that a process takes a checkpoint in one setting but not in the other. We discuss this next. It should be clear that a converted mutable checkpoint can be earlier than the corresponding checkpoint taken by the blocking queue algorithm. A computation in which a process takes a checkpoint in the blocking queue algorithm but not in mutable checkpointing is illustrated in Figure 2. We use M to depict a mutable checkpoint, M for a mutable checkpoint converted to a checkpoint, and ⊗ for a (regular) checkpoint. Arcs with numbers reflect messages and their flag. Checkpoint requests are indicated by cpr. In Figure 2, the checkpoint of P i in the blocking queue algorithm has no counterpart in mutable checkpointing. Such checkpoints, however, can lead to earlier checkpoints in the blocking queue algorithms and in turn lead to fewer checkpoints than in mutable checkpointing. With regard to the potential snapshots, it has been established in [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF] that the potential snapshots of the blocking queue algorithm are always consistent, contrasting the general inconsistency of the potential snapshots of mutable checkpointing shown here. In particular, the former implies that one can always only reset those processes for which a checkpoint has been taken without losing consistency. In mutable checkpointing the processes not taking part in the checkpointing also need to be reset as they may have received messages sent out after a checkpoint. Similarly, the garbage collection after phase I does also involve the non-participating processes while for clearing the blocking queues it is sufficient for the participating processes to send a respective clearing message. For mobile computing environments the blocking queue algorithm seems therefore preferable, but it comes together with the temporary buffering and delaying of messages. The comparison is summed up in Table 2. Note, that we did not discuss autonomy of processes here as it is a feature present in [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF] independent of the others (but it utilizes the blocking queues). In brief, it allows processes not to take a checkpoint immediately but to postpone it to a time more suitable.

Conclusions

We gave a concise specification of the operational behavior of mutable checkpointing, set up an invariant for the reachable states (Lemma 2) and utilized it for the correctness proof of the final snapshot. We extracted the specification of the operational behavior from the pseudo code in [START_REF] Cao | Checkpointing with mutable checkpoints[END_REF]. With our translation we omitted a feature not part of the mutable checkpointing concept (the sent i condition) and in this way obtained a more concise presentation of the algorithm. This feature, however, reduces the number of checkpoints further. It needs to be worked out how it reflects in the potential snapshot.

Taking aside the initial work [START_REF] Chandy | Distributed snapshots: determining global states of distributed systems[END_REF] most papers on checkpointing prove correctness by contradiction. We believe that a direct approach provides more insight into an algorithm. It can also form the basis of a tool-supported proof as recently shown in [START_REF] Andriamiarina | Revisiting snapshot algorithms by refinement-based techniques Computer Science and Information Systems[END_REF] for Chandy/Lamport's snapshot algorithm (among others). The set-up in [START_REF] Andriamiarina | Revisiting snapshot algorithms by refinement-based techniques Computer Science and Information Systems[END_REF] is based on the Event-B modelling language [START_REF] Cansell | The Event-B modelling method -concepts and case studies[END_REF] and very similar to ours. Whether the proof given in this paper can be mechanized in a similar way is subject of future work.

A concise formal model can be the base of qualitative comparisons which would add to existing quantitative comparisons based on simulations, like [START_REF] Agbaria | Model-based performance evaluation of distributed checkpointing protocols[END_REF][START_REF] Jiang | An optimistic checkpointing and message logging approach for consistent global checkpoint collection in distributed systems[END_REF]. We gave such a comparison with the blocking queue algorithm introduced in [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF]. That algorithm is conceptually different -it employs partial buffering of channel contents -but the overall objective is the reduction of coordination overhead as for mutable checkpointing.

We further showed that for a given underlying computation the respective snapshots may be incomparable. The potential snapshots of [START_REF] Kiehn | A causal checkpointing algorithm for mobile computing environments[END_REF] are always consistent unlike those of mutable checkpointing. Moreover, resetting processes and clearing blocking queues can be done in a localized way (that is involving only processes participating in the checkpointing). Hence, for computing environments in which the economic use of resources is crucial, the blocking queue algorithm seems preferable.

Recently, checkpointing has gained new attention in the area of high performance computing where fault tolerance techniques are essential [START_REF] Boutellier | Coordinated checkpoint versus message log for fault tolerant MPI[END_REF][START_REF] Elliot | Combining partial redundancy and checkpointing for HPC[END_REF][START_REF] Ljubuncic | Be kind, rewind: checkpoint & restore capability for improving reliability of large-scale semiconductor design[END_REF]. As the reduction of the coordination overhead may help to improve the overall performance, the algorithm discussed in this paper may be of interest there.

Fig. 1 .

 1 Fig. 1. Projection functions used in this paper.

  one of the following: (a) e / ∈ {cp taken i , rec ji ( cpr j , dep ), rec ji ( msg, 1 ) | j ∈ {1, . . . , n}}, and f (A, S) e -→ f (A, S ) (b) e = rec ji ( cpr j , dep ), mcp taken S i , and f (A∪{P i }, S) = f (A∪{P i }, S ) (c) e = cp taken i , ¬mcp taken S i , and f (A, S) = f (A ∪ {P i }, S ) (d) e = rec ji ( msg, 1 ), P j / ∈ A, and i

Fig. 2 .

 2 Fig. 2. a) Mutable checkpointing, b) blocking queue algorithm. Process Pi takes a checkpoint in in b), only.

Table 2 .

 2 Comparison of the two algorithms.

	Mutable Checkpointing Blocking Queue Algorithm
	blocking processes	no	no
	delaying processing of messages	no	yes
	PSN consistent	no	yes
	Actions to be taken after phase I discard unconverted	clear blocking queues
	mutable checkpoints
	Autonomy of processes	no	yes
	6 Comparison of Mutable Checkpointing with the
	Blocking Queue Algorithm


Jaber Karimpour
email: karimpour@tabrizu.ac.ir

Ayaz Isazadeh
email: isazadeh@tabrizu.ac.ir

Mohammadsadegh Mohagheghi

Khayyam Salehi
email: khayyam.salehi@gmail.com

Improved Iterative Methods for Verifying Markov Decision Processes

Keywords: Markov decision processes, probabilistic model checking, value iteration, policy iteration, graph partitioning, variable ordering

Value and policy iteration are powerful methods for verifying quantitative properties of Markov Decision Processes (MDPs). In order to accelerate these methods many approaches have been proposed. The performance of these methods depends on the graphical structure of MDPs. Experimental results show that they don't work much better than normal value/policy iteration when the graph of the MDP is dense. In this paper we present an algorithm which tries to reduce the number of updates in dense MDPs. In this algorithm, instead of saving unnecessary updates we use graph partitioning method to have more important updates.

Introduction

Markov Decision Processes (MDPs) are transition systems that can be used for modeling both nondeterministic and stochastic behaviors of reactive systems. In this paper we mainly focus on the quantitative verification of MDPs and consider reachability probabilities, i.e., calculating the maximum (or minimum) probability of reaching some goal states.

In general there are some main classic methods to solve MDPs: value iteration [START_REF] Baier | Principles of model checking[END_REF], Gauss-Seidel, policy iteration, and linear programming approach [START_REF] Puterman | Markov decision processes: discrete stochastic dynamic programming[END_REF]. Many researchers have tried to improve the performance of Value Iteration (VI) and Policy Iteration (PI) by reducing the number of updates of states [START_REF] Barto | Learning to act using real-time dynamic programming[END_REF][START_REF] Dai | Topological value iteration algorithms[END_REF][START_REF] Sanner | Bayesian real-time dynamic programming[END_REF][START_REF] Smith | Focused real-time dynamic programming for mdps: Squeezing more out of a heuristic[END_REF][START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF]. Although the main focus of so-called papers is on dealing with some problems in learning, one can use those techniques for quantitative verification of MDPs [START_REF] Brázdil | Verification of markov decision processes using learning algorithms[END_REF][START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF].

Experimental results show that when the graph of an MDP is dense or in the situation where all states belong to only one Strongly Connected Component (SCC), Gauss-Seidel version of VI works better than other advanced methods. In addition, a good variable ordering can accelerate iterative methods, but finding the optimal variable ordering for cyclic MDPs is an NP-complete problem [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF].

In this paper we concentrate on dense MDPs and consider maximum reachability probability problems (as defined in [START_REF] Baier | Principles of model checking[END_REF]). We present an algorithm that works faster than VI (and also faster than other methods). The main contribution is to present a prioritized algorithm for accelerating verification of dense MDPs.

The remainder of this paper is structured as follows. Section 2 formally defines MDPs and reviews PI algorithm. In Section 3 we present heuristics for variable reordering in both sparse and dense MDPs and then present a prioritized algorithm for dense MDPs. Section 4 summarises our experimental results and Section 5 presents conclusions and ideas for future research.

Preliminaries

In this section, we provide an overview of MDP and policy iteration method. Detailed definitions and topics are available in [START_REF] Baier | Principles of model checking[END_REF][START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF].

Markov Decision Processes (MDPs)

An MDP is a tuple M = (S, Act, P, AP, L), where S is a countable set of states, Act is a finite set of actions, P : S × Act × S → [0, 1] is the transition probability function such that for each state s ∈ S and each action α ∈ Act : s ∈S P (s, α, s ) ∈ {0, 1} , AP is a nonempty set of atomic propositions, and L : S → 2 AP is a labeling function.

For the sake of simplicity, we suppose that AP = {goal, non -goal} and there is a unique start state s 0 . For a state s ∈ S and an enabled action α ∈ Act, set of successors are defined as P ost(s, α) = {s ∈ S|P (s, α, s ) > 0} and P ost(s) = ∪ α∈Act P ost(s, α).

A path in an MDP is a non-empty (finite or infinite) sequence of the form:

s 0 α0 -→ s 1 α1 -→ s 2 α2 -→ • • •
where s i ∈ S and s i+1 ∈ P ost(s i , α) for each i > 0. We define P aths s as the set of infinite paths that start in s. To resolve nondeterministic choices in an MDP we require the notion of policy. A policy π selects an enabled action in each state based on the history of choices made so far (or simply the last state in memory-less policies). It restricts the behavior of the MDP to a set of paths paths π s ⊆ paths s . One can define a probability space P rob π s over the paths P aths π s [START_REF] Baier | Principles of model checking[END_REF]. For an MDP M we use Π M to denote the set of all policied of M .

MDPs can be used in the verification of systems (probabilistic verification). In this area, properties that should be verified against MDPs can be expressed using temporal logics such as PCTL [START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF]. In this paper, we concentrate on a limited yet important class of problems: maximum reachability probabilities, i.e. the maximum probability that a path through the MDP which starts from s 0 eventually reaches a goal state.

Quantitative Verification of MDPs

Model checking of PCTL formulas can be reduced to some important questions against MDPs. The maximum (or minimum) reachability probability is one of the most important questions against them. Given a set of goal states G ⊆ S, the maximum and minimum reachability probability can be defined as:

p min s (G) = inf π∈Π M p π s (G) and p max s (G) = sup π∈Π M p π s (G),
where p π s (G) = P rob π s ({ω ∈ P ath π s |∃i.ω i ∈ G}). As we have mentioned, there are some methods to compute reachability probabilities in MDPs but we only consider PI (because PI has better performance for dense MDPs).

Policy Iteration

Algorithm 1 describes the policy iteration method to calculate the values of p max s . This algorithm uses an array P to save the value p max si for each state s i . It first estimates a good policy (Line 8) and computes the value of states iteratively according to this policy (Lines 15-25). After reaching the threshold if the estimated policy is not optimal it will be improved and the iterative method continues. Act[s i ] saves the best estimated action for each state s i .

Algorithm1: Policy Iteration 1. Set initial values : P [s i ] = 1 if {s i ∈ G} and o . w . P [s i ] = 0. 2. diff1 := 1 3. while diff1 > epsilon do 4.
diff1 := 0; temp := 0; diff2 := 1 5.

for i := One of the main drawbacks of VI (and also PI) is that in every iteration it updates the values of all (nontrivial) states. Researchers proposed a range of methods to avoid unnecessary updates and speed up this algorithm. Some of these methods [START_REF] Dai | Topological value iteration algorithms[END_REF][START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF] try to split the MDP to some SCCs and in every iteration only compute the new value for states in some SCCs. Another approach for accelerating iterative methods is to consider a better variable ordering [START_REF] Dai | Topological value iteration algorithms[END_REF][START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF][START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF].

We review the idea of variable reordering and propose a heuristic algorithm for variable reordering in dense MDPs.

Variable ordering

The PI algorithm in Section 2 tries to use the update of states as soon as possible. In this case the order of updated states can influence the performance of algorithm. Let StatesOrder[s i ] be the array that determines the (static) order of states for update. When the value of a state is updated the new value can be propagated to next computation if the values of next states depend on the value of the current state. There are some heuristics for variable ordering in previous works [START_REF] Brázdil | Verification of markov decision processes using learning algorithms[END_REF][START_REF] Dai | Topological value iteration algorithms[END_REF][START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF][START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF], but none of them are useful for dense MDPs.

Here we propose an algorithm for variable reordering whose time complexity is linear in the size of the MDP. The idea of this algorithm is to select a state s for update where the most of states of P ost(s) have been updated before. The for loop in line 5 is used to guarantee the selection of all states.

Algorithm2: VariableReordering 1. for i := 0 to n -1 2.

Selected [ i ] := false ; 3. end for 4. left := right := 0; 5. for i := 0 to n -1 6.

if Selected [ i ] = false then 7.

Selected Policy iteration algorithm should call this function before the beginning of inner while loop (line 15 of Algorithm 1). In this case the VariableReordering function uses P ost(s j , Act[s j ]) (line 10 of algorithm 2). The for loop of line 18 (of algorithm 1) should be in reverse order and the state s i could be selected according to the StateOrder array:

for i := number_of_states down to 1

s i = StateOrder[i];
This algorithm is useful for sparse MDPs but in order to deal with dense MDPs we modify the Post set in line 10. Given t < 1 as a threshold, we define P ost(s i , α, t) = {s j |P (s i , α, s j ) ≥ t}. The experimental results show that the good value for t is between 0.3 and 0.5. It causes the algorithm to consider more important transitions. Algorithm 2 is used as a precomputation for every policy modification and doesn't affect the correctness of the PI algorithm.

Prioritized Algorithm for PI

Prioritized algorithms [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF] in general try to focus on regions of the problem space that are more important and have the maximum effect on the whole problem. In this section we propose an algorithm that uses a simple graph partitioning method for prioritizing state updates.

Inspiring from the idea of SCC-based methods [START_REF] Kwiatkowska | Incremental quantitative verification for markov decision processes[END_REF] we propose an algorithm which uses a good heuristic to split the state space to some partitions and updates these states according to this partitioning. Let B be a partition. Define AverageT rans(s i , B) = S j ∈B P (si,Act(si),sj ) sizeof (B)

. Our method tries to make partitions where for each state s i and each partition B the value of AverageT rans(s i , B) is high if s i ∈ B and this value is low otherwise. In this case the partition that contains goal states is the most important and the frequency of updates for states of this partition should be more than the other two. We use this partitioning algorithm in the PI because for dense MDPs the performance of PI is usually better than the performance of VI.

We use an O(n 2 ) heuristic for graph partitioning of the MDP because its overhead in the case of dense MDPs is negligible for most case studies. There are some options for the size of partitions. In this paper we define 3 partitions and suppose that the size of the first partition is 25% and the second partition is 35% of all state space. Algorithm 3 describes this partitioning method and because of page limitation, we only present the code for the first partition (with 25% of states).

Algorithm3: Graph Partitioning 1. for i := 1 to number_of_states do 2.

Distance [ i ] := 0; 3. end for 4. for i := 1 to number_of_states do 5.

if s i is a goal state then 6.

Selected [ i ] := true ; 7.

for j := 1 to number_of_states do 8.

Distance

Experiments

We implemented the proposed and original iterative algorithms in C++ using MS Visual Studio 2010 and ran it on an Intel Core i3 processor with 4GB memory. In the sections that follow we first consider the proposed algorithm of Section 3.1 and then consider the algorithm of Section 3.2.

Results for the Variable Ordering Algorithm

We tested our modified ordering algorithm on some dense MDPs. These models are randomly generated problems with 100 states and 3 actions per state and a parameter λ. We created these MDPs such that for each state s i , the average of maximum value of P (s i , α, s i+1 ) is λ with standard deviation of 0.1. Table 1 shows results of running Policy Iteration with best and worst variable ordering and also a random variable ordering. For simplicity we only present number of iterations for the execution of PI with = 10 -6 . The impact of variable ordering for these case studies is considerable where the λ parameter is more than 30%.

Results for partitioning-based algorithms

SysAdmin problem [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF] is a good example of real problems that have dense MDPs. Because of relatively high number of actions per state, the performance of PI algorithm is better than VI and Gauss-Seidel. We used an implementation for the MDP of this problem that is developed by the authors of [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF].

We also defined one other MDP: M1 is a model that the probability of reaching to 20% of its states is about 8 times more than the probability of reaching other 80% of states. This model has 400 states where average number of actions per state is 3.

It has been shown that the performance of SCC-based methods is lower than standard iterative method for dense MDPs [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF]. Hence, we don't compare our algorithm with SCC-based methods. To compare it with learning based ones, we use the implementation of learning algorithms that the authors of [START_REF] Brázdil | Verification of markov decision processes using learning algorithms[END_REF] proposed.

Table 2 shows the results of running normal VI and PI methods and, our prioritized algorithm (PI with algorithm 3). We called our algorithm Prioritized PI (PPI). Because of high average number of actions per state, the running time of PI is less than VI. The results show that our prioritized algorithm reduces the running time for all models. While prioritized methods of [START_REF] Wingate | Prioritization methods for accelerating mdp solvers[END_REF] could not improve the performance of iterative methods for SysAdmin, our algorithm accelerates iterative computations for these models.

The main reason that the performance of learning based algorithms for dense MDP's is so low is that these methods doesnt usually propose good variable ordering for this class of MDPs.

  [ j ] += P (s j , Act[s j ], s i ); += P (s k , Act[s k ], s j ) + P (s j , Act[s j ], s k );This algorithm should be called before the second while loop (Line 15) in Algorithm 1. In order to use the result of this algorithm we modify Algorithm 1 and add the following statements after Line 18:

	9.	end for
	10.	end if
	11. end for
	12. for i := 1 to 0.25×number_of_states do
	13.	k := the index of non -selected state for which
		Distance [ k ] is maximum ;
	14.	Selected [ k ] := true ;
	15.	for j := 1 to number_of_states do
	16.	if Selected [ j ] = false then
	17. Distance [ j ] 18. end if
	19.	end for
	20. end for
	if i % 7 = 0
	update states of partition #3
	else if i % 7 = 2 or i % 7 = 5
		update states of partition #2
	else
		update states of partition #1
	end if
	end if

Table 1 .

 1 Results of Variable Ordering for Some Dense MDPs

	λ	0.9	0.7	0.5	0.3	0.2	0.1
	Random ordering 11.6K	5.5K	3.7K	2.9K	2.6K	2.5K
	Best ordering	1.7K	1.9K	2K	2.1K	2.2K	2.2K
	Worst ordering	20.5K	9.2K	5.6K	3.8K	3.2K	2.9K
	Best/random	0.147	0.364	0.568	0.758	0.846	0.88

The main contribution of this paper is that we present a prioritized algorithm for dense MDPs and show that it can reduce the running time of iterative methods for solving probabilistic reachability problems of this class of MDPs. An approach for future works is to use a good variable ordering in each partition in our prioritized algorithm. In addition, one can propose a better prioritized algorithm that outperforms other prioritized ones in both dense and sparse models.

While many of previous works focus on VI, we believe that variable reordering can improve the performance when it is used in PI. One can also improve the performance of PI for both dense and sparse MDPs and outperform the VI approach by using advanced methods for selection of good policies (like action elimination.)