Chicago Journal of Theoretical Computer Science

The MIT Press

Volume 1998, Article 4 ? December

ISSN 1073–0486. MIT Press Journals, Five Cambridge Center, Cambridge, MA 02142-1493 USA; (617)253-2889; journals-orders@mit.edu, journalsinfo@mit.edu. Published one article at a time in L^{A}TEX source form on the Internet. Pagination varies from copy to copy. For more information and other articles see:

• http://mitpress.mit.edu/CJTCS/

• http://www.cs.uchicago.edu/publications/cjtcs/

• ftp://mitpress.mit.edu/pub/CJTCS

• ftp://cs.uchicago.edu/pub/publications/cjtcs Kulkarni and Arora Multitolerance (Info)

The Chicago Journal of Theoretical Computer Science is abstracted or indexed in Research Alert,◯^{R}SciSearch,◯^{R}Current Contents◯^{R}/Engineering Computing & Technology, and CompuMath Citation Index.◯^{R}

\begin{matrix}c \\ ◯ \end{matrix}1998 The Massachusetts Institute of Technology. Subscribers are licensed to use journal articles in a variety of ways, limited only as required to insure fair attribution to authors and the journal, and to prohibit use in a competing commercial product. See the journal’s World Wide Web site for further details. Address inquiries to the Subsidiary Rights Manager, MIT Press Journals; (617)253-2864; journals-rights@mit.edu.

The Chicago Journal of Theoretical Computer Science is a peer-reviewed scholarly journal in theoretical computer science. The journal is committed to providing a forum for significant results on theoretical aspects of all topics in computer science.

Editor in chief: Janos Simon

Consulting editors: Joseph Halpern, Stuart A. Kurtz, Raimund Seidel

Editors:

Martin Abadi  Greg Frederickson John Mitchell
Pankaj Agarwal Andrew Goldberg Ketan Mulmuley
Eric Allender Georg Gottlob Gil Neiger
Tetsuo Asano  Vassos Hadzilacos David Peleg
Laszló Babai  Juris Hartmanis Andrew Pitts
Eric Bach  Maurice Herlihy James Royer
Stephen Brookes Ted Herman  Alan Selman
Jin-Yi Cai  Stephen Homer  Nir Shavit
Anne Condon  Neil Immerman  Eva Tardos
Cynthia Dwork Howard Karloff  Sam Toueg
David Eppstein Philip Klein  Moshe Vardi
Ronald Fagin  Phokion Kolaitis Jennifer Welch
Lance Fortnow Stephen Mahaney Pierre Wolper
Steven Fortune Michael Merritt

Managing editor: Michael J. O’Donnell

Electronic mail: chicago-journal@cs.uchicago.edu

[ii]

Multitolerance in Distributed Reset

Sandeep S. Kulkarni  Anish Arora

? December, 1998

Abstract

A reset of a distributed system is safe if it does not complete “pre-

Abstract-1

maturely,” i.e., without having reset some process in the system. Safe resets are possible in the presence of certain faults, such as process failstops and repairs, but are not always possible in the presence of more general faults, such as arbitrary transients. In this paper, we design a bounded-memory distributed-reset program that possesses two tolerances: (1) in the presence of fail-stops and repairs, it always executes resets safely, and (2) in the presence of a finite number of transient faults, it eventually executes resets safely. Designing this multitolerance in the reset program introduces the novel concern of designing a safety detector that is itself multitolerant. A broad application of our multitolerant safety detector is to make any total program likewise multitolerant.

1 Introduction

A principal requirement of modern distributed systems, such as the evolving

1-1

national and global information infrastructures, is robustness. Robustness implies that systems should be able to deliver their services in an appropriate manner in spite of variations in environmental behavior and occurrences of faults. Designing robustness in modern distributed systems is a challenging problem: not only is their scale unprecedented, but in a more fundamental sense, their characteristics are atypical in at least two ways: faults of various types are not only possible, but are likely to occur at some component or the other; and transient-system states are the norm and not the exception, since these systems are subject to constant change and evolution.

Kulkarni and Arora Multitolerance §1

1 In systems that are subject to multiple fault classes, designing the same

1-2

tolerance to all fault classes is often inappropriate, inefficient, or impossible. For example, in a system that is subject to timing glitches, configuration changes, and safety hazards, it may be desirable that the system recover from the first fault class, mask the second, and fail safely in the presence of the third. In such a system, it would be inappropriate to fail safely in the presence of all three fault classes, or it would be inefficient or impossible to mask all three fault classes. Thus, it is desirable that modern distributed systems be designed to be “multitolerant” [AK98a], that is, tolerant to each of a number of fault classes, in a manner that is best suited to each fault class.

In this paper, we present a bounded-memory multitolerant, distributed

1-3

program that enables the processes in a distributed system to reset the state of the system. We focus our attention on the so-called distributed-reset program [AG94], owing to its wide applicability in designing fault tolerance. We consider two fault classes, one of which effectively fail-stops or repairs processes, and the other of which transiently and arbitrarily corrupts the state of processes. Our program is masking tolerant to the first fault class, and stabilizing tolerant to the second.

Below, we first define the reset problem and what it means for a reset

1-4

program to be masking tolerant and stabilizing tolerant. We then describe the main difficulties involved in a bounded-memory reset program that is both masking tolerant and stabilizing tolerant.

Distributed Reset. A distributed-reset program consists of two mod-

1-5

ules at each process: an application module, and a reset module. The application module can initiate a reset operation to reset the program to any given global state. Upon initiation of the reset operation, the reset module resets the state of the application to a state that is reachable from the given global state, and then informs the application module that the reset operation is complete. In other words, each reset operation satisfies the following two properties:

• every reset operation is nonpremature, i.e., if the reset operation completes, the program state is reachable from the given global state; and

• every reset operation completes eventually, i.e., if an application module at a process initiates a reset operation, eventually the reset module at that process informs the application module that the reset operation is complete.

2 The definition captures the intuition that resetting the distributed pro-

1-6

gram to exactly the given global state is not necessarily practical nor desirable, since that would require freezing the distributed program while the processes are individually reset. The definition therefore allows the program computation to proceed concurrently with the reset, to any extent that does not interfere with the correctness of the reset.

Observe that to reset the program state to the given global state, the

1-7

application module at every process needs to be reset. Furthermore, if any two application modules communicate only if both have been reset in the same reset operation and all processes have been reset in a reset operation, then the current program state is reachable from the corresponding global state.

Masking Tolerance. The ideal fault tolerance for distributed reset is

1-8

masking tolerance. A reset program is masking tolerant to a fault class if every reset operation is correct in the presence of the faults in that class. In other words, the safety of distributed reset (i.e., that every reset operation is nonpremature) is satisfied before, during, and after the occurrences of faults. Also, the liveness of distributed reset (i.e., that every reset operation completes) is satisfied after fault occurrences stop.

Consider a fault that fail-stops a process and repairs it instantaneously.

1-9

It is possible to design masking tolerance to this fault. In fact, even if the fault only fail-stops processes or only repairs processes, it is still possible to design masking tolerance to the fault, with respect to the processes that are up throughout the reset operation. We therefore redefine a premature reset operation as follows: a reset operation is premature if its initiator completes it without resetting the state of all processes that are up throughout the reset operation. In the rest of the paper, we use this refined definition of premature reset.

Stabilizing Tolerance. An alternative fault tolerance for distributed

1-10

reset is stabilizing tolerance. A reset program is said to be stabilizing tolerant to a fault class if, starting from any arbitrary state, eventually the program reaches a state from where every reset operation is correct, i.e., the safety and liveness of distributed reset are satisfied.

Stabilizing tolerance is ideal when an arbitrary state may be reached in

1-11

the presence of faults. Arbitrary states may be reached, for example, in the presence of fail-stops, repairs, or message loss, as demonstrated by Jayaram and Varghese [JV96]. In such cases, masking tolerance cannot be designed, because the fault itself may perturb the program to a state where the reset

3 operation has completed prematurely.

Since arbitrary states can be reached in the presence of arbitrary transient

1-12

faults, the ideal tolerance to transient faults is stabilizing tolerance. From the definition of stabilizing tolerance, if the program is stabilizing tolerant to transient faults, it is also stabilizing tolerant to fail-stops and repairs. However, this is not the ideal tolerance to fail-stops and repairs.

Multitolerant Reset. As motivated above, the best-suited tolerance

1-13

to fail-stop and repair faults is masking, and the best-suited tolerance to transient faults is stabilizing. We therefore design a multitolerant program that offers the best-suited tolerance for each of these two classes. (Note that by being stabilizing tolerant to transient faults, our program is also stabilizing tolerant to fail-stops and repairs; therefore, it is both masking and stabilizing tolerant to fail-stops and repairs.)

It is important to emphasize that our reset program is not just a stabi-

1-14

lizing program. A reset program that is only stabilizing tolerant to fail-stops and repairs permits a reset operation to complete incorrectly in the presence of fail-stops and repairs. (All existing stabilizing reset programs in fact do so.) By way of contrast, our program ensures that in the presence of fail-stops and repairs, every reset operation is correct. In fact, as discussed below, designing a multitolerant reset program is significantly more complex compared to designing just a stabilizing reset program.

In principle, to design a multitolerant reset program, the initiator of the

1-15

reset operation needs to “detect” whether all processes have been reset in the current operation. For the program to be masking tolerant to fail-stops and repairs, this “detection” must itself be masking tolerant to fail-stops and repairs. Also, for the program to be stabilizing, this detection must itself stabilize if perturbed to an arbitrary state. Thus, the design of the multitolerant reset program involves the design of a multitolerant detector.

Also, adding such a multitolerant detector to a stabilizing reset program

1-16

is not sufficient for the design of a multitolerant reset program. Since the detector and the actions of the stabilizing program execute concurrently, the detector may interfere with the stabilizing program, making it nonstabilizing, and the stabilizing actions may interfere with the detector, causing incorrect detection. Thus, to design a multitolerant program, we also need to ensure freedom from interference between the detector and the actions of the stabilizing program.

Both these problems are further complicated if the program uses bounded

1-17

memory. In the masking reset, when the initiator completes the reset op-4 eration, it needs to check that all processes are reset in the current reset operation. To this end, each process detects whether all its neighbors have reset their states in the current reset operation. Using bounded sequence numbers to distinguish between different reset operations is tricky, because it is possible that multiple processes will have the same sequence number even if they were last reset in different reset operations.

(Notice that sequence numbers for old reset operations may exist in the

1-18

system. This is because some communication channels may be slower than others, communication channels may allow messages to be reordered, processes may repair with incorrect sequence numbers, or transient faults may arbitrarily corrupt the sequence numbers. In Section 5.2, we illustrate this with an example of multiple processes that end up with the same sequence number even though they have been reset in different reset operations.)

The complication due to bounded memory is more severe in designing

1-19

masking tolerance than in stabilizing tolerance, as the former requires that the detection be always correct, whereas the latter requires that the detection be eventually correct.

As discussed in Section 8, our bounded-memory multitolerant solution

1-20

for distributed reset is also useful in designing a bounded-memory multitolerant solution for any total program [Tel89], e.g., leader election, termination detection, or global snapshot. A total program characteristically has one or more “decider” actions whose execution depends on the state of all processes. The multitolerant detector in the reset program enables the design multitolerance in total programs so that in the presence of fail-stops and repairs, the decider actions always execute correctly, and after the occurrence of transient faults, the decider actions eventually execute correctly.

Related Work. To our knowledge, this is the first bounded-memory

1-21

multitolerant distributed-reset program. In fact, we are not aware of a bounded-memory distributed-reset program that is masking tolerant to failstops and repairs. We note that Afek and Gafni [AG91] have shown a masking-tolerant solution under the severe assumption that processes do not lose their memory if they fail. They do, however, allow channels to fail, and the messages sent on those channels to be lost. Their program is not stabilizing tolerant.

While little work has been done on bounded-memory masking tolerant

1-22

resets, bounded-memory stabilizing tolerant resets have received more attention [AG94, Var93, APSV91, APSVD94, AO94, AH93, DH97]. All of these programs are stabilizing tolerant to fail-stops and repairs, but they are

5 not masking tolerant to them. Specifically, in the presence of fail-stops and repairs, they allow premature completion of distributed resets.

Masuzawa has presented a reset program [TM94] that tolerates two fault

1-23

classes: transient faults and undetectable crash faults. His solution assumes that at most M processes fail undetectably for some fixed M such that the process graph is (M+1)-connected. While his solution ensures that in a reset operation eventually all processes are reset, it permits premature completion of a reset operation. Also, his solution uses unbounded memory.

Outline of the Paper. In light of the above discussion, we design a dis-

1-24

tributed reset program that (1) is masking tolerant to fail-stops and repairs,

(2) is stabilizing tolerant to transient faults, and (3) has bounded space complexity. Using a stepwise approach for designing multitolerance, we proceed as follows: first, we design a fault-intolerant program for distributed reset. Then, we transform this program so as to add masking tolerance to fail-stops and repairs. Masking tolerance is itself added in two stages. In the first stage, we add nonmasking tolerance to fail-stops and repairs. The nonmasking program ensures that starting from a state reached as a result of fail-stops and repairs, the program eventually reaches a state from where every reset completes correctly. Until such a state is reached, however, some resets may complete incorrectly. In the second stage, we add the multitolerant detector that lets the initiator detect whether or not the reset is premature. If the reset is premature, the initiator repeats the reset operation. Finally, we transform this program again so as to add stabilizing tolerance to transient faults, while ensuring that the masking tolerance to fail-stops and repairs is preserved. (The interested reader is referred to [AK98a] for the foundations of this stepwise design of multitolerance.)

The rest of the paper is organized as follows: in Section 2, we define

1-25

programs, faults, and fault tolerances, and state our assumptions about distributed systems. In Section 3, we give an outline of our solution and its proof of correctness. In Section 4, we develop the fault-intolerant program for distributed reset. In Section 5, we transform the fault-intolerant program to add masking tolerance to fail-stops and repairs. In Section 6, we transform the masking-reset program to add stabilizing tolerance to transient faults. In Section 7, we describe how this reset program can be used to design multitolerant application programs. Finally, we make concluding remarks in Section 8.

6

2 Preliminaries

In this section, we first recall a formal definition of programs, faults, and fault

2-1

tolerances [AG93]. We then state our assumptions about the distributed systems considered in this paper.

Programs. A program is a set of variables and a finite set of actions.

2-2

Each variable has a predefined domain. Each action is uniquely identified by a name, and is of the form:

⟨name⟩ :: ⟨guard⟩ ⟶ ⟨statement⟩

The guard of an action is a boolean expression over the program variables.

2-3

The statement of an action updates zero or more program variables. An action can be executed only if its guard evaluates to true. To execute an action, the statement of that action is executed atomically.

State and State Predicate. A state of program p is defined by a value

2-4

for each variable of p, chosen from the predefined domain of the variable. A state predicate of p is a Boolean expression over the variables of p. We say that an action of p is enabled in a state if and only if its guard evaluates to true in that state.

Closure. Let S be a state predicate of p. An action of p preserves S if

2-5

and only if in any state where S holds and the action is enabled, executing the statement of the action atomically yields a state where S holds. In a set of actions, S is closed in a set of actions if and only if each action in that set preserves S.

Computation. A computation of p is a fair, maximal sequence of steps;

2-6

in every step, an action of p that is enabled in the current state is chosen, and the statement of that action is executed atomically. Fairness of the sequence means that each action in p that is continuously enabled along the states in the sequence is eventually chosen for execution. Maximality of the sequence means that if the sequence is finite, then the guard of each action in p is false in the final state.

The Invariant Predicate. One state predicate of p is distinguished as

2-7

its invariant. The invariant predicate of p holds at all states reached by the computations of p which meet the problem specification that p satisfies. Thus, informally speaking, the invariant predicate characterizes the set of all states reached in the “correct” computations of p.

We assume that in all computations of p that start from a state where the

2-8

invariant holds, the invariant predicate holds throughout. In other words, the 7 invariant predicate of p is closed in p. Note that many other state predicates may be closed in p, some of which may not be true at states where the invariant holds; the state predicate false provides a trivial example of such a predicate.

Techniques for the design of the invariant predicate have been articu-

2-9

lated by Dijkstra [Dij76], using the notion of auxiliary variables, and by Gries [Gri81], using the heuristics of state-predicate ballooning and shrinking. Techniques for the mechanical calculation of the invariant predicate have been discussed by Alpern and Schneider [AS87].

Convergence. A state predicate Q converges to a state predicate R in p

2-10

if and only if Q and R are closed in p, and starting from any state where Q holds, every computation of p reaches a state where R holds.

Faults. The faults that a program is subject to are systematically rep-

2-11

resented by actions that perturb the state of the program. We emphasize that such representation is readily obtained for a variety of fault classes, including stuck-at, crash, fail-stop, repair, message loss, message corruption, timing faults, and Byzantine. Also, such a representation is readily obtained for faults of different natures, such as permanent, transient, and intermittent faults.

The Fault Span. The fault span of p, with respect to a set of fault actions

2-12

F, is a predicate that characterizes the set of all states reached when the computations of p are subject to the occurrence of faults in F. Thus, if an enabled action is executed in a state where the fault span holds, the resulting state satisfies the fault span. Also, if a fault in F occurs in a state where the fault span holds, the resulting state also satisfies the fault span. In other words, the fault span of p with respect to a set of fault actions F is closed in both p and F.

Fault Tolerances. Let p be a program with the invariant S, and let F be

2-13

a set of fault actions. We say that “p is F -tolerant for S” if and only if there exists a state predicate T of p that satisfies the following three conditions:

• inclusion: T ⇐S,

• closure: T is closed in F, and

• convergence: T converges to S in p.

This definition may be understood as follows. At any state where the

2-14

invariant S holds, executing an action in p yields a state where S continues

8 to hold. However, executing an action in F may yield a state where S does not hold. Nonetheless, the following three facts are true about this resulting state : (1) T, the fault span, holds; (2) subsequent execution of actions in p and F yields states where T holds; and (3) when actions in F stop executing, subsequent execution of actions in p alone eventually yields a state where S holds, from which point the program resumes its intended execution.

In the context of multitolerance, it is important to note that there may

2-15

be multiple predicates T for which p satisfies the above three conditions. Moreover, there may be multiple fault classes F for which p is F -tolerant.

When the invariant S is clear from the context, we omit S. Thus, the

2-16

statement “p is F -tolerant” abbreviates “p is F -tolerant for the invariant of p.”

Types of Fault Tolerances. The definition of fault tolerance lets us

2-17

formally distinguish various types of fault tolerances, such as masking, nonmasking, and stabilizing:

1. When the definition is instantiated so that T is identical to S, p is masking tolerant to F. In other words, p is masking tolerant to F if S is closed in F; i.e., if a fault in F occurs in a state where S holds, the resulting state continues to satisfy S.

2. When the definition is instantiated so that T differs from S, p is nonmasking tolerant to F. In other words, p is nonmasking tolerant to F if when a fault in F occurs in a state where S holds, the resulting state may violate S; however, the resulting state satisfies T, and the continued execution of p alone yields a state where S is (re)satisfied, from which point the program resumes its intended execution.

3. When the definition is instantiated so that T is identical to true, p is stabilizing tolerant to F. In other words, p is stabilizing tolerant to F if when p reaches an arbitrary state, continued execution of p alone yields a state where S is (re)satisfied.

Multitolerance. Let p be a program with invariant S. Let

2-18

F 1, F 2, ..., F n be n fault classes. We say that p is multitolerant to F 1, F 2, ..., F n if and only if for each fault class F j, p is F j-tolerant for S.

Informally, the definition can be understood as follows: in the presence

2-19

of faults in F j, the program is perturbed to a state where the fault span T j

9 holds. After faults in F j stop occurring, p recovers to a state where S is (re)satisfied. It is important to note that T j may be different for each fault class F j, and for each F j, the tolerance of p to F j may also be different.

This definition of multitolerance captures that the effect of different fault

2-20

classes may be different. For example, in our reset program, we consider two sets of fault classes: (1) fail-stop and repair of processes, and (2) transient faults. Since the program is masking tolerant to the first fault class, the fault span in the prsence of fail-stop and repair will satisfy so that no reset completes prematurely. The program is stabilizing tolerant to the second fault class. Thus, the fault span in the presence of transient faults, namely, true, may allow a reset to complete prematurely.

System Assumptions. A distributed system consists of processes, each

2-21

with a unique integer identifier, and bidirectional channels, each connecting a unique pair of processes. At any time, a process is either up or down. Only up processes execute their actions.

As mentioned previously, system execution may be affected by faults.

2-22

These faults may fail-stop and repair processes, or arbitrarily corrupt the state of the system. Faults may occur in any finite number, in any order, and at any time, but they may never partition the graph of up processes.

Remark 1 Henceforth, we use the terms “process” and “up process” interchangeably. Also, when the context is clear, we use “process” to mean the “reset module of the process.”

3 Outline of the Solution

Recall that in accordance with our approach to designing multitolerance we

3-1

first design a fault-intolerant reset program, then transform this program to add masking tolerance to fail-stops and repairs, and finally add stabilizing tolerance to the program while ensuring that the masking tolerance to failstops and repairs is preserved. In this section, we outline the structure of each of these three programs and their proofs of correctness.

The Fault-Intolerant Program. We use a variation of the diffusing com-

3-2

putation program. In particular, we use a tree that spans all up processes in the system, and perform the reset-diffusing computation only over the tree edges. The root of the tree initiates the diffusing computation of each reset. When a process receives a diffusing computation from its parent in the tree, it resets its local state, and propagates the diffusing computation to its

10 children in the tree. When all descendents of process j have reset their local states, j completes its diffusing computation. Thus, when the root completes the diffusing computation, all processes have reset their local states.

Adding Masking Tolerance. In the presence of fail-stops and repairs, the

3-3

tree may become partitioned. Hence, the diffusing computation initiated by a root process may not reach all processes in the system.

To add masking tolerance, it suffices that we ensure the following two

3-4

conditions for every distributed reset:

1. eventually, the local states of all processes are reset, and

2. in the interim, no diffusing computation completes incorrectly.

To achieve condition 1, we ensure that eventually the tree spanning all

3-5

up processes is restored, so that a diffusing computation can reach all up processes. To this end, we reuse a nonmasking-tolerant tree program due to Arora [Aro94] that, in the presence of fail-stops and repairs, maintains the graph of the parent relation of all up processes to always be a forest, and when faults stop occurring, restores the graph to be a spanning tree. The details of this program are given in Section 5.1.

To achieve condition 2, we ensure that when the root process completes a

3-6

diffusing computation, it can detect whether all processes participated in that diffusing computation. Suppose that some processes have not participated when the root completes: since the up processes remain connected in the presence of fail-stops and repairs, it follows that there exists at least one pair of neighboring processes j and k such that j participated in the diffusing computation but k did not. To detect such pairs, a “result” is associated with each diffusing computation: process j completes a diffusing computation with the result true only if all its neighbors have propagated the diffusing computation, and hence, reset their local states. Otherwise, j completes the diffusing computation with the result false. The result is propagated in the completion wave of the diffusing computation. In particular, if j has completed a diffusing computation with the result false, then the parent of j completes that diffusing computation with the result false, and so on. Also, if j fails or moves to a different tree, then the (old) parent of j cannot always determine the result of j. Hence, when j fails or moves to a different tree, the parent of j completes with the result false. It follows that when the root completes the diffusing computation with the result true, all processes have participated in the diffusing computation.

Kulkarni and Arora Multitolerance §3.1

11 Finally, if a root completes a diffusing computation with the result false,

3-7

it starts a new diffusing computation. Since the nonmasking-tolerant tree program eventually spans a tree over the up processes, in any diffusing computation initiated after the tree is constructed and during which no failures occur, the distributed reset completes correctly.

(We reemphasize that the challenging part of this solution is how j

3-8

decides—with a bounded sequence number—whether its neighbors have propagated the same diffusing computation as j has, and not just an old diffusing computation with the same sequence number. We discuss the issue of boundedness in Section 5.2.)

Adding Stabilizing Tolerance. To design stabilizing tolerance into the

3-9

program, we add convergence actions that ensure that eventually the program reaches a state from where subsequent resets will complete correctly. In particular, in the presence of transient faults, the graph of the parent relation may form cycles, and so we add actions to detect and eliminate cycles in the graph of the parent relation. While adding stabilizing tolerance to transient faults, we preserve the masking tolerance to fail-stops and repairs by ensuring that the convergence actions and the actions of the masking program do not interfere. The details of this program are given in Section 6.

3.1 Outline of the Proof

In accordance with the formal definition of a fault-tolerant program given in

3.1-1

Section 2, the proof of correctness of all programs in this paper is given in terms of their invariant and fault-span predicates.

For the fault-intolerant program R, we exhibit an invariant S_{R}. In other

3.1-2

words, we show that if the program is executed in a state where S_{R} holds, then the resulting state satisfies S_{R}. Also, when the root completes the diffusing computation in a state where S_{R} holds, the state of the system is reachable from the given global state.

In the presence of fail-stops and repairs, program R may be perturbed to

3.1-3

a state where the predicate S_{R} may be violated. Let T_{R} denote the predicate characterizing the set of states reached by program R in the presence of failstops and repairs. As mentioned above, to add masking tolerance to fail-stops and repairs, we add actions to detect whether all processes participated in a reset wave. Let D denote the invariant of these detection actions added to R to obtain the masking-tolerant program MR. Thus, for MR, the invariant is S_{MR}, S_{MR} = T_{R} ∧ D. By definition, the fault span of MR is identical

12 to S_{MR}. In other words, we show that if an action of MR is executed or a fail-stop/repair fault occurs in a state where S_{MR} holds, the resulting state satisfies S_{MR}. Also, when the root completes the diffusing computation in a state where S_{MR} holds, the state of the system is reachable from the given global state.

In the presence of transient faults, program MR may be perturbed to

3.1-4

an arbitrary state. Hence, the fault span of our stabilizing-tolerant program, MSR, is the predicate true. The invariant of the stabilizing-tolerant program is the same as that of the program MR, i.e., S_{MR}. As mentioned above, to add stabilizing tolerance to transient faults, we add convergence actions to program MR to ensure that upon starting from an arbitrary state, eventually a state satisfying S_{MR} is reached. After the program reaches a state where S_{MR} is satisfied, when a root completes the reset wave, the state of the system is reachable from the given global state. We also ensure that program MSR is masking tolerance to fail-stops and repairs. To this end, we show that the convergence actions preserve S_{MR} and do not execute indefinitely after the program reaches a state where S_{MR} holds. Hence, eventually only the actions of MR are executed. It follows that eventually a root process will declare that the reset is complete.

4 Fault-Intolerant Distributed Reset

In this section, we describe a straightforward distributed-reset program in

4-1

terms of a diffusing computation over a rooted spanning tree. For simplicity, we assume that only the root process of the tree initiates distributed resets.

When the root process initiates a distributed reset, it marks its state as

4-2

reset, resets its local state, and propagates a reset wave to its children in the tree. Likewise, when a process j receives a reset wave from its parent, j marks its state as reset, resets its local state, and propagates the reset wave to its children. We refer to these propagations as the propagation of the reset wave.

When a leaf process j propagates a reset wave, j completes the reset wave,

4-3

marks its state as normal, and responds to its parent. When all children of process j have responded, j completes the reset wave, and responds to its parent. We denote these completions as the completion of the reset wave.

It follows that when a process completes a reset wave, all its descen-

4-4

dents have completed that reset wave. In particular, when the root process

13

Stabilizing and Masking Program MSR Masking Program MR Fault-Intolerant Program R^{Stabilizing tolerant to transient faults (fault span = true)}^{Masking tolerant to fail-stops and repairs (fault span = S_{MSR})}^{Invariant = S_{MSR}}^{Masking tolerant to fail-stop and repair (fault span = S_{MR})}^{Invariant = S_{MR}}^{Invariant = S_{R}}

Figure 1: Structure of the program and its proof 14

Chicago Journal of Theoretical Computer Science 1998-4 completes the reset wave, all processes have completed the reset wave, and the root process can declare that the distributed reset has been successfully completed.

Variables. As described above, every process j maintains the following

4-5

variables:

• st.j, the state of j: the state is reset if j is propagating a reset wave; otherwise, it is normal;

• sn.j, the sequence number of j: the sequence number of j is either 0 or 1; and

• par.j, the parent of j: the parent of the root process is set to itself.

Actions. As described above, program R consists of three actions at

4-6

each process j. Action R1 lets j initiate a new reset wave if j is a root process. Action R2 lets j propagate a reset wave if par.j is propagating a reset wave and the sequence numbers of j and par.j are different. Action R3 lets j complete a reset wave if j is in the reset state and all children of j have completed in that reset wave; if j is a root process, j also declares that the distributed reset is complete.

Formally, the actions of the program at process j are shown in Figure 2

4-7

(let ch.j denote the set of children of j):

R1 :: par.j = j ∧ st.j = normal ∧ {j needs to initiate a new reset wave} ⟶ st.j, sn.j := reset, sn.j⊕1; {reset local state of j}

R2 :: st(par.j)=reset ∧ sn.j ≠sn.(par.j)

⟶ st.j, sn.j := reset, sn.(par.j); {reset local state of j}

R3 :: st.j = reset ∧ (∀k : k ∈ch.j : sn.j =sn.k ∧ st.k ≠reset) ⟶ st.j := normal; {if par.j =j, then declare reset complete}

Figure 2: Actions of program R at process j

Invariant. Observe that if both j and par.j are propagating a reset wave,

4-8

then they have the same sequence number. Also, if par.j is in the normal 15 state, then j is also in the normal state and has the same sequence number as par.j. Hence, the predicate GD = (∀j :: Gd.j) is in the invariant of the program, where:

Gd.j = ((st.(par.j) = reset ∧ st.j = reset) ⇒ sn.j = sn.(par.j)) ∧ ((st.(par.j) ≠ reset) ⇒ (st.j ≠ reset ∧ sn.j = sn.(par.j)))

Moreover, the invariant of the program is:

4-9

S_{R} = GD ∧ graph of the parent relation forms a tree.

Remark 2 Although, for simplicity, we assumed that the reset request was initiated by the root process, our program can be generalized to let any process initiate a reset wave. To this end, any request made by a process is propagated toward the root, which then performs the reset. This extension is identical to the one given in [AG94], and is not discussed in this paper.

5 Masking Fault-Tolerant Distributed Reset

In this section, we transform the fault-intolerant program of Section 4 to add

5-1

masking tolerance to fail-stop and repair faults. As described in Section 3, to add masking tolerance to fail-stop and repair faults, it suffices that:

• after faults stop occurring, the program eventually reaches a state from where no distributed reset ever completes incorrectly; and

• when a root process declares that a distributed reset has completed, all up processes have participated in that reset wave.

We design the masking-tolerant program in two stages. In the first stage,

5-2

we transform the fault-intolerant program to add nonmasking tolerance to fail-stop and repair faults. The nonmasking fault-tolerant program ensures that in the presence of fail-stop and repair of processes, the program eventually reaches a state from where no distributed reset will complete incorrectly. In the second stage, we transform the nonmasking fault-tolerant program into one that is masking-fault tolerant, by restricting the actions of the former program so that a process declares completion of a distributed reset only if all up processes have participated in the last reset wave. (The interested reader is referred to [AK98b] for the foundations of this two-stage method for adding masking tolerance.)

16 In Section 5.1, we design the nonmasking program to tolerate fail-stop and

5-3

repair faults. Then, in Section 5.2, we restrict the actions of the nonmasking program, so that the resulting program is masking-fault tolerant.

5.1 Nonmasking Fault-Tolerant Distributed Reset

Observe that if the program reaches a state where the invariant S_{R} holds,

5.1-1

then starting from such a state no distributed reset will complete incorrectly. To design a nonmasking-reset program for fail-stop and repair faults, we add convergence actions that restore the program to a state where S_{R} holds; i.e., we add actions that (re)construct the rooted spanning tree and restore Gd.j for every process.

To construct a spanning tree, we use Arora’s program for tree mainte-

5.1-2

nance [Aro94], which allows fail-stops and repairs to yield states where there are multiple, possibly unrooted, trees. Next we briefly describe how the program deals with multiple trees and unrooted trees, and eventually converges to a state where there is exactly one tree spanning all processes. We refer the reader to [Aro94] for the proof of the nonmasking program.

The program merges multiple trees such that no cycles are formed: each

5.1-3

process maintains a variable root.j to denote the process that j believes to be the root. When process j observes a neighbor k such that root.k is greater than root.j, j merges in the tree of k by setting root.j to root.k and par.j to k. By merging thus, cycles are not formed, and the root value of each process remains at most the root value of its parent. This process continues until no merge action is enabled, at which point all processes have the same root value.

The program has actions to let each process detect if it is in an unrooted

5.1-4

tree. To detect whether a process is in an unrooted tree, each process j maintains a variable col.j to denote the color of process j (which is either red or green). Whenever j detects that a parent of j has failed, j sets col.j to red, denoting that j is in an unrooted tree. This color is propagated from the tree root to the leaves so that all descendents of j detect that they are in an unrooted tree; i.e., when a process l observes that the parent of l has set its color to red, denoting that the parent of l is in an unrooted tree, l sets col.l to red. Finally, when a leaf process sets its color to red, it separates from the tree, forms a tree consisting only of itself, and sets its color to green, denoting that it is no longer in an unrooted tree. Thus, Arora’s tree-maintenance program ensures that after faults stop occurring,

17 the parent tree is (re)constructed.

To restore Gd.j at every process, we proceed as follows. We ensure that

5.1-5

if j and par.j are in the same tree (i.e., if root.j is the same as root.(par.j) and their color is green), then Gd.j is satisfied. Also, when j merges into the tree of k, j satisfies Gd.j by copying the state and sequence number from k. It follows that in all stable states where the root values of all processes are equal, Gd.j holds for all processes.

Variables. Every process j maintains the following variables:

5.1-6

• col.j, the color of the process j: the color of j is either green or red; and

• root.j, the root of the process j: the identifier of the process that j believes to be the root.

Actions. Program NR consists of six actions for each process j. The

5.1-7

first three actions implement the reset wave. Action NR1 is the initiation action; it is the same as action R1 . Action NR2 is the propagation action; it is a restricted version of action R2, where j executes the action NR2 only if j and par.j are green and in the same tree. Action NR3 is the completion action; it is a restricted version of R3, where j executes action R3 only if col.j is green and the root value of the children of j is the same as root.j.

The remaining three actions maintain a spanning tree. Action NR4 deals

5.1-8

with unrooted trees: if j detects that par.j has failed or that col.(par.j) is red, j sets col.j to red. Action NR5 lets a leaf process change its color from red to green: if j is a red leaf, then j separates from its tree and resets its color to green, thus forming a tree consisting only of itself. Action NR6 merges two trees: a process j merges into the tree of a neighboring process k when root.k >root.j. Upon merging, j sets root.j to be equal to root.k and par.j to be equal to k, and it copies the state and sequence number from k.

Formally, the actions of program NR at process j are as shown in Figure 3

5.1-9

(let Adj.j denote the neighbors of j):

NR1 :: R1

NR2 :: root.j =root.(par.j) ∧ col.(par.j)=green ∧

st(par.j)=reset ∧ sn.j ≠sn.(par.j)

⟶ st.j, sn.j := reset, sn.(par.j); {reset local state of j}

18 Kulkarni and Arora Multitolerance §5.1.3

NR3 :: st.j =reset ∧ col.j =green

(∀k : k ∈ch.j : root.j =root.k ∧ sn.j =sn.k ∧ st.k ≠reset) ⟶ st.j := normal; if par.j =j, then {declare reset complete}

NR4 :: col.j =green ∧ (par.j ∉Adj.j∪{j} ∨ col.(par.j)=red) ⟶ col.j := red

NR5 :: col.j =red ∧ (∀k : k ∈Adj.j : par.k ≠j)

⟶ col.j, par.j, root.j := green, j, j

NR6 :: k ∈Adj.j ∧ root.j <root.k ∧ col.j =green ∧ col.k =green ⟶ par.j, root.j,:= k, root.k; st.j, sn.j := st.k, sn.k

Figure 3: Actions of program NR at process j

5.1.3 Fault Actions

The fail-stop and repair actions are shown in Figure 4.

fail-stop :: up.j  ⟶  up.j := false
repair ::  ¬up.j  ⟶  up.j, par.j, root.j, col.j := true, j, j, red

Figure 4: Fail-stop and repair actions of program NR

Fault Span and Invariant. From Arora’s tree-maintenance program,

5.1-10

we know that in the presence of fail-stops and repairs, the program actions preserve the acyclicity of the graph of the parent relation, as well as the fact that the root value of each process is at most the root value of its parent. They also preserve the fact that if a process is colored red, then its parent has failed or its parent is colored red. Thus, the predicate T_{T REE} is in the fault span, where:

T_{T REE} = the graph of the parent relation is a forest ∧ (∀j : up.j : T 1.j), where

T 1.j = ((col.j =red ⇒ (par.j ∉Adj.j∪{j} ∨ col(par.j)=red)) ∧ 19

(par.j =j ⇒ root.j =j) ∧ (par.j ≠j ⇒ root.j >j) ∧

(par.j ∈Adj.j ⇒ (root.j ≤root.(par.j) ∨ col(par.j)=red)))

Observe that Gd.j is preserved when root.j is the same as root.(par.j),

5.1-11

and col.(par.j) is green. Hence, the predicate NGD = (∀j :: NGd.j) is in the fault span, where:

NGd.j = (root.j =root.(par.j) ∧ col.(par.j)=green ⇒ Gd.j)

Thus, the fault span of the program is:

T_{NR} = T_{T REE} ∧ NGD

In a stable state, the color of all processes is green, and the root values of all processes are identical. Thus, the invariant of the program S_{NR} is:

S_{NR} = T_{NR} ∧ S_{R} ∧ (∀j, k :: par.j ∈Adj.j ∧ col.j =green ∧ root.j =root.k)

Theorem 1 Program NR is nonmasking tolerant to fail-stop and repair faults for invariant S_{NR} and fault span T_{NR}.

5.2 Enhancing Tolerance to Masking

Program NR, being nonmasking tolerant, allows a reset operation to com-

5.2-1

plete prematurely. To enhance the tolerance of NR to masking, we now add actions that detect whether all processes participated in the given reset operation. Recall from Section 3 that this detection is made possible by letting each process maintain for each reset wave a “result” that is true only if its neighbors have propagated that wave. The result of each process is propagated toward the initiator in the completion of the reset wave. In particular, if j has completed a reset wave with the result false, then the parent of j completes that reset wave with the result false, and so on. Also, if j fails or changes its tree, the (old) parent of j cannot always determine the result of j. Hence, when j fails or changes its tree, the parent of j completes the reset wave with the result false. It follows that when the root completes the reset wave with the result true, all processes have participated in the reset wave.

It remains to specify how a process detects whether its neighbors have

5.2-2

propagated the current wave. One possibility is for j to detect whether the 20 sequence numbers of all of its neighbors are the same as that of j. Unfortunately, because the sequence numbers are bounded, such a detection is insufficient. We illustrate this by an example. In particular, we exhibit a program computation whereby (1) even though j and l have the same sequence number, they are in different reset waves; and (2) even though j completes one reset wave after it changes its tree, and j and l have the same sequence number, they are in different reset waves.

Let the initial state be as shown in Figure 5a. Process k is the root,

5.2-3

and the root value of all processes is k. Also, k has initiated a reset wave with sequence number 0, which all processes except l have propagated. The computation proceeds as follows:

• Process n fails.

• Process k completes its reset wave and initiates a new reset wave with sequence number 1 (Figure 5b).

• Process j separates from the tree, changes its parent to k, and propagates the reset wave with sequence number 1 (Figure 5c).

• Process j completes its reset wave (Figure 5d). Observe that when j completes this reset wave, although the sequence number of l is the same as that of j, l has not propagated the current reset wave of k. Thus, (1) is satisfied.

• Process l propagates the reset wave with sequence number 0. Also, k completes its reset wave and initiates a new reset wave with sequence number 0 (Figure 5e).

• Process j propagates the new reset wave of k with sequence number 0 (Figure 5f). Observe that although j has completed one reset wave since it changed its tree, and the sequence numbers of j and l are the same, they are in different reset waves. Thus, (2) is satisfied.

From the above computation, we observe that after j changes its tree, it

5.2-4

cannot safely detect whether l is in the same wave as j during the subsequent two waves.

Fortunately, in the third wave after j changes its tree, j can safely detect

5.2-5

whether l is in the same wave, provided j and l do not change their trees in the interim. Returning to our example:

21 Kulkarni and Arora Multitolerance §5.2 Figure 5: Detecting whether a neighbor is reset in the current reset operation

22

Chicago Journal of Theoretical Computer Science 1998-4 • Process j completes the reset wave with sequence number 0. Again,

observe that when j completes this second reset wave, l is still propagating an old reset wave (Figure 5g).

• Process k completes its reset wave and initiates a new reset wave with sequence number 1. Also, process j propagates this reset wave (Figure 5h).

Observe that starting from the state in Figure 5h, j can complete its reset

5.2-6

wave only when the sequence number of l is 1. However, since all ancestors of l have sequence number 0 and none of them is a root, l cannot change its sequence number to 1 unless l changes its tree. Also, in any tree that l joins and completes two reset waves, l cannot propagate the next reset wave unless k is an ancestor of l, in which case the reset wave propagated by l is the current reset wave of k. Thus, if j and l both complete at least two reset waves since they changed their respective trees, j can safely detect whether the reset wave propagated by l is the current reset wave of k. Thus, the following lemma holds.

Lemma 1 (Sufficiency Condition for Bounded-Memory Safety Detection) Let j, k, l be processes such that j and l are neighbors. Consider a state in S_{MR} where root.j = root.l = root.k = k, and k is an ancestor of j. In every computation of MR starting from this state, if j and l do not change their tree and complete two reset waves, then the next reset wave propagated by j (respectively, l) is the current reset wave being propagated by k.

We use Lemma 1 to specify how j detects whether its neighbors have

5.2-7

propagated the same reset wave as that of j, as follows. Process j maintains a ternary variable new.j, whose value is either 0, 1, or 2. When j changes its tree, new.j is set to 2. When j completes a reset wave, if new.j is nonzero, j decrements new.j by 1. Thus, j detects that it has completed at least two reset waves since it last changed its tree by checking that new.j is zero. Also, j detects that all its neighbors have propagated at least two reset waves since they changed their tree by checking that their new values are zero.

Thus, new implements the “result” associated with the reset wave. The

5.2-8

new value being zero is equivalent to the result being true, and the new value being nonzero is equivalent to the result being false. Therefore, if the new value of j or any neighbor of j is nonzero, j sets new.(par.j) to a nonzero value to ensure that when par.j completes the reset wave, par.j sets

23 new.(par.(par.j)) to a nonzero value, and so on. Thus, when the initiator completes the reset wave, its new value is nonzero, and the initiator concludes that the reset wave has completed incorrectly.

As mentioned in Section 3, if the initiator detects that the reset wave has

5.2-9

completed incorrectly, it initiates a new reset wave. Also, if a process j fails, the parent of j cannot obtain the value of new.j. In that case, the parent of j aborts that reset wave by setting its new value to 2.

Variables. As described above, each process j additionally maintains

5.2-10

the variable new.j, which is either 0, 1, or 2.

Actions. Program MR consists of six actions for each process j. The

5.2-11

first three actions implement the reset wave. Action MR1 is the initiation action; it is the same as action NR1 . Action MR2 is the propagation action; it is the same as action NR2 . Action MR3 is the completion action; it is a restricted version of NR3, where j executes action NR3 only if the predicate (∀l : l ∈ Adj.j : root.j = root.l ∧ sn.j = sn.l) holds. Also, j updates the variable new as described above. If the initiator completes a reset wave incorrectly, it initiates a new reset wave. Actions MR4, MR5, and MR6 maintain a spanning tree. When j changes its tree, by executing actions NR5 and NR6, j sets the new value of j and the old parent of j to 2.

Formally, the actions for the process j are as in Figure 6 (for simplicity,

5.2-12

we let actions MR3, MR5, and MR6 at j update the value of new.(par.j). As discussed in the Appendix (Section A3), this program can be refined so that j writes only the variables at process j.)

MR1 :: NR1

MR2 :: NR2

MR3 :: st.j = reset ∧ col.j = green∧ ⟶ st.j := normal;

(∀l : l ∈ Adj.j : root.l = root.j∧ if (∃l : l ∈Adj.j∪{j} : new.l >0), then

sn.j =sn.l) ∧ if (par.j =j), then
(∀l : l ∈ch.j : st.l ≠reset) st.j, sn.j := reset, sn.j⊕1;

{reset local state of j} else

new.(par.j) := max(new.(par.j), 1) else if (par.j =j) then {declare reset new.j := max(0, new.j−1) complete};

MR4 :: NR4

24

MR5 :: col.j =red ∧ ⟶ col.j, par.j, root.j := green, j, j; (∀k : k ∈Adj.j : par.k ≠j) new.j, new.(par.j) := 2, 2

MR6 :: k ∈Adj.j ∧ root.j <root.k ∧ ⟶ par.j, root.j := k, root.k;

col.j =green ∧ col.k =green st.j, sn.j := st.k, sn.k;

new.j, new.(par.j) := 2, 2

Figure 6: Actions of program MR at process j

Fault Actions. As described above, when a process j fail-stops, par.j

5.2-13

needs to set new.(par.j) to 2. Since a process does not know whether j is its child, we implement this by letting all neighbors of j set their new value to 2. When a process j is repaired, j sets new.j to 2. Formally, the actions are described in Figure 7.

fail-stop:: up.j ⟶ up.j := false; (∀l : l ∈ Adj.j : new.l := 2) repair:: ¬up.j ⟶ up.j, par.j, root.j, col.j, d.j, new.j := true, j, j, red, 0, 2

Figure 7: Fail-stop and repair actions of program MR

Remark 3 In the fail-stop action, we have overloaded the operator ∀ to denote that the statement “new.l := 2” is executed at all processes in Adj.j. In the Appendix (Section A3), we observe that this parallel execution can be refined so that these statements are executed asynchronously.

Invariant. While we relegate the detailed invariant (S_{MR}) of the masking

5.2-14

reset program to the Appendix (Section A1), we sketch here the essential predicates in the invariant. To characterize the predicates of the invariant, we define:

X.j = {j} if par.j =j ∨ par.j ∉ Adj.j ∨ col.j =red ∨ root.j ≠root.(par.j) {j} ∪ X.(par.j) otherwise

pc.j.k = set of processes to whom j propagated the current reset wave of k; thus, if j is propagating the current reset wave initiated by k, and a child of j (say l) propagates this reset wave by executing action MR2, l is added to pc.j.k. If j has not propagated the current reset wave initiated by k, or if k is not a root process, pc.j.k is the empty set 25 des.j.k = {j} ∪ (⋃ l : l ∈ pc.j.k : des.l.k)

nbrs(des.j.k) = des.j.k ∪ {l : ∃j :: (l ∈ Adj.j ∧ j ∈ des.j.k)}

failed.k = set of processes that repaired after k started its reset wave

Intuitively, X.j is the set of ancestors of j that have the same root value

5.2-15

as j and their color is green, and des.j.k is the set of processes that have propagated the current reset wave initiated by k via j. It follows that des.k.k denotes the set of processes that have propagated the current reset wave of k.

When j completes a reset wave initiated by k, j detects whether all of

5.2-16

its neighbors have propagated the current reset wave of k. It also detects that all processes that have propagated this reset wave via j (i.e., des.j.k) have completed their detections successfully. Thus, all neighbors of des.j.k have propagated the current reset wave of k (i.e., they are in des.k.k) or they are newly repaired processes (they are in failed.k). Thus, nbrs(des.j.k) is a subset of (des.k.k∪failed.k).

Observe that when a process j, such that k ∈ X.j, completes a reset

5.2-17

wave, j detects the predicate nbrs(des.j.k) ⊆ (des.k.k ∪failed.k) by checking new.j and the new values of its neighbors. If j cannot conclude that nbrs(des.j.k) ⊆ (des.k.k ∪ failed.k) holds, j sets new.(par.j) to a nonzero value. And, new.(par.j) remains nonzero until par.j completes this reset wave. Thus, the predicate I1 is in the invariant, where:

I1 = (k ∈ X.j ∧ new.j = 0 ∧ st.j ≠ reset∧ st.k = reset ∧ sn.j = sn.k) ⇒ nbrs(des.j.k)⊆(des.k.k∪failed.k) ∨

new.(par.j)>0 ∨
(par.j ≠ j ∧ st.(par.j)≠reset)

Finally, the predicates T_{T REE} and NGD are in the invariant.

5.2-18

Lemma 2 At any state where S_{MR} holds, if a root process declares that a distributed reset has completed correctly, then nbrs(des.k.k) ⊆ (des.k.k ∪ failed.k).

Theorem 2 Program MR is masking tolerant to fail-stop and repair faults for invariant S_{MR}.

26

6 Stabilizing- and Masking-Tolerant Distributed Reset

In this section, we transform program MR to add stabilizing tolerance to

6-1

transient faults. To this end, we add convergence actions to program MR that restore it from an arbitrary state to a state where S_{MR} holds.

We proceed as follows. Since each state where S_{MR} holds satisfies T_{T REE}

6-2

and NGD, we add convergence actions to program MR that restore it from an arbitrary state to a state where T_{T REE} ∧ NGD holds. Further, we show that starting from a state where T_{T REE} and NGD hold, the program converges to a state where S_{MR} holds.

By the definitions of T_{T REE} and NGD, T_{T REE} ∧ NGD may be violated

6-3

if any of the following three conditions hold:

1. the graph of the parent relation contains cycles,

2. there exists a process j such that T 1.j is violated, or

3. there exists a process j such that NGd.j is violated.

To handle condition 1, each cycle in the graph of the parent relation is

6-4

detected and removed. To detect cycles, j maintains a variable d.j to be the distance between j and root.j in the graph of the parent relation. Thus, if j is a root process, d.j is zero; otherwise d.j is d.(par.j) + 1. Observe that if the graph of the parent relation is acyclic and there are at most K up processes, then for all processes, their distance is less than K. Hence, whenever par.j ∈Adj.j and d.(par.j)<K, j maintains d.j to be d.(par.j) + 1. If j belongs to a cycle, then d.j increases repeatedly. Whenever d.j exceeds K−1, a cycle is detected. To remove the detected cycle, j sets the parent of j to j.

To handle condition 2, whenever T 1.j is violated, j corrects T 1.j by

6-5

separating from the tree and setting par.j and root.j to j.

To handle condition 3, whenever NGd.j is violated, j corrects NGd.j by

6-6

copying the state and sequence number values from its parent.

Variables. As described above, each process maintains a variable d.j to

6-7

denote the distance of j from root.j in the graph of the parent relation. Actions. Program MSR consists of nine actions for each process j. Ac-

6-8

tions MSR1 –MSR6 construct the spanning tree and implement the reset wave; they are identical to the actions MR1 –MR6 . Action MSR7 corrects

27 d.j whenever par.j ∈ Adj.j and d.(par.j) < K, by setting d.j to d.(par.j)+1. Action MSR8 is executed when d.j exceeds K or T 1.j is violated. As described earlier, when j executes MSR8, j sets par.j and root.j to j and d.j to zero. Since j changes its tree in action MSR8, j sets both new.j and the new of the old parent of j to 2. Action MSR9 is executed when j violates NGd.j. Additionally, j corrects NGd.j by copying the state and sequence number from its parent.

Formally, the actions are as shown in Figure 8.

6-9

MSR1 :: MR1

⋮

MSR6 :: MR6 MSR7 :: par.j ∈Adj.j ∧ d.j ≠d.(par.j) + 1 ∧ d.(par.j)< K

⟶ d.j := d.(par.j) + 1

MSR8 :: d.j ≥K ∨ ¬T 1.j ∨ (par.j =j ∧ d.j ≠0) ⟶ par.j, col.j, root.j, d.j, new.j, new.(par.j) := j, red, j, 0, 2, 2

MSR9 : ¬NGd.j ⟶ st.j, sn.j := st.(par.j), sn.(par.j)

Figure 8: Actions of program MSR at process j

Invariant. The invariant of the stabilizing and masking program MSR

6-10

is:

S_{MSR} = S_{MR}

As mentioned in Section 3.2, to preserve the masking tolerance to fail-stop

6-11

and repair faults, we prove the following lemma.

Lemma 3 Actions MSR7–MSR9 preserve S_{MR}, and do not execute indefinitely after program MSR reaches a state in S_{MR}.

Theorem 3 Program MSR is masking tolerant to fail-stop and repair faults, and is stabilizing tolerant to transient faults for invariant S_{MSR}.

6-12

28 Remark 4 Since the program MSR is masking tolerant to fail-stop and repair faults, the fault span in the presence of fail-stop and repair faults, T 1, is identical to the invariant S_{MSR}. Since the MSR is stabilizing tolerant to transient faults, the fault span in the presence of transient faults, T 2, is true.

7 Bounding the Sequence Numbers of Multitolerant Applications

In this section, we discuss how applications use the bounded sequence num-

7-1

bers associated with the multitolerant distributed reset to become multitolerant. For ease of exposition, we focus our attention on the case when the application has to be made masking-fault tolerant to some fault class. In this case, when a fault is detected, the application is reset while ensuring that both the old and the new instances of the application execute correctly. In particular, we ensure that two processes communicate only when they have been reset in the same reset wave.

7.1 Need for Incarnation Numbers

If the sequence numbers associated with the distributed resets are un-

7.1-1

bounded, ensuring this property is simple: it suffices to restrict the communication between any two processes to occur only when their sequence numbers are identical. When the sequence numbers are bounded, however, it is possible for two processes to have the same sequence number even though they have reset their states in different reset waves.

We therefore introduce an incarnation number for each process. Two

7.1-2

processes have the same incarnation number if and only if they have reset in the same reset wave. Hence, it suffices to restrict the communication between two processes to occur only when their incarnation numbers are identical.

It turns out that a bound of two on the incarnation number is insuffi-

7.1-3

cient. To see this, consider the following computation: The initial state is as shown in Figure 10a: processes 1, 2, and 3 form a tree rooted at 3. Let 3 initiate a reset wave to change the incarnation numbers to 1. Processes 1 and 3 propagate this reset wave, and change their incarnation number to 1 (Figure 10b). Before 2 propagates this reset wave, 3 fails, and the resulting tree is rooted at 2 (Figure 10c). Unfortunately, the state in Figure 10c can

29

Stabilizing and Masking Program MSR Actions MSR–9 converge to S_{MR} Masking Program MR gNR3 sNR3 sNR4 sNR5  Nonmasking Program NR Actions NR4–6 to maintain tree gR3 gR2 Fault-intolerant program, R Actions R1 − 3 Legend: Action Y i of program Y is obtained by action Xi of program X with gXi added to the guard of Xi and sXi added to the statement of Xi. Unless explicitly mentioned, gXi is true and sXi is skip gR2 = (root.j = root.(par.j)) and col.(par.j) = green gR3 = (forall k : k in ch.j : root.j = root.k and col.j = green) gNR3 = (forall l : l in Adj.j : root.j = root.l and sn.j = sn.l) sNR3 = update new.j, new.(par.j) sNR4 = new.j, new.(par.j) := 2, 2 sNR5 = new.j, new.(par.j) := 2, 2

Figure 9: Composition of the masking- and stabilizing-reset program (MSR)

30

Chicago Journal of Theoretical Computer Science 1998-4 alternatively be reached by starting from a state in Figure 10d and letting process 2 initiate a new reset wave. In the first computation, all processes should change their incarnation numbers to 1 in the future. In the second computation, all processes should change their incarnation numbers to 0 in the future. Thus, keeping only two incarnation numbers is insufficient, as processes cannot determine which incarnation number is current.

Legend ^{failed process}^{up process}^{k} ^{parent of j is k}^{j, 0}  ^{incarnation number of j is 0}^{j}^{j :}^{j :}^{3, 0} ^{1, 0} ^{2, 0}^{1, 1} ^{2, 1}  ^{1, 1} ^{2, 0} (a)  (b)  (c) (d)  (e)^{3, 1} ^{1, 1} ^{2, 0} ^{3, 1} ^{1, 1} ^{2, 0}

Figure 10: Insufficiency of two incarnation numbers

7.2 Designing Multitolerant Applications using Three Incarnation Numbers

It is possible to determine the current incarnation number if we use ternary

7.2-1

(0, 1, or 2) incarnation numbers and follow the rule that a new incarnation number B + 1 can be created only if the incarnation number B − 1 does not exist in the system (in this section, we let + and − denote modulo 3 addition and subtraction, respectively.) It follows that at any invariant state, at most two incarnation numbers may coexist. Also, for any pair of incarnation numbers, it is easy to determine which of the two is associated with the current reset wave.

When to Reset the Local State of a Process. When process j propagates

7.2-2

a reset wave, it resets its state if and only if the incarnation number of the parent of j is one greater (in mod 3 arithmetic) than the incarnation number of j. When j resets its state, it also copies the incarnation number of its parent.

When to Create a New Incarnation Number. As motivated above, all

7.2-3

three incarnation numbers should not exist simultaneously. Hence, we ensure that a process changes its incarnation number from B to B + 1 only if no process with incarnation number B − 1 exists in the system. From the invariant of the reset program, we know that when the root completes a reset wave successfully, all processes have propagated that reset wave. Thus, if a

31 process with incarnation number B − 1 existed in the system when the root initiated the reset wave, this process would have set its incarnation number to B upon propagation of the reset wave. Also, no process can change its incarnation number from B to B − 1. Hence, when the root process completes a reset wave successfully, it can safely increment its incarnation number.

When to Declare that Reset is Complete. When a root completes a reset

7.2-4

wave successfully with incarnation number B, no process in the system has incarnation number B − 1. It is, however, possible that some processes have incarnation number B + 1. (Such a state may arise if the tree program converges to a state where the root does not have the current incarnation number). Hence, we let the root declare completion of a reset only if the reset completes correctly and the root can detect that the incarnation numbers of all processes are the same. To this end, we let each process check whether all its children have the same incarnation numbers when it completes in the reset wave. The completion wave propagates this information toward the root so that the root can determine whether the incarnation numbers of all processes are the same.

Variables. Every process j maintains the following variables:

7.2-5

• inc.j, the incarnation number: one of 0, 1, or 2, and

• ares.j, application result: a Boolean.

Actions. Program APP consists of nine actions for each process j. The

7.2-6

first three actions implement the reset wave. These actions are obtained by modifying actions MSR1–MSR3 to update inc and ares appropriately. Action APP1 is the initiation action; whenever j initiates a reset wave, j increments its incarnation number if and only if new.j is zero. Action APP2 is the propagation action; whenever j propagates a reset wave, j increments its incarnation number if and only if the incarnation number of the parent of j is one higher than that of j. Action APP3 is the completion action; whenever j completes a reset wave, j sets ares.j to true if and only if all children of j have the same incarnation number and their application result is true. Finally, the remaining actions APP4 –APP9 break cycles in the graph of parent relation and maintain the underlying tree; these actions are identical to the actions MSR4 –MSR9 of program MSR.

APP1 :: par.j =j ∧ st.j = normal ∧ {j needs to initiate a new reset wave} ⟶ st.j, sn.j := reset, sn.j⊕1;

32

if (new.j =0) then inc.j := inc.j+1; {reset application state}

APP2 :: root.j =root.(par.j) ∧ col.(par.j)=green ∧ st(par.j)=reset

∧ sn.j ≠sn.(par.j) ⟶ st.j, sn.j := reset, sn.(par.j);

if ((inc.j+1) = inc.(par.j))) then inc.j := inc.(par.j); {reset application state}

APP3 :: st.j =reset ∧ col.j =green ∧ (∀l : l ∈ ch.j : st.l ≠ reset) ∧ (∀l : l ∈ Adj.j : root.l = root.j ∧ sn.j = sn.l)

⟶ st.j, ares.j := normal, (∀l : l ∈ch.j : ares.l ∧ (inc.j =inc.l));

if (∃l : l ∈Adj.j∪{j} : new.l >0) then if (par.j =j) then st.j, sn.j := reset, sn.j⊕1;

else new.(par.j) := max(new.(par.j), 1)

else if (par.j =j ∧ ares.j) then {declare reset complete} else if (par.j =j ∧ ¬ares.j) then

st.j, sn.j, inc.j := reset, sn.j⊕1, inc.j + 1; {reset application state};

new.j := max(0, new.j−1)

AP P 4 :: MSR4

⋮

AP P 9 :: MSR9

Figure 11: Actions of program APP at process j

Outline of the Proof. We need to show that:

7.2-7

1. when a root process with incarnation number B declares that a reset is complete, all processes have incarnation number B;

2. at most two incarnation numbers coexist at any invariant state; and

3. after a reset operation is initiated at an invariant state, the root process eventually declares that the reset is complete.

When j completes a reset wave, it checks that the incarnation number

7.2-8

of j is the same as its children. Thus, when j completes its reset wave, it 33 can detect whether all processes that received the reset wave via j have the same incarnation number. Recall that when the root declares that reset is complete, we know from MSR that all processes have propagated that reset wave. Hence, when the root declares that a reset is complete, all processes have the same incarnation number. Thus, condition 1 above is satisfied.

To satisfy condition 2, we show that when a process creates a new incar-

7.2-9

nation number B + 1 after completing a reset wave with incarnation number B, no process has incarnation number B − 1. Suppose not: consider the first process, say j, that has incarnation number B − 1 after propagating this reset wave. We consider three cases, depending upon the value of the incarnation number of par.j when j propagated this reset wave: (1) the incarnation number of par.j cannot be B − 1, since par.j has propagated the reset wave and j is the first process to change its incarnation number to B − 1; (2) if the incarnation number of par.j is B, then after propagating the reset wave, the incarnation number of j is either B or B + 1; and (3) if the incarnation number of par.j is B + 1, then before j propagates the reset wave, the incarnation number of j cannot be B − 1, as only two incarnation numbers coexist. Thus, condition 2 above is satisfied.

From MSR, we know that eventually the root with incarnation number

7.2-10

B will either declare that reset is complete or initiate a new reset wave with incarnation number B +1. Upon propagation of this reset wave, all processes with incarnation number B change their incarnation number to B + 1. It follows that the root will eventually declare that the reset is complete. Thus, condition 3 is satisfied.

8 Conclusions

In this paper, we presented a bounded-memory distributed reset program

8-1

that is distinguished by its ability to be both masking tolerant to any finite number of fail-stops and repairs and stabilizing tolerant to transient faults. The program was designed by iteratively transforming a fault-intolerant program so as to add tolerance to each class of faults.

Distributed reset programs belong to the class of total programs [Tel89].

8-2

Total programs characteristically contain one or more “decider” actions, whose execution depends on the state of all processes. In the case of distributed reset programs, the action that declares the completion of a reset operation is a decider action. The safety of the execution of this decider

Kulkarni and Arora Multitolerance §A.1

34 action was achieved in this paper by using a detector that ensures that (1) if fail-stops and repairs occur, the decider action is executed only after all processes are contacted; and (2) after transient faults occur, eventually the program reaches a state from where the decider action executes only after all processes are contacted. This strategy provides a basis for making other total programs likewise multitolerant: before a process executes a decider action, it waits for the detector to collect the state of all processes (i.e., whenever a process is contacted, its state is collected). From points 1 and 2, it follows that the resulting total program is multitolerant.

Our discussion of distributed reset has intentionally omitted how the ap-

8-3

plication module chooses the global reset state parameter for each reset operation, but it is worthwhile to point out that these global states may be determined dynamically, say by a checkpointing program.

In our program, in stable states, the processes form a rooted tree and

8-4

all reset operations are performed on this underlying tree. An alternative approach would be to construct the tree dynamically in every reset operation, as in [APSV91, Var93]. Analogous to their reset program, there exists a reset program that is masking tolerant to fail-stop and repair faults and stabilizing tolerant to transient faults and that does not use an underlying tree.

Finally, we reiterate that our assumption that the distributed reset re-

8-5

quest be initiated only at the root process is not necessary. The program is easily extended to allow any process to initiate a reset, by propagating a reset request toward the root along the parent tree. (The interested reader is referred to [AG94] for the implementation of this request propagation.) Moreover, the program is systematically extended to add masking tolerance to channel failure and repairs, as well as to use message-passing communication.

A Appendix

A.1 Proof of Masking-Fault Tolerance of Program MR

Invariant for the Masking-Distributed Reset. As described in Section

A.1-1

5, the predicates T_{T REE}, NGD, and I1 are in the invariant, S_{MR}, of the masking reset. Here, we characterize the remaining predicates in S_{MR}.

First, we recall the definition of X.j from Section 5.2:

A.1-2

35 X.j = {j} if par.j =j ∨ par.j ∉ Adj.j

∨ col.j =red ∨ root.j ≠root.(par.j)

{j} ∪ X.(par.j) otherwise

Intuitively, X.j denotes the green-colored ancestors of j that have the

A.1-3

same root value as j.

For the following discussion (predicates I2–I8), we assume that j and l

A.1-4

are two processes such that k ∈ X.j (i.e., there exists a path from j to k in the graph of the parent relation, and all processes on this path are green and have the root value k), and l ∈ Adj.j (i.e., l is a process adjacent to j).

When j completes a reset wave, sn.j is the same as sn.l. The predicate

A.1-5

sn.j = sn.l is violated only if either sn.j or sn.l is updated. The variable sn.j is updated only if j changes trees or propagates a reset wave. If j(l) changes its tree, violating sn.j = sn.l, then new.j(new.l) is set to 2. When l propagates a reset wave, from NGD, all processes in X.l have the same sequence number. When j propagates a reset wave, j is in the reset state and it cannot complete the reset wave until sn.j =sn.l is (re)satisfied. Thus, the predicate I2 is in the invariant, where:

I2 = (new.j ≠2 ∧ new.l ≠2) ⇒ (st.j ≠reset ≡ sn.j =sn.l) ∨ (∀m : m∈ X.l : sn.m=sn.l)

When j completes a reset wave and decrements new.j from 1 to 0, j is

A.1-6

in the reset state and sn.j is the same as sn.l. Thus, from the predicate I2, the second disjunct, (∀m : m ∈ X.l : sn.m = sn.l), must be true; i.e., all processes in X.l have the same sequence number. Also, when j completes a reset wave, sn.l is the same as sn.j, which in turn is equal to sn.k (from NGD). Thus, the predicate I3 is in the invariant, where:

I3 = (st.j ≠reset ∧ sn.j =sn.k ∧ new.j =0 ∧ new.l ≠2) ⇒ (∀m : m∈ X.l : sn.m=sn.k)

Consider the case where k starts a new reset wave by changing sn.k: From

A.1-7

I3, observe that all processes in X.l have the same sequence number (in this case, different from sn.k) unless k ∈X.l. If k ∈X.l, then trivially there exists a process in X.l (namely, k itself) which has propagated the current reset wave of k. Thus, the predicate I4 is in the invariant, where:

36 I4 = (sn.j ≠ sn.k ∧ new.j = 0

∧ new.l ≠2) ⇒ (∀m : m∈ X.l : sn.m≠sn.k)

∨ (sn.l ≠sn.k ∧
(∃m : m∈ X.l∩ des.k.k : sn.m=sn.k))
∨ (sn.l =sn.k ∧ l ∈ des.k.k)

Starting from a state where I4 holds, if j propagates a reset wave initiated

A.1-8

by k, then the consequent of I4 continues to hold. When l executes the completion action and new.l is decremented from 2 to 1, from NGD, all ancestors of l have the same sequence number. Thus, the predicate I5 is in the invariant, where:

A.1-9

I5 = (sn.j = sn.k ∧ st.j = reset∧

new.j = 0 ∧ new.l ≠ 2) ⇒ (∀m : m ∈ X.l : sn.m ≠ sn.k)

∨ (sn.l ≠ sn.k∧
(∃m : m ∈ X.l ∩ des.k.k : sn.m = sn.k))
∨ (sn.l = sn.k ∧ l ∈ des.k.k)
∨ (new.l = 1∧
(∀m : m ∈ X.l : sn.m = sn.k) ∧ st.l ≠ reset)

As claimed earlier, when a process j completes a reset wave, if new.l and

A.1-10

new.j are zero, then l has propagated the current reset wave initiated by k. Thus, the predicate I6 is in the invariant, where:

I6 = (sn.j =sn.k =sn.l ∧ st.j =reset ∧ new.j =0 ∧ new.l =0) ⇒ (l ∈ des.k.k)

When k starts a new reset wave, if sn.j is different from sn.k, j has not

A.1-11

propagated this reset wave, i.e., pc.j.k is the empty set. When j propagates a reset wave, all processes in pc.j.k are children of j, unless some of these children have moved to a different tree or failed. If one of the processes in pc.j.k moves to a different tree or fails, new.j is set to 2. Thus, the predicate I7 is in the invariant, where:

I7 = (new.j =0) ⇒ (sn.j ≠sn.k ⇒ pc.j.k =ϕ) ∧ (sn.j =sn.k ⇒ pc.j.k ∈ch.j)

37 Finally, if j and par.j are propagating a reset wave initiated by k and

A.1-12

par.j is propagating the current wave of k, j is also propagating the current wave of k. Thus, the predicate I8 is in the invariant, where:

I8 = (par.j ∈ des.k.k ∧ sn.j = sn.(par.j) ∧ st.j = reset) ⇒ (j ∈ des.k.k)

Thus, the invariant of the masking distributed-reset program, MR, is:

A.1-13

S_{MR} = (NGD ∧ T_{T REE} ∧ (∀j, l : k ∈X.j ∧ l ∈Adj.j ∧ root.j =root.l =k : I1 ∧ I2 ∧ I3 ∧ I4 ∧ I5 ∧ I6 ∧ I7 ∧ I8)

Lemma 4 Consider a state in S_{MR} where root.j =root.l =root.k =k holds, j and l are neighbors, and k is an ancestor of j. In every computation of MR starting from this state, if j and l do not change their tree and complete two reset waves, then the next reset wave propagated by j (respectively, l) is the current reset wave being propagated by k.

Proof of Lemma 4 When j concludes that j and l are propagating the same reset wave, new.j and new.l is zero. From I6, it follows that l has propagated the current reset wave propagated by k.

Proof of Lemma 4 □

Lemma 5 At any state where S_{MR} holds, if a root process k declares that a distributed reset has completed (by executing action MR3), then nbrs(des.k.k) ⊆ (des.k.k∪failed.k).

Proof of Lemma 5 When k declares that reset is complete by executing action MR3, we have:

(∀l : l ∈(Adj.k∪ {k}) : new.l =0 ∧ root.l =root.k ∧ sn.l =sn.k) ∧

(∀l : l ∈ ch.k : st.j ≠reset) ∧ (st.k =reset)

⇒ {from I6, I1, I7} (∀l : l ∈(Adj.k∪ {k}) : l ∈des.k.k) ∧ (∀l : l ∈ ch.k : nbrs(des.l.k)⊆(des.k.k∪failed.k)) ∧ (pc.k.k ⊆ch.k)

⇒ {by predicate calculus} (∀l : l ∈Adj.k : l ∈ des.k.k) ∧

(∀l : l ∈ pc.k.k : nbrs(des.l.k)⊆(des.k.k∪failed.k))

⇒ {by definition of des.k.k} nbrs(des.k.k)⊆(des.k.k∪failed.k)

Proof of Lemma 5 □

38

A.2 Proof of Stabilizing Fault Tolerance of Program MSR

Theorem 4 Program MSR is masking tolerant to fail-stop and repair faults, and stabilizing tolerant to transient faults for invariant S_{MSR}.

Proof of Theorem 4 Here, we show that MSR is stabilizing tolerant to transient faults. The proof of masking tolerance follows from Lemma 6 below. Proof of stabilization is based upon the “convergence stair” method of Gouda and Multari [GM91]. In particular, we exhibit predicates S.1, S.2, S.3, and S.4, where:

S.1 = true S.2 = NGD S.3 = S.2 ∧ graph of the parent relation forms a tree ∧

(∀j, k :: root.j = root.k ∧ col.j = green ∧ par.j ∈ Adj.j∧

(par.j = j ⇒ d.j = 0) ∧ (par.j ≠ j ⇒ d.j = d.(par.j) + 1))

S.4 = S.3 ∧ S_{MSR}

and show that for each i, 1 ≤ i < 4, S.i converges to S.(i + 1) in program MSR. It follows that starting from an arbitrary state, program MSR reaches a state where S.4 and, hence, S_{MSR} hold.

To prove S.1 converges to S.2, consider the set of processes for which

A.2-1

NGd.j is violated. When a process executes action MSR9, the cardinality of this set decreases by 1. The cardinality of the set never increases. Thus, eventually, the cardinality of the set reduces to zero, and hence S.2 holds. Also, it is easy to observe that S.2 is closed under the execution of program MSR.

To prove that S.2 converges to S.3, we use a proof identical to the con-

A.2-2

vergence proof in Arora and Gouda’s reset paper [AG94]. For brevity, we omit this proof here. We merely note that in a state that satisfies S.3, since the graph of the parent relation forms a tree and the predicate NGd.j holds for all processes, actions MSR4–MSR9 are disabled. Actions MSR1–MS3 trivially preserve S.3. Thus, S.3 is closed under execution of program MSR. Also, if the set of processes forms a rooted tree and all processes are green, the predicate T_{T REE} holds trivially.

To prove S.3 converges to S.4, we need to prove that the program con-

A.2-3

verges to a state where the predicates I1–I8 hold. We first prove that the program reaches a state where k, the root of the graph of the parent tree,

39 is in the normal state. We then prove that in such a state, the predicates I1–I8 hold.

As mentioned above, in a state satisfying S.3, only actions MSR1–MSR3

A.2-4

may be enabled. If action MSR1 is executed, then k is in the normal state. Hence, to prove that eventually the program reaches a state where k is in the normal state, we can assume that action MSR1 is not executed.

Consider the variant function |{j : st.j = reset}| + 2|{j : sn.j ≠ sn.k}|.

A.2-5

When a process executes either the propagation or the completion action, the value of this function decreases. Thus, eventually the system will reach a state where the value of this function is zero, in which case k is in the normal state.

We now prove that when k is in the normal state, the predicates I1–I8

A.2-6

hold. From NGD, we have that all processes are in the normal state with the sequence number sn.k. Hence, the following predicate is true for each process j:

(∀j :: sn.j =sn.k ∧ st.j ≠reset)

Since k is not in the reset state, predicates I1, I5, and I6 are satisfied.

A.2-7

Since all processes have the same sequence number, the predicate (∀m : m∈ X.l : sn.m = sn.k) holds for all processes l, i.e., predicates I2 and I3 are satisfied. Since sn.j is equal to sn.k and j is in the normal state, predicates I4, I7, and I8 are also satisfied. Thus, when k is in the normal state, the predicate S_{MSR} holds.

It now follows that starting from an arbitrary state, the program execu-

A.2-8

tion converges to a state where the predicate S_{MSR} holds.

To prove that MSR is masking tolerant to fail-stops and repairs, we show

A.2-9

that newly added actions MSR7, MSR8, and MSR9 do not interfere with the actions of program MR. Toward this end, we prove the following lemma.

Proof of Theorem 4 □

Lemma 6 Actions MSR7, MSR8, and MSR9 preserve S_{MR}, and do not execute indefinitely after program MSR reaches a state in S_{MR}.

Proof of Lemma 6 From the above proof, eventually the program reaches a state where S.3 is satisfied. In a state where S.3 is satisfied, MSR7–MSR9 are disabled. Since S.3 is closed in MSR, these actions remain disabled. Thus, actions MSR7–MSR9 do not execute indefinitely.

40 Since action MSR7 does not update any variable in S_{MR} and MSR9 is

A.2-10

disabled in S_{MR}, these two actions trivially preserve S_{MR}. Observe that when j executes action MSR8, the effect is equivalent to a fail-stop of j followed by an instantaneous repair of j. And, we know that S_{MR} is preserved under fail-stop and repair faults. Thus, MSR8 also preserves S_{MR}.

Proof of Lemma 6 □

A.3 Refinement to Low Atomicity

In program MR, the actions MR3, MR4, and MR6 of process j update the

A.3-1

new.(par.j) variable of par.j simultaneously with the variables of j. We now refine program MR so that in each action a process updates only its own variables. The refinement is made possible by the fact that the parent of j cannot complete its reset wave until j completes its reset wave. Hence, new.(par.j) can be updated after the variables of j have been updated.

In the refined version of MR, for each of its neighbors k, j maintains a

A.3-2

variable new.j.k as a local copy of the nonlocal variable new.k. Whenever j needs to update the new value of k, j updates the value of new.j.k. Process k asynchronously reads new.j.k and updates new.k. More specifically, MR is modified as follows (the modification to MSR is analogous):

1. Add a variable new.j.k in j for every neighbor k.

2. Replace the statements new.k := m by new.j.k := m.

3. Add the following two actions, the first to k and the second to j:

• new.j.k > 0 ∧ new.j.k > new.k ⟶ new.k := new.j.k

• new.j.k > 0 ∧ new.j.k ≤ new.k ⟶ new.j.k := 0

4. Replace action MR3 of j as follows:

• (∀j : j ∈ Adj.j : new.j.k = 0) ∧ guard ⟶ statement

where guard and statement denote the guard and statement of action MR3, respectively.

With this refinement, the predicates I1 and I7 of the invariant S_{MR}

A.3-3

change as follows:

41 I1′ = I1 ∨ new.j.(par.j)>0 I7′ = (new.j =0) ⇒ (sn.j ≠sn.k ⇒ pc.j.k =ϕ)

∧ (sn.j =sn.k ⇒ pc.j.k ∈ch.j
∨ (∃l : l ∈Adj.j : new.l.j >0))

And the invariant S_{MR} changes as follows:

A.3-4

SMR^{′} = (NGD ∧ T_{T REE} ∧ (∀j, l : j ∈KERN.k ∧ l ∈Adj.j

∧ root.j =root.l =k :

I1′ ∧ I2 ∧ I3 ∧ I4 ∧ I5 ∧ I6 ∧ I7′ ∧ I8))

Finally, in the fail-stop action of program MR, the state of all of its

A.3-5

neighbors is updated when process j fail-stops. This action can be easily refined so that each neighbor asynchronously updates its own state when it detects that j has fail-stopped. Thus, in the refined program, each process updates only its own state.

A.4 An Illustration of Tree Correction

We illustrate how the tree maintenance program constructs a tree in the

A4.1-1

presence of fail-stop and repair faults with an example. Let the initial state be as shown in Figure 12a. In this state, the invariant of the tree program holds, the processes 1–4 are up, and they form a tree rooted at process 4. (The arrows define the parent relation.) Now, consider the following computation.

• Process 4 fail-stops and process 5 repairs (see Figure 12b).

• Since the parent of process 2 has failed, 2 changes its color to red. And, since 5 has no children, 5 resets its color to green (Figure 12c).

• Since the color of process 2—the parent of 1—is red, 1 sets its color to red (Figure 12d).

• Since 1 has no children, 1 changes its color to green and sets its root value to 1. Also, since the root value of 3 is smaller than that of 5, 3 changes its parent to 5 and copies its root value (Figure 12e).

• Since 2 has no children, 2 changes its color to green and sets its root value to 2 (Figure 12f).

42 • Finally, since 3 has a higher root value, 1 and 2 both change their

parent to 3. The resulting state satisfies the invariant, and the tree is rooted at 5 (Figure 12g).

1,1,green^{1,4,green}^{3,5,green}^{3,4,green}^{4} ^{2,4,red}^{2,4,green}^{5,5,green}^{5}  ^{1,1,green}^{3,5,green}^{4}^{4,4,green}  ^{3,4,green} ^{5,5,red}^{1,4,green} ^{4} ^{2,2,green}^{5,5,green}^{2,4,green}  ^{1,4,green}^{1,5,green}^{3,4,green}^{3,5,green}^{4}^{4} ^{2,4,red}^{2,5,green}^{5,5,green}^{5,5,green}  ^{1,4,red}^{3,4,green}^{j} ^{j:}^{j:} ^{k} ^{3,4,green}^{4}^{root.3=4 and col.3=green}^{failed process}^{up process}^{parent of j is k}^{2,4,red}^{5,5,green} (a)  (b)  (c)  (d) (e)  (f)  (g)  Legend

Figure 12: Tree correction

43

Kulkarni and Arora Multitolerance (Ref)

A.5 Notation

Symbols

p  Program
F, F 1, F 2  Faults

D, S, T, I1−I8

State predicates

R, NR, MR, MSR, AP P  Programs
R1−R3, NR1−NR6, MR1−MR6  Actions

MSR1−MSR9, AP P 1−AP P 9

Variables  Domain  Read As

st.j {reset, normal}

State

sn.j

{0, 1}

Sequence number

par.j  Process ID  Parent
col.j  {green, red}  Color
root.j  Process ID  Root
new.j  {0, 1, 2}  New
d.j  {1...K}  Distance

inc.j

{0, 1, 2}

Incarnation number

ares.j Boolean

Application result

Propositional Connectives (in decreasing order of precedence)

¬  Negation
∧, ∨  Conjunction, disjunction
⇒, ⇐  Implication, consequence
≡, ≢  Equivalence, inequivalence

First-Order Quantifiers

∀, ∃  Universal, existential

Acknowledgment of support: Research supported in part by NSF grant CCR-93-08640 and OSU grant 221506.

References

[AG91] Y. Afek and E. Gafni. Bootstrap network resynchronization. In Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, pages 295–307, New York, 1991. ACM.

44 [AG93] A. Arora and M. G. Gouda. Closure and convergence: A foun-

dation of fault-tolerant computing. IEEE Transactions on Software Engineering, 19(11):1015–1027, 1993.

[AG94] A. Arora and M. G. Gouda. Distributed reset. IEEE Transactions on Computers, 43(9):1026–1038, 1994.

[AH93] E. Anagnostou and V. Hadzilacos. Tolerating transient and permanent failures. In WDAG93: Distributed Algorithms 7th International Workshop Proceedings, volume 725 of Lecture Notes in Computer Science, pages 174–188, Berlin, 1993. Springer-Verlag.

[AK98a] A. Arora and S. S. Kulkarni. Component-based design of multitolerance. IEEE Transactions on Software Engineering, 24(1):63–78, January 1998.

[AK98b] A. Arora and S. S. Kulkarni. Designing masking fault-tolerance via nonmasking fault-tolerance. IEEE Transactions on Software Engineering, 24(6), June 1998.

[AO94] B. Awerbuch and R. Ostrovsky. Memory-efficient and selfstabilizing network reset. In PODC94: Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing, pages 254–263, New York, 1994. ACM.

[APSV91] B. Awerbuch, B. Patt-Shamir, and G. Varghese. Selfstabilization by local checking and correction. In FOCS91: Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science, pages 268–277, Los Alamitos, CA, 1991. IEEE.

[APSVD94] B. Awerbuch, B. Patt-Shamir, G. Varghese, and S. Dolev. Selfstabilizing by local checking and global reset. In WDAG94: Distributed Algorithms 8th International Workshop Proceedings, volume 857 of Lecture Notes in Computer Science, pages 326– 339, Berlin, 1994. Springer-Verlag.

[Aro94] A. Arora. Efficient reconfiguration of trees: A case study in the methodical design of nonmasking fault-tolerance. In Proceedings

45 of the Third International Symposium on Formal Techniques in Real Time and Fault-Tolerance, pages 110–127, 1994. Also to appear in Science of Computer Programming.

[AS87] B. Alpern and F. B. Schneider. Proving Boolean combinations of deterministic properties. In Proceedings of the Second Symposium on Logic in Computer Science, pages 131–137, Ithaca, NY, 1987. IEEE Computer Society.

[DH97] Shlomi Dolev and Ted Herman. Superstabilizing protocols for dynamic distributed systems. Chicago Journal of Theoretical Computer Science, 1997(4), December 1997.

[Dij76] E. W. Dijkstra. A Discipline of Programming. Englewood Cliffs, NJ, 1976. Prentice-Hall.

[GM91] M. G. Gouda and N. Multari. Stabilizing communication protocols. IEEE Transactions on Computers, 40(4):448–458, 1991.

[Gri81] D. Gries. The Science of Programming. Berlin, 1981. Springer-Verlag.

[JV96] M. Jayaram and G. Varghese. Crash failures can drive protocols to arbitrary states. In ACM Symposium on Principles of Distributed Computing, New York, 1996. ACM.

[Tel89] G. Tel. Structure of distributed algorithms. PhD Thesis, University of Utrecht; also published by Cambridge University Press, 1989.

[TM94] S. Tsang and E. Magill. Detecting feature interactions in the intelligent network. Feature Interactions in Telecommunications Systems II, 1994.

[Var93] G. Varghese. Self-stabilization by local checking and correction. PhD Thesis, Massachusetts Institute of Technology; also Technical Report LCS-TR-583, Cambridge, MA, 1993.

46