Component Based Design of Multitolerant Systems.
AbstractThe concept of multitolerance abstracts problems in system dependability and provides a basis for improved design of dependable systems. In the abstraction, each source of undependability in the system is represented as a class of faults, and the corresponding ability of the system to deal with that undependability source is represented as a type of tolerance. Multitolerance thus refers to the ability of the system to tolerate multiple fault-classes, each in a possibly different way. In this paper, we present a component based method for designing multitolerance. Two types of components are employed by the method, namely detectors and correctors. A theory of detectors, correctors, and their interference-free composition with intolerant programs is developed, that enables stepwise addition of components to provide tolerance to a new fault-class while preserving the tolerances to the previously added fault-classes. We illustrate the method by designing a fully distributed multitolerant program for a token ring.
Introduction
Dependability is an increasingly relevant system-level requirement that encompasses the ability of
a system to deliver its service in a desirable manner, in spite of the occurrence of faults, security
intrusions, safety hazards, configuration changes, load variations, etc. Achieving this ability is
difficult, essentially because engineering a system for the sake of one dependability property, say
availability in the presence of faults, often interferes with another desired dependability property,
say security in presence of intrusions.
In this paper, to effectively reason about multiple dependability properties, we introduce the concept
of multitolerance. Each source of undependability is treated as a class of "faults" and each
dependability property is treated as a type of "tolerance". Thus, multitolerance refers to the ability
of a system to tolerate multiple classes of faults, each in a possibly different way.
Although there are many examples of multitolerant systems in practice [1 \Gamma 3] and there exists a
growing body of research that presents instances of multitolerant systems [4 \Gamma 9], we are not aware
of previous work that has considered the systematic design of multitolerance. Towards redressing
this deficiency, we present in this paper a formal method for the design of multitolerant systems.
To deal with the difficulty of interference between multiple types of tolerances, our method is based
on the use of components. More specifically, a multitolerant system designed using the method
consists of an intolerant system and a set of components, one for each desired type of tolerance.
Thus, the method reduces the complexity of design to that of designing the components and that of
correctly adding them to the intolerant system. Moreover, it enables reasoning about each type of
tolerance and the interferences between different types of tolerance at the level of the components
themselves, as opposed to involving the whole system.
The method further reduces the complexity of adding multiple components to an intolerant system
by adding each component in a stepwise fashion. In other words, the method considers the fault-
classes that an intolerant system is subject to in some fixed total order, say F1 :: Fn. A component
is added to the intolerant system so that it tolerates F1 in a desirable manner. The resulting system
is then augmented with another component so that it tolerates F2 in a desirable manner and its
tolerance to F1 is preserved. This process of adding a new tolerance and preserving all old tolerances
is repeated until all n fault-classes are accounted for. It follows that the final system is multitolerant
with respect to F1 :: Fn.
Components used in our method are built out of two building blocks, namely detectors and correctors,
that occur -albeit implicitly- in fault-tolerant systems. Intuitively, a detector "detects" whether
some predicate is satisfied by the system state; and a corrector detects whether some predicate is
satisfied by the system state and also "corrects" the system state in order to satisfy that predicate
whenever the predicate is not satisfied. Detectors can be used to ensure that each step of the system
is "safe" with respect to its "problem specification", while correctors can be used to ensure that
the system eventually reaches a state from where its problem specification is (re)satisfied. Thus,
in this paper, we are also able to show that components built out of detectors are sufficient for
designing "fail-safe" tolerance in programs, that components built out of correctors are sufficient
for designing "nonmasking" tolerance in programs, and that components built out of both detectors
and correctors are sufficient for designing "masking" tolerance in programs. (We will formally define
each of these terms shortly.)
The rest of this paper is organized as follows. In Section 2, we give formal definitions of programs,
their problem specifications, their faults, and their fault-tolerances. In Sections 3 and 4, we define
detectors and correctors, discuss their role in the design of fault-tolerant systems, and illustrate
how they can be designed hierarchically and efficiently. In Section 5, we present a theory of non-interference
for composing detectors and correctors with intolerant programs. In Section 6, we
define multitolerance and present our formal method for designing multitolerance. In Section 7, we
illustrate our method by designing a multitolerant token ring program. Finally, we discuss some
issues raised by our methodology in Section 8 and make concluding remarks in Section 9.
Preliminaries
In this section, we give formal definitions of programs, problem specifications, faults, and fault-
tolerances. The formalization of programs is a standard one, that of specifications is adapted from
Alpern and Schneider [9], and that of faults and fault-tolerances is adapted from earlier work of
the first author with Mohamed Gouda [10] (with the exception of the portion on fail-safe tolerance
which is new).
Programs.
A program is a set of variables and a finite set of actions. Each variable has a predefined
nonempty domain. Each action has a unique name, and is of the form:
The guard of each action is a boolean expression over the program variables. The statement of
each action is such that its execution atomically and instantaneously updates zero or more program
variables.
Notation. To conveniently write an action as a restriction of another action, we use the notation
hname
to define an action hname 0 i whose guard is obtained by restricting the guard of action hnamei
with hguard 0 i, and whose statement is identical to the statement of action hnamei. Operationally
speaking, hname 0 i is executed only if the guard of hnamei and the guard hguard 0 i are both true.
Likewise, to conveniently write a program as a restriction of another program, we use the notation
to define a program consisting of the set of actions hguardi - ac for each action ac of hprogrami.
Let p be a program.
Definition (State). A state of p is defined by a value for each variable of p, chosen from the
predefined domain of the variable.
Definition (State predicate). A state predicate of p is a boolean expression over the variables of p.
Note that a state predicate may be characterized by the set of all states in which the boolean
expression (of the state predicate) is true.
Definition (Enabled). An action of p is enabled in a state iff its guard (which is a state predicate)
is true in that state.
Definition (Computation). A computation of p is a fair, maximal sequences of states s
that for each j, j ? 0, s j is obtained from state s j \Gamma1 by executing an action of p that is enabled in
the state s j \Gamma1 . 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, i.e.,
the sequence cannot be further extended by executing an enabled action in its final state.
Problem specification.
problem specification is a set of sequences of states that is suffix closed and fusion
closed. Suffix closure of the set means that if a state sequence oe is in that set then so are all the
suffixes of oe. Fusion closure of the set means that if state sequences hff; x; fli and hfi; x; ffii are in that
set then so are the state sequences hff; x; ffii and hfi; x; fli, where ff and fi are finite prefixes of state
sequences, fl and ffi are suffixes of state sequences, and x is a program state.
Note that the state sequences in a problem specification may be finite or infinite. Following Alpern
and Schneider [9], it can be shown that any problem specification is the intersection of some "safety"
specification that is suffix closed and fusion closed and some "liveness" specification, defined next.
Definition (Safety). A safety specification is a set of state sequences that meets the following
condition: for each state sequence oe not in that set, there exists a prefix ff of oe, such that for all
state sequences fi, fffi is not in that set (where fffi denotes the concatenation of ff and fi).
Definition (Liveness). A liveness specification is a set of state sequences that meets the following
condition: for each finite state sequence ff, there exists a state sequence fi such that fffi is in that
set.
Defined below are some examples of problem specifications, namely, generalized pairs, closures,
and converges to. Let S and R be state predicates.
Definition (Generalized Pairs). A generalized pair (fSg; fRg) is a set of all state sequences, s
such that for each j; j - 0, if S is true at s j then R is true at s j+1 .
Definition (Closure). The closure of S, S   , is the set of all state sequences s
is true at s j then for all k, k - j, S is true at s k .
Definition (Converges to). S converges to R is the set of all state sequences s in the
intersection of S   and R   such that for all is true at s i then there exists k, k- i, where
R is true at s k .
Note that (fSg; converges to S.
Program correctness with respect to a problem specification.
Let SPEC be a problem specification.
Definition (Satisfies). p satisfies SPEC for S iff each computation of p that starts at a state where
S is true is in SPEC.
Definition (Violates). p violates SPEC for S iff it is not the case that p satisfies SPEC for
there exists a computation of p that starts at a state where S is true and is not in SPEC.
For convenience in reasoning about programs that satisfy special cases of problem specifications, we
introduce the following notational abbreviations.
Definition (Generalized Hoare-triples). fSg p fRg iff p satisfies the generalized pair (fSg; fRg) for
true.
Definition (Closed in p). S is closed in p iff p satisfies S   for true.
Note that it is trivially true that the state predicates true and false are closed in p.
Definition (Converges to in p). S converges to R in p iff p satisfies S converges to R for true.
Informally speaking, proving the correctness of p with respect to SPEC involves showing that p
satisfies SPEC for some state predicate S. (Of course, to be useful, the predicate S should not
be false.) Now, since problem specifications are suffix closed, we may without loss of generality
restrict our attention to proving that p satisfies the problem specification for some closed state
predicate S. We call such a state predicate S an invariant of p. Invariants enable proofs of program
correctness that eschew operational arguments about long (sub)sequences of states, and are thus
methodologically advantageous.
Definition (Invariant). S is an invariant of p for SPEC iff S is closed in p and p satisfies SPEC for
S.
Notational remark. Henceforth, whenever the problem specification is clear from the context, we
will omit it; thus, "S is an invariant of p" abbreviates "S is an invariant of p for SPEC ".
One way to calculate an invariant of p is to characterize the set of states that are reachable under
execution of p starting from some designated "initial" states. Experience shows, however, that for
ease of proofs of program correctness one may prefer to use invariants of p that properly include
such a reachable set of states. This is a key reason why we have not included initial states in the
definition of programs.
Techniques for the design of invariants have been articulated by Dijkstra [11], using the notion of
auxiliary variables, and by Gries [12], using the heuristics of state predicate ballooning and shrinking.
Techniques for the mechanical calculation of invariants have been discussed by Alpern and Schneider
[13].
Faults.
The faults that a program is subject to are systematically represented by actions whose execution
perturbs the program state. We emphasize that such representation is possible notwithstanding the
type of the faults (be they stuck-at, crash, fail-stop, omission, timing, performance, or Byzantine),
the nature of the faults (be they permanent, transient, or intermittent), or the ability of the program
to observe the effects of the faults (be they detectable or undetectable).
Definition (Fault-class). A fault-class for p is a set of actions over the variables of p.
Let T be a state predicate, S an invariant of p, and F a fault-class for p.
Definition (Preserves). An action ac preserves a state predicate T iff execution of ac in any state
where T is true results in a state where T is true.
is an F -span of p for S iff S ) T , T is closed in p, and each action of F
preserves T .
Thus, at each state where an invariant S of p is true, an F -span T of p for S is also true. Also, like
S, T is also closed in p. Moreover, if any action in F is executed in a state where T is true, the
resulting state is also one where T is true. It follows that for all computations of p that start at
states where S is true, T is a boundary in the state space of p up to which (but not beyond which)
the state of p may be perturbed by the occurrence of the actions in F .
Notational remark. Henceforth, we will ambiguously abbreviate the phrase "each action in F
preserves T " by "T is closed in F ". And, whenever the program p is clear from the context, we
will omit it; thus, "S is an invariant" abbreviates "S is an invariant of p" and "F is a fault-class"
abbreviates "F is a fault-class for p".
Fault-tolerances.
We are now ready to define what it means for a program p with an invariant S to tolerate a fault-class
F .
Definition -tolerant for S). p is F -tolerant for S iff there exists a state predicate T that satisfies
the following three conditions:
ffl At any state where S is true, T is also true. (In other words, S ) T .)
ffl Starting from any state where T is true, if any action in p or F is executed, the resulting state
is also one where T is true. (In other words, T is closed in p and each action in F preserves
.)
ffl Starting from any state where T is true, every computation of p alone eventually reaches a
state where S is true. (In other words, since S and T are closed in p, T converges to S in
p.)
This definition may be understood as follows. The state predicate T is an F -span of p for S- a
boundary in the state space of p up to which (but not beyond which) the state of p may be perturbed
by the occurrence of faults in F . If faults in F continue to occur, the state of p remains within this
boundary. When faults in F stop occurring, p converges from this boundary to the stricter boundary
in the state space where the invariant S is true.
It is important to note that there may be multiple such state predicates T for which p meets the above
three requirements. Each of these multiple T state predicates captures a (potentially different) type
of fault-tolerance of p. We will exploit this multiplicity in Section 6 in order to define multitolerance.
Types of fault-tolerances. We now classify three types of fault-tolerances that a program
can exhibit, namely masking, nonmasking, and fail-safe tolerance, using the above definition of
F -tolerance.
Informally speaking, this classification is based upon the extent to which the program satisfies its
problem specification in the presence of faults. Of the three, masking is the strictest type of tolerance:
in the presence of faults, the program always satisfies its safety specification, and the execution
of p after execution of actions in F yields a computation that is in both the safety and liveness
specification of p, i.e., the computation is in the problem specification of p. Nonmasking is less strict
than masking: in the presence of faults, the program need not satisfy its safety specification but,
when faults stop occurring, the program eventually resumes satisfying both its safety and liveness
specification; i.e., the computation has a suffix that is in the problem specification. Fail-safe is also
less strict than masking: in the presence of faults, the program always satisfies its safety specification
but, when faults stop occurring, the program need not resume satisfying its liveness specification;
i.e., the computation is in the safety specification -but not necessarily in the liveness specification- of
p. Formally, these three types of tolerance may be expressed in terms of the definition of F -tolerance,
as follows:
Definition (masking tolerant). p is masking tolerant to F for S iff p is F -tolerant for S and S is
closed in F . (In other words, if a fault in F occurs in a state where S is true, p continues to be in a
state where S is true.)
Definition (nonmasking tolerant). p is nonmasking tolerant to F for S iff p is F -tolerant for S and
S is not closed in F . (In other words, if a fault in F occurs in a state where S is true, p may be
perturbed to a state where S is violated. However, p then recovers to a state where S is true.)
Definition (fail-safe tolerant). p is fail-safe tolerant to F for S iff there exists a state predicate R
such that p is F -tolerant for S - R, S - R is closed in p and in F , and p satisfies the safety
specification (of the problem specification) for S - R. (In other words, if a fault in F occurs in
a state where S is true, p may be perturbed to a state where S or R is true. In the latter case,
the subsequent execution of p yields a computation that is in the safety specification of p but not
necessarily in the liveness specification.)
Notation. In the sequel, whenever the fault-class F and invariant S are clear from the context, we
omit them; thus, "masking tolerant" abbreviates "masking tolerant to F for S", and so on.
Detectors
In this section, we define the first of two building blocks which are sufficient for the design of
fault-tolerant programs, namely detectors. We also present the properties of detectors, show how
to construct them in a hierarchical and efficient manner, and discuss their role in the design of
fault-tolerance.
As mentioned in the introduction, intuitively, a detector is a program that "detects" whether a given
state predicate is true in the current system state. Implementations of detectors abound in practice:
Wellknown examples include comparators, error detection codes, consistency checkers, watchdog
programs, snoopers, alarms, snapshot procedures, acceptance tests, and exception conditions.
Z be state predicates of a program d and U be a state predicate that is
closed in d. We say that "Z detects X in d for U " iff the following three conditions hold:
ffl (Safeness) At any state where U is true, if Z is true then X is also true. (In other words,
U
ffl (Progress) Starting from any state where U -X is true, every computation of d either reaches
a state where Z is true or a state where X is false.
ffl (Stability) Starting from any state where U - Z is true, d falsifies Z only if it also falsifies X .
(In other words, fU - Zg d fZ - :Xg.)
The Safeness condition implies that a detector d never lets the predicate Z "witness" the detection
predicate X incorrectly when executed in states where U is true. The Progress condition implies
that in any computation of d starting from a state where U is true, if X is true continuously then d
eventually detects X by truthifying Z. The Stability condition implies that once Z is truthified, it
continues to be true unless X is falsified.
Remark. If the detection predicate X is closed in d, our definition of the detects relation reduces
to one given by Chandy and Misra [14]. We have considered this more general definition to accommodate
the case -which occurs for instance in nonmasking tolerance- where X denotes that
"something bad has happened"; in this case, X is not supposed to be closed since it has to be
subsequently corrected. (End of Remark.)
In the sequel, we will implicitly assume that the specification of a detector d (dn) is "Z detects X
in d for U " (respectively, "Zn detects Xn in dn for Un"). Also, we will implicitly assume that U
(Un) is closed in d (respectively, dn).
Properties. The detects relation is reflexive, antisymmetric, and transitive in its first two arguments

Lemma 3.0 Let X , Y , and Z be state predicates of d and U be a state predicate that is closed
in d. The following statements hold.
detects X in d for U
ffl If Z detects X in d for U , and X detects Z in d for U
then U
ffl If Z detects Y in d for U , and Y detects X in d for U
then Z detects X in d for U
Lemma 3.1 Let V be a state predicate such that U - V is closed in d. The following statements
hold.
ffl If Z detects X in d for U
then Z detects X in d for U-V
ffl If Z detects X in d for U , and V ) X
then Z-V detects X in d for U
ffl If Z detects X in d for U , and Z
then Z detects X-V in d for U
Compositions. Regarding the construction of detectors, there are cases where a detection
predicate X cannot be witnessed atomically, i.e., by executing at most one action of a detector
program. To detect such predicates, we give compositions of "small" detectors that yield "large"
detectors in a hierarchical and efficient manner. In particular, given two detectors, d1 and d2, we
compose them in two ways: (i) in parallel and (ii) in sequence.
Parallel composition of detectors. In the parallel composition of d1 and d2, denoted by d1[]d2, both
d1 and d2 execute in an interleaved fashion. Formally, the parallel composition of d1 and d2 is the
union of the (variables and actions of) programs d1 and d2.
Observe that '[]' is commutative: d1[](d2[]d3), and that
'-' distributes over `[]': g -
Theorem 3.2 Let Z1 detect X1 in d1 for U and Z2 detect X2 in d2 for U .
If the variables of d1 and d2 are mutually exclusive
then Z1-Z2 detects X1-X2 in d1[]d2 for U
Proof. The Safeness condition of d1[]d2 follows trivially from the Safeness of d1 and of d2. For
the Progress condition, we consider two cases, (i) a computation of d1[]d2 falsifies X1 - X2 and (ii)
a computation of d1[]d2 never falsifies X1 - X2: In the first case, Progress is satisfied trivially. In
the second case, eventually Z1 is truthified, and by Stability of d1, Z1 continues to be true in the
execution of d1. moreover, since the variables of d1 and d2 are disjoint, Z1 continues to be true in d2.
Likewise, Z2 is eventually truthified and continues to be true. Thus, Progress is satisfied. Finally,
the Stability condition is satisfied since Z1-Z2 can be falsified only if X1 or X2 are violated.
In d1[]d2, since d1 and d2 perform their detection concurrently, the time required for detection of
X1-X2 is the maximum time taken to detect X1 and to detect X2. (We are assuming that the
unit for measuring time allows both d1 and d2 to attempt execution of an action each.) Also, the
space complexity of d1[]d2 is the sum of the space complexity of d1 and d2, since the state space of
d1[]d2 is the union of the state space of d1 and of d2.
Sequential composition of detectors. In the sequential composition of d1 and d2, denoted by d1; d2,
d2 executes only after d1 has completed its detection, i.e., after the witness predicate Z1 is true.
Formally, the sequential composition of d1 and d2 is the program whose set of variables is the union
of the variables of d1 and d2 and whose set of actions is the union of the actions of d1 and of Z1-d2.
We postulate the axiom that ';' is left-associative: d1; d2;
Observe that ';' is not commutative, that `;' distributes over '[]': d1;
and that '-' distributes over `;': g - (d1;
Suppose, again, that the variables of d1 and d2 are mutually exclusive. In this case, starting from
any state where X1-X2 is true continuously, d1 eventually truthifies Z1. Only after Z1 is truthified
are the actions of d2 executed; these actions eventually truthify Z2. Since Z2 is truthified only
when Z1 (and, hence, X1) and X2 are true, it also follows that U
assume U
Theorem 3.3 Let Z1 detect X1 in d1 for U and Z2 detect X2 in d2 for U-X1.
If the variables of d1 and d2 are mutually exclusive, and U
then Z2 detects X1-X2 in d1; d2 for U
In d1; d2, the time (respectively, space) taken to detect X1-X2 is the sum of the time (respectively,
space) taken to detect X1 and to detect X2. The extra time taken by d1; d2 as compared to d1[]d2 is
warranted in cases where the witness predicate Z2 can be witnessed atomically but Z1-Z2 cannot.
Example: Memory access. Let us consider a simple memory access program that obtains the
value stored at a given address (cf. Figure 1). The program is subject to two fault-classes: The first
consists of protection faults which cause the given address to be corrupted so that it falls outside the
valid address space, and the second consists of page faults which remove the address and its value
from the memory.
For tolerance to the first fault-class, there is a detector d1 that uses the page table TBL to detect
whether the address addr is valid (X1). For tolerance to the second fault-class, there is another
detector d2 that uses the memory MEM to detect whether the given address is in memory (X2).
d2 MEM
addr

Figure

1: Memory access
Formally, these detectors are as follows (for simplicity, we assume that TBL is a set of valid addresses
and MEM is a set of objects of the form haddr; vali):
Thus, we may observe:
ffl Z1 detects X1 in d1 for U1 (1)
ffl Z2 detects X2 in d2 for U1 - X1 (2)
Note that an appropriate choice of initial state in U1 would be one where both Z1 and Z2 are false.
Note also that, in U1, Z1 is truthified only when X1 is true and that Z2 is truthified only when X1
and X2 are both true.
To detect X1-X2, we may compose d1 and d2 sequentially: d1 would first detect X1, and then d2
would detect X2. From Theorem 3.3, (1) and (2) we get:
ffl Z2 detects X1 - X2 in d1; d2 for U1 (3)
Application to design of fault-tolerance. Detectors suffice to ensure that a program satisfies
its safety specification. To see this, recall that a safety specification essentially rules out certain
finite prefixes of program computation. Now, consider any prefix of a computation that is not ruled
out by the safety specification. Execution of a program action starting from this prefix does not
violate the safety specification iff the elongated prefix is not ruled out by the safety specification.
In other words, for each program action ac there exists a set of computation prefixes from which
execution of ac does not violate the safety specification. It follows that there exists a "detection"
state predicate such that execution of ac in any state where that state predicate is true does not
violate the safety specification. (From the fusion closure of the safety specification, it suffices that
this state predicate characterize a set of states, each state st of which yields upon executing ac
a successor state st 0 such that there is some state sequence in the safety specification in which st
and st 0 occur consecutively in that order.) Now, if detectors can be added to the program so that
for each program action ac a detection predicate of ac is witnessed, and each program action can
be restricted to execute only if its corresponding witness predicate is true, the resulting program
satisfies the safety specification.
To design fail-safe tolerance to F for S, we need to ensure that upon starting from a state where
S is true, the execution of p in the presence of F always yields a computation that is in the safety
specification of p. It follows that detectors suffice for the design of fail-safe tolerance.
Likewise, to design masking tolerance to F for S, we need to ensure that upon starting from a state
where S is true, the execution of p in the presence of F never violates the safety specification and
the execution of p after execution of actions in F always yields a computation that is in both the
safety and the liveness specification of p, i.e., that computation is in the problem specification of
p. (From the fusion closure of the problem specification, it follows that a computation of p that is
in the safety specification and that has a suffix in the problem specification is itself in the problem
specification.) Now, regarding safety, it suffices that detectors be added to p. (Regarding liveness,
it suffices that correctors be added to p, as discussed in the next section.)
Detectors can also play a role in the design of nonmasking tolerance: They may be used to detect
whether the program is perturbed to a state where its invariant is false. As discussed in the next
section, such detectors can be systematically composed with correctors that restore the program to
a state where its invariant is true.
In this section, we discuss the second set of building blocks, namely correctors, in a manner analogous
to our discussion of detectors.
As mentioned in the introduction, intuitively, a corrector is a detector that also "corrects" the
program state whenever it detects that its detection predicate is false in the current system state.
Implementations of correctors also abound in practice: Wellknown examples include voters, error
correction codes, reset procedures, rollback recovery, rollforward recovery, constraint (re)satisfaction,
exception handlers, and alternate procedures in recovery blocks.
Z be state predicates of a program c and U be closed in c. We say that "Z
corrects X in c for U " iff the following four conditions holds:
ffl (Safeness) At any state where U is true, if Z is true then X is also true. (In other words,
U
ffl (Convergence) Starting from any state where U is true, every computation of c eventually
reaches a state where X is true, and subsequently, X continues to be true thereafter. (In other
words, U converges to X in c.)
Starting from any state where U - X are true, every computation of c either
reaches a state where Z is true or a state where X is false.
ffl (Stability) Starting from any state where U -Z is true, c falsifies Z only if it also falsifies X .
(In other words, fU - Zg c fZ - :Xg.)
From the above definition, it follows that if Z corrects X in c for U , then Z detects X in c for U .
It also follows, that U - X is closed in c (cf. Convergence). Consequently, starting from any state
where U -X is true, every computation of c reaches a state where Z is true (cf. Progress). moreover,
U - Z is closed in c (cf. Stability).
Remark. If the witness predicate Z is identical to the correction predicate X , our definition of
the corrects relation reduces to one given by Arora and Gouda [10]. We have considered this more
general definition to accommodate the case -which occurs for instance in masking tolerance- where
the witness predicate Z can be checked atomically but the correction predicate X cannot.
(End of Remark.)
Properties. The corrects relation is antisymmetric and transitive in its first two arguments:
Lemma 4.0 Let X , Y , and Z be state predicates of c and U be a state predicate that is closed in
c. The following statements hold.
ffl If Z corrects X in c for U , and X corrects Z in c for U
then U
ffl If Z corrects Y in c for U , and Y corrects X in c for U
then Z corrects X in c for U
Lemma 4.1 Let V be a state predicate such that U - V is closed in c. Then the following
statements hold.
ffl If Z corrects X in c for U
then Z corrects X in c for U - V
ffl If Z corrects X in c for U and V ) X
then Z-V corrects X in c for U
Compositions. Analogous to detection predicates that cannot be witnessed atomically, there exist
cases where a correction predicate X cannot be corrected atomically, i.e., by executing at most one
step (action) of a corrector. To correct such predicates, we construct "large" correctors from "small"
correctors just as we did for detectors.
Parallel composition of correctors. The parallel composition of two correctors c1 and c2, denoted
by c1[]c2, is the union of the (variables and actions of) programs c1 and c2.
Theorem 4.2 Let Z1 correct X1 in c1 for U and Z2 correct X2 in c2 for U .
If the variables of c1 and c2 are mutually exclusive
then Z1-Z2 corrects X1-X2 in c1[]c2 for U
The time taken by c1[]c2 to correct X1-X2 is the maximum of the time taken to correct X1 and to
correct X2. The space taken is the corresponding sum.
Sequential composition of correctors. The sequential composition of correctors c1 and c2, denoted
by c1; c2, is the program whose set of variables is the union of the variables of c1 and c2 and whose
set of actions is the union of the actions of c1 and of Z1 - c2.
Theorem 4.3 Let Z1 correct X1 in c1 for U and Z2 correct X2 in c2 for (U -X1).
If the variables of c1 and c2 are mutually exclusive, and U
then Z2 corrects X1-X2 in c1; c2 for U
The time (respectively, space) taken by c1; c2 to correct X1-X2 is the sum of the time (respectively,
space) taken to correct X1 and to correct X2.
As mentioned in the previous section, one way to design a corrector for X is by sequential composition
of a detector and a corrector: the detector first detects whether :X is true and, using this witness,
the corrector then establishes X .
Theorem 4.4 Let Z detect :X in d for U , Z
, and X correct X in c for U - Z 0
If X is closed in d, and fU - Zg c fZ - Xg
then X corrects X in (:Z - d); c for U
If c is atomic, i.e., c satisfies Progress and Convergence in at most one step, the following corollary
holds.
Corollary 4.5 Let Z detect :X in d for U , Z
, and X correct X in c for U - Z 0
If X is closed in d, and c is atomic
then X corrects X in d; c for U
Another way to design a corrector for X is by sequential composition of a corrector and a detector:
the corrector first satisfies its correction predicate X and then the detector satisfies the desired
witness predicate Z.
Theorem 4.6 Let X correct X in c for U , and Z detect X in d for U .
If X is closed in d
then Z corrects X in (:X - c); d for U
Again, if d is atomic, the following corollary holds.
Corollary 4.7 Let X correct X in c for U , and Z detect X in d for U .
If X is closed in d and c is atomic
then Z corrects X in c; d for U
Example: Memory access (continued). If the given address is valid but is not in memory,
an object of the form haddr; \Gammai has to be added to the memory. (We omit the details of how this
object is obtained, e.g., from a disk, a remote memory, or a network.) Thus, there is a corrector, c,
which is formally specified as follows:
addr
d2
c

Figure

2: Memory access
Thus, we may observe:
ffl X2 corrects X2 in c for true (4)
ffl X2 corrects X2 in c for U1 (5)
ffl X2 corrects X2 in c for U1 - X1 (6)
Before detector d2 can witness that the value of the address is in memory, corrector c should execute.
Hence, we compose c and d2 sequentially. From Corollary 4.7, (2) and (6) we have:
ffl Z2 corrects X2 in c; d2 for U1 - X1 (7)
moreover, detector d1 should witness that the address is valid, before either corrector c or detector
d2 execute. Hence, we compose d1 and c; d2 sequentially. Recall from Section 3 that Z1 detects X1
in d1 for U1. Also, X1 is closed in d1. Hence, if d1 is started in a state satisfying U1 - X1, it will
eventually satisfy Z1. It follows that Z1 corrects X1 in d1 for U1 - X1. Therefore, from Theorem
4.3 and (9), we have:
ffl Z2 corrects X1 - X2 in d1; (c; d2) for U1 - X1 (8)
Application to design of fault-tolerance. Correctors suffice to ensure that computations
of a program have a suffix in the problem specification. To see this, observe that if the correction
predicate of a corrector is chosen to be an invariant of the program, the corrector ensures the program
will eventually reach a state where that invariant is true and henceforth the program computation
is in the problem specification.
To design nonmasking tolerance to F for an invariant S, we need to ensure that upon starting from a
state where S is true, execution of p will, after execution of actions in F , always yield a computation
that has a suffix in the problem specification. It follows that correctors whose correction predicate
is the invariant S suffice for the design of nonmasking tolerance.
Likewise, to design masking tolerance to F for S, we need to ensure that upon starting from a
state where S is true, execution of p in the presence of F never violates its safety specification and
execution of p after execution of actions in F always yields a computation that is in the problem
specification of p. For the latter guarantee, it suffices that correctors be added to p (and, for the
former, it suffices that detectors be added to p, as discussed in the previous section).
5 Composition of Detector/Corrector Components and Programs
In this section, we discuss how a detector/corrector component is correctly added to a program
so that the resulting program satisfies the specification of the component. As far as possible, the
proof of preservation should be simpler than explicitly proving all over again that the specification
is satisfied in the resulting program. This is achieved by a compositional proof that shows that
the program does not "interfere" with the component, i.e., the program and the component when
executed concurrently do not violate the specification of the component.
Compositional proofs of interference-freedom have received substantial attention in the formal methods
community [15\Gamma19] in the last two decades. Drawing from these efforts, we identify several simple
sufficient conditions to ensure that when a program p is composed with a detector (respectively a
corrector) q, the safety specification of q, viz Safeness and Stability, and liveness specification, viz
Progress and Convergence, are not violated.
Sufficient conditions for satisfying the safety specification of a detector. To demonstrate that
p does not interfere with Safeness and Stability, a straightforward sufficient condition is that the
actions of p be a subset of the actions of q; this occurs, for instance, when program itself acts as
a detector. Another straightforward condition is that the variables of p and q be disjoint. A more
general condition is that p only reads (but not writes) the variables of q; in this case, p is said to be
"superposed" on q.
Sufficient conditions for satisfying the liveness specification of a detector. The three conditions
given above also suffice to demonstrate that p does not interfere with Progress of q, provided that
the actions of p and q are executed fairly. Yet another condition for satisfying Progress of q is to
require that q be "atomic", i.e., that q achieves its Progress in at most one step. It follows that even
if p and q execute concurrently, Progress of q is satisfied.
Alternatively, require that p executes only after Progress of q is achieved. It follows that p cannot
interfere with Progress of q. Likewise, require that p terminates eventually. It follows that after p
has terminated, execution of q in isolation satisfies its Progress.
More generally, require that there exists a variant function f (whose range is over a well-founded
set) such that execution of any action in p or q reduces the value of f until Progress of q is achieved.
It follows that even if q is executed concurrently with p, Progress of q is satisfied.
The sufficient conditions outlined above are formally stated in Table 1. Sufficient conditions for the
case of a corrector are similar.
In the following theorems, let Z detect X in q for U , and let U be closed in p.
Theorem 5.0 (Superposition)
If q does not read or write any variable written by p, and
only reads the variables written by q
then Z detects X in q[]p for U
Theorem 5.1 (Containment)
If actions of p are a subset of q
then Z detects X in q[]p for U
Theorem 5.2 (Atomicity)
If fU - Zg p fZ - :Xg, and q is atomic
then Z detects X in q[]p for U
Theorem 5.3 (Order of execution)
If fU - Zg p fZ - :Xg
then Z detects X in q; p for U
Theorem 5.4 (Termination)
If fU - Zg p fZ - :Xg, and U converges to V in p[]q
then Z detects X in (:V - p)[]q for U
Theorem 5.5 (Variant function)
If fU - (0!f =K)g q f(0!f
then Z detects X in q[]p for U

Table

Sufficient conditions for interference-freedom
The discussion above has addressed how to prove that a program does not interfere with a component,
but not how a component does not interfere with a program. Standard compositional techniques
suffice for this purpose. In practice, detectors such as snapshot procedures, watchdog programs, and
snooper programs typically read but not write the state of the program to which they are added.
Thus, these detectors do not interfere with the program. Likewise, correctors such as reset, rollback
recovery, and forward recovery procedures are typically restricted to execute only in states where
the invariant at hand is false. Thus, these correctors do not interfere with the program.
Example: Memory access (continued). Consider an intolerant program p for memory access
that assumes that the address is valid and is currently present in the memory. For ease of exposition,
we let p access only one memory location instead of multiple locations. Thus, p is as follows:
For p to not interfere with the specification of the corrector d1; (c; d2), it suffices that p execute only
after Z2, the witness predicate of d1; (c; d2), is satisfied. Hence, d1; (c; d2) and p should be composed
in sequence. From the analogue of Theorem 5.3 for the case of correctors, we have that p does not
interfere with d1; (c; d2):
ffl Z2 corrects X1 - X2 in d1; (c; d2); p for U1 - X1
6 Designing Multitolerance
In this section, we first define multitolerance and then present our method for compositional, stepwise
design of multitolerant programs.
Let p be a program with invariant S, F1::Fn be n fault-classes, and l1; l2; ::; ln be
types of tolerance (i.e., masking, nonmasking or fail-safe). We say that p is multitolerant to F1::Fn
for S iff for each fault-class F j; 1-j- n, p is lj-tolerant to F j for S.
The definition may be understood as follows: In the presence of faults in class F j, p is perturbed
only to states where some F j-span predicate for S, T j, is true. (Note that there exists a potentially
different fault-span for each fault-class.) After faults in F j stop occurring, subsequent execution
of p always yields a computation that is in the problem specification as prescribed by the type of
tolerance lj. For example, if lj is fail-safe, each computation of p starting from a state where T j is
true is in the safety specification.
Example: Memory access (continued). Observe that the memory access program, d1; (c; d2); p,
discussed in Section 5, is multitolerant to the classes of protection faults and page faults: it is fail-safe
tolerant to the former and masking tolerant to latter. In particular, in the presence of a page
fault, it always obtains the correct data from the memory. And in the presence of a protection fault,
it obtains no data value.
Compositional and stepwise design method. As outlined in the introduction, our method
starts with a fault-intolerant program and, in a stepwise manner, considers the fault-classes in some
fixed total order, say F1::Fn. In the first step, the intolerant program is augmented with detector
and/or corrector components so that it is l1-tolerant to F 1. The resulting program is then augmented
with other detector/corrector components, in the second step, so that it is l2-tolerant to F2 and its
l1-tolerance to F1 is preserved. And so on until, in the n-th step, the ln-tolerance to Fn is added
while preserving the l1::ln\Gamma1tolerances to F1::Fn\Gamma1. The multitolerant program designed thus has
the structure shown in Figure 3.
detectors and/or correctors for Fn
Fault-intolerant program
detectors and/or correctors for F1
detectors and/or correctors for F2

Figure

3: Structure of a multitolerant program designed using our method
First step. Let p be the intolerant program with invariant S. By calculating an F 1-span of p for S,
detector and corrector components can be designed for satisfying l1-tolerance to F 1. As discussed
in Section 3 and 4, it suffices to add detectors to design fail-safe tolerance to F 1, correctors to design
nonmasking tolerance to F 1, and both detectors and correctors to design masking tolerance to F 1.
tolerant
program
Nonmasking
program
Failsafe
correctors
detectors and correctors
Intolerant program
Masking tolerant program
detectors
tolerant

Figure

4: Components that suffice for design of various tolerances
Note that the detectors and correctors added to p are also subject to F . Hence, they themselves have
to be tolerant to F . But it is not necessary that they be masking tolerant to F . More specifically, it
suffices that detectors added to design fail-safe tolerance be themselves fail-safe tolerant to F ; this is
because if the detectors do not satisfy their liveness specification in the presence of F , the resulting
program can be made to not satisfy the liveness specification of p in the presence of F . Likewise, it
suffices that correctors added to design nonmasking tolerance be themselves nonmasking tolerant to
F ; this is because as long as the computations of the correctors have suffixes that are in their safety
and liveness specification, the computations of the resulting program can be made to have suffixes
in the safety and liveness specification of p. Lastly, as can be expected, it suffices that the detectors
and correctors added to design masking tolerance be themselves masking tolerant to F . (See Figure
5.)
In practice, the detectors and correctors added to p often possess the desired tolerance to F trivially.
But if they do not, one way to design them to be tolerant to F is by the analogous addition of more
detectors and correctors. Another way is to design them to be self tolerant, without using any more
detector and corrector components, as is exemplified by self-checking, self-stabilizing, and inherently
fault-tolerant designs.
tolerant
program
nonmasking components
tolerant
program
Intolerant program
Failsafe
Masking tolerant program
Nonmasking
masking components

Figure

5: Tolerance requirements for the components
With the addition of detector and/or corrector components to p, it remains to show that, in the
resulting program p1, the components do not interfere with p and that p does not interfere with
the components. Note that p1 may contain variables and actions that were not in p and, hence,
invariants and fault-spans of p1 may differ from those of p. Therefore, letting S1 be an invariant of
p1 and T1 be an F 1-span of p1 for S1, we show the following.
1. In the absence of F 1, i.e., in states where S1 is true, the components do not interfere with p,
i.e., each computation of p is in the problem specification even if it executes concurrently with
the new components.
2. In the presence of F 1, i.e., in states where T1 is true, p does not interfere with the components,
i.e., each computation of the components is in the components' specification (in the sense
prescribed by its type of tolerance) even if they execute concurrently with p.
The addition of the detectors and correctors may itself be simplified by using a stepwise
For instance, to design masking tolerance, we may first augment the program with detectors, and
then augment the resulting fail-safe tolerant program with correctors. Alternatively, we may first
augment the program with correctors, and then augment the resulting nonmasking tolerant program
with detectors. (See Figure 6.) For reasons of space, we refer the interested reader to [20] for the
formal details of this two-stage approach for designing masking tolerance.000000000000000000000000000000000000000000000000000000111111111111111111111111111111111111111111111111111111111111111000000000000000000000000000000000000000000000000000000000000000111111111111111111111111111111111111111111111111111111tolerant
Masking tolerant program
Intolerant program
correctors detectors
program
correctors
program
detectors
Failsafe
Nonmasking
tolerant

Figure

Two approaches for stepwise design of masking tolerance
Second step. This step adds l2-tolerance to F2 and preserves the l1-tolerance to F 1. To add l2-
tolerance to F 2, just as in the first step, we add new detector and corrector components to p1. Then,
we account for the possible interference between the executions of these added components and of
p1. More specifically, letting S2 be an invariant of the resulting program p2, T21 be an F 1-span of
p2 for S2, and T22 denote an F 2-span of p2 for S2, we show the following.
1. In the absence of F1 and F 2, i.e., in states where S2 is true, the newly added components
do not interfere with p1, i.e., each computation of p1 is in the problem specification even if it
executes concurrently with the new components.
2. In the presence of F 2, i.e., in states where T22 is true, p1 does not interfere with the new com-
ponents, i.e., each computation of the new components is in the new components' specification
(in the sense prescribed by its type of tolerance) even if they execute concurrently with p1.
3. In the presence of F 1, i.e., in states where T21 is true, the newly added components do not
interfere with the l1-tolerance of p1 for F 1, i.e., each computation of p1 is in the specification,
l1-tolerant to F 1, even if p1 executes concurrently with the new components.
Remaining steps. For the remaining steps of the design, where we add tolerance to F3::Fn, the
procedure of the second step is generalized accordingly.
7 Case Study in Multitolerance Design : Token Ring
Recall the mutual exclusion problem: Multiple processes may each access their critical section
provided that at any time at most one process is accessing its critical section. moreover, no process
should wait forever to access its critical section, assuming that each process leaves its critical section
in finite time.
Mutual exclusion is readily achieved by circulating a token among processes and letting each process
enter its critical section only if it has the token. In a token ring program, in particular, the processes
are organized in a ring and the token is circulated along the ring in a fixed direction.
In this case study, we design a multitolerant token ring program. The program is masking tolerant
to any number, K, of faults that each corrupt the state of some process detectably. Its tolerance
is continuous in the sense that if K state corruptions occur, it corrects its state within \Theta(K) time.
Thus, a quantitatively unique measure of tolerance is provided to each FK, where FK is the fault-
class that causes at most K state corruptions of processes.
By detectable corruption of the state of a process, we mean that the corrupted state is detected
by that process before any action inadvertently accesses that state. The state immediately before
the corruption may, however, be lost. (For our purposes, it is irrelevant as to what caused the
corruption; i.e., whether it was due to the loss of a message, the duplication of a message, timing
faults, the crash and subsequent restart of a process, etc.)
We proceed as follows: First, we describe a simple token ring program that is intolerant to detectable
state corruptions. Then, we add detectors and correctors so as to achieve masking tolerance to the
fault that corrupts the state of one process. Progressively, we add more detectors and correctors so
as to achieve masking tolerance to the fault-class that corrupts process states at most K, K ? 1,
times.
7.1 Fault-Intolerant Binary Token Ring
Processes 0::N are organized in a ring. The token is circulated along the ring such that process j,
the token to its successor j +1. (In this section, + and \Gamma are in modulo N+1
Each process j maintains a binary variable x:j. Process j; j 6= N , has the token iff x:j
differs from its successor x:(j +1) and process N has the token iff x:N is the same as its successor
x:0.
The program, TR, consists of two actions for each process j. Formally, these actions are as follows
(where
Invariant. Consider a state where process j has the token. In this state, since no other process
has a token, the x value of all processes 0::j is identical and the x value of all processes (j+1)::N is
identical. Letting X denote the string of binary values x:0; x:1; :::; x:N , we have that X satisfies the
regular expression (0 l 1 (N+1\Gammal) [ 1 l 0 (N+1\Gammal) ), which denotes a sequence of length N+1 consisting of
zeros followed by ones or ones followed by zeros. Thus, an invariant of the program TR is
7.2 Adding Tolerance to 1 State Corruption
Based on our assumption that state corruption is detectable, we introduce a special value ?, such
that when any process j detects that its state (i.e., the value of x:j) is corrupted, it resets x:j to ?.
We can now readily design masking tolerance to a single corruption of state at any process j by
ensuring that (i) the value of x:j is eventually corrected so that it is no longer ? and (ii) in the
interim, no process (in particular, j+1) inadvertently gets the token as a result of the corruption of
x:j.
For (i), we add a corrector at each process j: it corrects x:j from ? to a value that is either 0 or
1. The corrector at j, j 6= 0, copies x:(j \Gamma 1); the corrector at
the corrector action at j has the same statement as the action of TR at j, and we can merge the
corrector and TR actions.
For (ii), we add a detector at each process Its detection predicate is and it has no
actions. The witness predicate of this detector (which, in this case, is the detection predicate itself)
is used to restrict the actions of program TR at j. Hence, the actions of TR at j execute only when
As a result, the execution of actions of TR is always safe (i.e., these actions
cannot inadvertently generate a token).
The augmented program, PTR, is
Fault Actions. When the state of x:j is corrupted, x:j is set to ?. Hence, the fault action is
Proof of interference-freedom. Starting from a state where S TR is true, in the presence of faults
that set the x value of a process to ?, string X always satisfies the regular expression (0 [ ?) l (1 [
?) (N+1\Gammal) or (1 [ ?) l (0 [ ?) (N+1\Gammal) . Thus, an invariant of PTR is SPTR , where
Consider the detector at j: Both its detection and witness predicates are x:(j \Gamma 1) 6= ?. Since the
detects relation is trivially reflexive in its first two arguments, it follows that
in PTR. In other words, the detector is not interfered by any other actions.
Consider the corrector at j: Both its correction and witness predicates are x:j 6= ?. Since the
program actions are identical to the corrector actions, by Theorem 5.1, the corrector actions are not
interfered by the actions of TR. Also, since the detectors have no actions, the detectors at processes
other than j do not interfere with the corrector at j; moreover, since at most one x value is set to
?, when x:j =? and thus the corrector at j is enabled, the witness predicate of the detector at j is
true and hence the corrector at j is not interfered by the detector at j.
Consider the program actions of TR: Their safety follows from the safety of the detectors, described
above. And, their progress follows from the progress of the correctors, which ensure that starting
from a state where SPTR is true and a process state is corrupted every computation of PTR reaches
a state where S TR is true, and the progress of the detectors, which ensures that no action of TR is
indefinitely blocked from executing.
Observe that our proof of mutual interference-freedom illustrates that we do not have to re-prove
the correctness of TR for the new invariant. Observe, also, that if the state of process j is corrupted
then within \Theta(1) time the corrector at j corrects the state of j.
7.3 Adding Tolerance to 2::N State Corruptions
The proof of non-interference of program PTR can be generalized to show that PTR is also masking
tolerant to the fault-class that twice corrupts process state.
The generalization is self-evident for the case where the state corruptions are separated in time so
that the first one is corrected before the second one occurs. For the case where both state corruptions
occur concurrently, say at processes j and k, we need to show that the correctors at j and k truthify
interference by each other and the other actions of the program. Let
us consider two subcases: (i) j and k are non-neighboring, and (ii) j and k are neighboring.
For the first subcase, j and k correct x:j and x:k from their predecessors j\Gamma1 and k\Gamma1, respectively.
This execution is equivalent to the parallel composition of the correctors at j and k. By Theorem
4.2, PTR reaches a state where x:j and x:k are not ?.
For the second subcase (letting j be the predessor of k), j corrects x:j from its predecessor
truthifies x:j 6=? and then terminates. Since the corrector at j does not read any variables written by
the corrector at k. Thus, from the analogue of Theorem 5.0 for the case of correctors, the corrector
at j is not interfered by the corrector at k. After x:j 6= ? is truthified, the corrector at k corrects
x:k from its predecessor j. By Theorem 4.4, the corrector at k is not interfered by the corrector
at j. Since the correctors at j and k do not interfere with each other, it follows that the program
reaches a state where x:j and x:k are not ?.
In fact, as long as the number of faults is at most N , there exists at least one process j with x:j 6=?.
PTR ensures that the state of such a j eventually causes j+1 to correct its state to x:(j
Such corrections will continue until no process has its x value set to ?. Hence, PTR tolerates up to
N faults and the time required to converge to S TR is \Theta(K), where K is the number of faults.
7.4 Adding Tolerance to More Than N State Corruptions
Unfortunately, if more than N faults occur, program PTR deadlocks iff it reaches a state where the
x value of all processes is ?. To be masking tolerant to the fault-classes that corrupt the state of
processes more than N times, a corrector is needed that detects whether the state of all processes is
? and, if so, corrects the program to a state where the x value of some process (say 0) to be equal
to 0 or 1.
Since the x values of all processes cannot be accessed simultaneously, the corrector detects in a
sequential manner whether the x values of all processes are ?. Let the detector added for this
purpose at process j be denoted as dj and the (sequentially composed) detector that detects whether
the x values of all processes is corrupted be dN
To design dj, we add a value ? to the domain of x:j. When dN detects that x:N is equal to ?, it
sets x:N to ?. Likewise, when dj, detects that x:j is equal to ?, it sets x:j to ?. Note that
since dj is part of the sequential composition, it is restricted to execute only after j+1 has completed
its detection, i.e., when x:(j+1) is equal to ?. It follows that when j completes its detection, the x
values of processes j::N are corrupted. In particular, when d0 completes its detection, the x values
of all processes are corrupted. Hence, when x:0 is set to ?, it suffices for the corrector to reset x:0
to 0.
To ensure that while the corrector is executing, no process inadvertently gets the token as a result
of the corruption of x:j, we add detectors that restrict the actions of PTR at j+1 to execute only
in states where x:j 6=? is true.
Actions. Program FTR consists of five actions at each process j. Like PTR, the first two actions,
FTR1 and FTR2, pass the token from j to j+1 and are restricted by the trivial detectors to execute
only when x:(j \Gamma1) is neither ? nor ?. Action FTR3 is dN ; it lets process N change x:N from ? to
?. Action FTR4 is dj for j ! N . Action FTR5 is the corrector action at process 0: it lets process
correct x:0 from ? to 0. Formally, these actions are as follows:
Invariant. Starting from a state where SPTR is true, the detector can change the trailing ? values
in X to ?. Thus, FTR may reach a state where X satisfies the regular expression (1 [ ?) l (0 [
Subsequent state corruptions may perturb X to
the form (1 [?) l (0 [?) m (? [?) (N+1\Gammal\Gammam) [ (0 [?) l (1 [?) m (?[?) (N+1\Gammal\Gammam) . Since all actions
preserve this last predicate, an invariant of FTR is
(0
Proof of interference-freedom. To design FTR, we have added a corrector (actions FTR3 \Gamma 5) to
program PTR to ensure that for some j, x:j is not corrupted, i.e., the correction predicate of this
corrector is V , where This corrector is of the form dN ; d(N\Gamma1); :::; d0; c0,
where each dj is an atomic detector at process j and c0 is an atomic corrector at process 0.
The detection predicate of dN is :V and its witness predicate is x:0 =?. To show
that this detector in isolation satisfies its specification, observe that
1. x:N =? detects in dN for SFTR .
2.
for (SFTR
From (1) and (2), by Theorem 3.3, x:(N \Gamma1) =? detects
. Using the same argument, x:0=? detects
in dN
Now, observe that SFTR converges to V in dN violated execution of
eventually truthify x:0 =?, and execution of c0 will truthify V . Thus, V
corrects V in dN
The corrector is not interfered by the actions FTR1 and FTR2. This follows from the fact that
FTR1 and FTR2 do not interfere with each dj and c0 (by using Theorem 5.2).
In program FTR, we have also added a detector at process j that detects x:(j\Gamma1) 6=?. As described
above (for the 1 fault case), this detector does not interfere with other actions, and it is not interfered
by other actions.
Finally, consider actions of program PTR: their safety follows from the safety of the detector
described above. Also, starting from any state in SFTR , the program reaches a state where x value
of some process is not corrupted. Starting from such a state, as in program PTR, eventually the
program reaches a state where S TR is truthified, i.e., no action of PTR is permanently blocked.
Thus, the progress of these actions follows.
Theorem 7.0 Program FTR is masking tolerant for invariant SFTR to the fault-classes FK,
K- 1, where FK detectably corrupts process states at most K times. moreover, SFTR converges
to S TR in FTR within \Theta(K) time.
Remark. We emphasize that the program FTR is masking tolerant to the fault-classes FK for the
invariant SFTR and not for S TR . Thus, in the presence of faults in FK, SFTR continues to be true
although S TR may be violated. Process j, j !N , has a token iff x:j differs from x:(j+1) and neither
x:j nor x:(j+1) is corrupted, and process N has a token iff x:N is the same as x:0 and neither x:N
nor x:0 is corrupted. Thus, in a state where SFTR is true at most one process has a token. Also
starting from such a state eventually the program reaches a state where S TR is true. Starting from
such a state, each process can get then token. Thus, starting from any state in SFTR , computations
of FTR are in the problem specification of the token ring.
In this section, we address some of the issues that our method for design of multitolerance has raised.
We also discuss the motivation for the design decisions made in this work.
Our formalization of the concept of multitolerance uses the abstractions of closure and convergence.
Can other abstractions be used to formalize multitolerance? What are the advantages of using closure
and convergence?
In principle, one can formulate the concept of multitolerance using abstractions other than closure
and convergence. As pointed out by John Rushby [21], the approaches to formulate fault-tolerance
can be classified into two: specification approaches and calculational approaches.
In specification approaches, a system is regarded as a composition of several subsystems, each with a
standard specification and one or more failure specifications. A system is fault-tolerant if it satisfies
its standard specification when all components do, and one of its failure specifications if some of its
components depart from their standard specification. One example of this approach is due to Herlihy
and Wing [22] who thus formulate graceful degradation, which is a special case of multitolerance.
In calculational approaches, the set of computations permissible in the presence of faults is calculated.
A system is said to be fault-tolerant if this set satisfies the specification of the system (or an
acceptably degraded version of it). Our approach is calculational since we compute the set of states
that are potentially reachable in the presence of faults (fault-span).
While other approaches may be used to formulate the design of multitolerance, we are not aware
of any formal methods for design of multitolerance using them. moreover, in our experience, the
structure imposed by abstractions of closure and convergence has proven to be beneficial in several
ways: (1) it has enabled us to discover the role of detectors and correctors in the design of all tolerance
properties (cf. Sections 3 and 4); (2) it has yielded simple theorems for composing tolerance actions
and underlying actions in an interference-free manner (cf. Sections 5 and 6); (3) it has facilitated
our design of novel and complex distributed programs whose tolerances exceed those of comparable
programs designed otherwise [5, 10, 20, 23, 24, 25].
We have represented faults as state perturbations. This representation readily handles transient
faults, but does it also handle permanent faults? intermittent faults? detectable faults? undetectable
All these faults can indeed be represented as state perturbations. The token ring case study illustrates
the use of state perturbations for various classes of transient faults. In an extended version
of this paper [24], we present a case study of tree-based mutual exclusion which illustrates the
analogous representation for permanent faults and for detectable or undetectable faults.
It is worth pointing out that representing permanent and intermittent faults, such as Byzantine
faults and fail-stop and repair faults, may require the introduction of auxiliary variables [5, 10].
For example, to represent Byzantine faults that affects a process j, we may introduce an auxiliary
boolean variable byz:j that is true iff j is Byzantine. If j is not Byzantine, it executes its "normal"
actions. Otherwise, it executes some "abnormal" actions. When the Byzantine fault occurs, byz:j is
truthified, thus, permitting j to execute its abnormal actions. Similarly, to represent fail-stop and
repair faults that affects a process j, we may introduce an auxiliary boolean variable down:j that is
true iff j has fail-stopped. All actions of j are restricted to be executed only when down:j is false.
When a fail-stop fault occurs, down:j is truthified, thus preventing j from executing its actions.
When a repair occurs, down:j is falsified.
We have assumed that problem specifications are suffix closed and fusion closed. Where are these
assumptions exploited in the design method? Do these assumptions restrict the applicability of the
method?
We have used these assumptions in three places: (1) Suffix closure of problem specifications implies
the existence of invariant state predicates. (2) Fusion closure of problem specifications implies the
existence of correction state predicates. (3) Suffix closure and fusion closure of problem specifications
imply that the corresponding safety specifications are fusion closed, which, in turn, implies the
existence of detection state predicates.
These assumptions are not restrictive in the following sense: Let L be a set of state sequences that
is not suffix closed and/or not fusion closed and let p be a program. Then, it can be shown that
by adding history variables to the variables of p, there exists a problem specification L 0 such that
the following condition holds: all computations of p that start at states where some "initial" state
predicate is true are in L iff p satisfies L 0 for some state predicate. Thus, the language of problem
specifications is not restrictive.
How would our method of considering the fault-classes one-at-a-time compare with a method that
considers them altogether?
There is a sense in which the one-at-a-time and the altogether methods are equivalent: programs
designed by the one method can also be designed by the other method. To justify this informally,
let us consider a program p designed by using the altogether method to tolerate fault-classes F 1,
F 2, . , Fn. Program p can also be designed using the one-at-a-time method as follows: Let p1
be a subprogram of p that tolerates F 1. This is the program designed in the first stage of the
one-at-a-time method. Likewise, let p2 be a subprogram of p that tolerates F1 and F 2. This is the
program designed in the second stage of the one-at-a-time method. And so on, until p is designed.
To complete the argument of equivalence, it remains to observe that a program designed by the
one-at-a-time n-stage method can trivially be designed by the altogether method.
In terms of software engineering practice, however, the two methods would exhibit differences.
Towards identifying these differences, we address three issues: (i) the structure of the programs
designed using the two methods, (ii) the complexity of using them, and (iii) the complexity of the
programs designed using them.
On the first issue, the stepwise method may yield programs that are better structured. This is
exemplified by our hierarchical token ring program which consists of three layers: the basic program
that transmits the token, a corrector for the case when at least one process is not corrupted, and a
corrector for the case when all processes are corrupted
On the second issue, since we consider one fault-class at a time, the complexity of each step is less
than the complexity of the altogether program. For example, in the token ring program, we first
handled the case where the state of some process is not corrupted. Then, we handled the only case
where the state of all processes is corrupted. Thus, each step was simpler than the case where we
would need to consider both these cases simultaneously.
On the third issue, it is possible that considering all fault-classes at a time may yield a program
whose complexity is (in some sense) optimal with respect to each fault-class, whereas the one-at-
a-time approach may yield a program that is optimal for some, but not all, fault-classes. This
suggests two considerations for the use of our method. One, the order in which the fault-classes
are considered should be chosen with care. (Again, in principle, programs designed with one order
can be designed by any other order. But, in practice, different orders may yield different programs,
and the complexity of these programs may be different.) And, two, in choosing how to design the
tolerance for a particular fault-class, a "lookahead" may be warranted into the impact of this design
choice on the design of the tolerances to the remaining fault-classes.
How does our compositional method affect the trade-offs between dependability properties?
Our method makes it possible to reason about the trade-offs locally, i.e., focusing attention only
on the components corresponding to those dependability properties, as opposed to globally, i.e., by
considering the entire program. Thus, our method facilitates reasoning about trade-offs between
dependability properties.
moreover, as can be expected, if the desired dependability properties are impossibility to cosatisfy,
it will follow that there do not exist components that can be added to the program while complying
with the interference-freedom requirements of our method.
How does our compositional design method compare with the existing methods for designing fault-tolerant
programs?
Our compositional design method is rich in the sense that it subsumes various existing fault-tolerance
design methods such as replication, checkpointing and recovery, Schneider's state machine approach,
exception handling, and Randell's recovery blocks. (The interested reader is referred to [20, 24] for
a detailed discussion of how properties such as replication, agreement, and order are designed by
interference-free composition within our method.)
How are fault-classes derived? Can our method be used if it is difficult to characterize the faults the
system is subject to?
Derivation of fault-classes is application specific. It begins with the identification of the faults that
the program may be subject to. Each of these faults is then formally characterized using state
perturbations. (As mentioned above, auxiliary variables may be introduced in this formalization.)
The desired type of tolerance for each fault is then specified. Finally, the faults are grouped into
(possibly overlapping) fault-classes, based on the characteristics of the faults or their corresponding
types of tolerance.
If it is difficult to characterize the faults in an application, a user of our method is obliged to guess
some large enough fault-class that would accommodate all possible faults. It is often for this reason
that designers choose weak models such as self-stabilization (where the state may be perturbed
arbitrarily) or Byzantine failure (where the program may behave arbitrarily).
9 Concluding Remarks and Future Work
In this paper, we formalized the notion of multitolerance to abstract a variety of problems in de-
pendability. It is worthwhile to point out that multitolerance has other related applications as well.
One is to reason about graceful degradation with respect to progressively increasing fault-classes.
Another is to guarantee different qualities of service (QoS) with respect to different user requirements
and traffics. A third one is to reason about adaptivity of systems with respect to different
modes of environment behavior.
We also presented a simple, compositional method for designing multitolerant programs, that added
detector and corrector components for providing each desired type of tolerance. The addition of
multiple components to an intolerant program was made tractable by adding tolerances to fault-
classes one at a time. To avoid re-proving the correctness of the program in every step, we provided
a theory for ensuring mutual interference-freedom in compositions of detectors and correctors with
the intolerant program.
To our knowledge, this is the first formal method for the design of multitolerant programs. Our
method is effective for the design of quantitative as well as qualitative tolerances. As an example
of quantitative tolerance, we presented a token ring protocol that recovers from upto K faults in
time. For examples of qualitative tolerances, we refer the interested reader to our designs of
multitolerant programs for barrier computations, repetitive Byzantine agreement, mutual exclusion,
tree maintenance, leader election, bounded-space distributed reset, and termination detection [23,
To apply our design method in practice, we are currently developing SIEFAST, a simulation and
implementation environment that enables stepwise implementation and validation of multitolerant
distributed programs. We are also studying the mechanical synthesis of multitolerant concurrent
programs.

Acknowledgments

. We are indebted to the anonymous referees for their detailed and constructive
comments on earlier versions of this paper, which significantly improved the presentation. Thanks
also to Laurie Dillon for all her help during the review process.



--R

Reliable Computer Systems: Design and Evaluation.
The AT&T Case
The Galileo Case

A foundation of fault-tolerant computing
Superstabilzing protocols for dynamic distributed systems.
Maximal flow routing.
A highly safe self-stabilizing mutual exclusion algorithm
Defining liveness.
Closure and convergence: A foundation of fault-tolerant computing
A Discipline of Programming.
The Science of Programming.
Proving boolean combinations of deterministic properties.
Parallel Program Design: A Foundation.
The existence of refinement mappings.
A proof technique for communicating sequential processes.
Stepwise refinement of parallel programs.
Proofs of networks of processes.
An axiomatic proof technique for parallel programs.
Designing masking fault-tolerance via nonmasking fault-tolerance
Critical system properties: Survey and taxonomy.
Specifying graceful degradation.
Multitolerance in distributed reset.
Multitolerance and its design.
Constraint satisfaction as a basis for designing nonmasking fault-tolerance
Multitolerant barrier synchronization.
Compositional design of multitolerant repetitive byzantine agreement.
--TR

--CTR
Anil Hanumantharaya , Purnendu Sinha , Anjali Agarwal, A component-based design and compositional verification of a fault-tolerant multimedia communication protocol, Real-Time Imaging, v.9 n.6, p.401-422, December
Orna Raz , Mary Shaw, An Approach to Preserving Sufficient Correctness in Open Resource Coalitions, Proceedings of the 10th International Workshop on Software Specification and Design, p.159, November 05-07, 2000
Anish Arora , Sandeep Kulkarni , Murat Demirbas, Resettable vector clocks, Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing, p.269-278, July 16-19, 2000, Portland, Oregon, United States
Anish Arora , Sandeep S. Kulkarni , Murat Demirbas, Resettable vector clocks, Journal of Parallel and Distributed Computing, v.66 n.2, p.221-237, February 2006
Paul C. Attie , Anish Arora , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.1, p.125-185, January 2004
Robyn R. Lutz, Software engineering for safety: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.213-226, June 04-11, 2000, Limerick, Ireland
Anish Arora , Marvin Theimer, On modeling and tolerating incorrect software, Journal of High Speed Networks, v.14 n.2, p.109-134, April 2005
I-Ling Yen , Farokh B. Bastani , David J. Taylor, Design of Multi-Invariant Data Structures for Robust Shared Accesses in Multiprocessor Systems, IEEE Transactions on Software Engineering, v.27 n.3, p.193-207, March 2001
Anish Arora , Paul C. Attie , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, p.173-182, June 28-July 02, 1998, Puerto Vallarta, Mexico
Axel van Lamsweerde , Emmanuel Letier, Handling Obstacles in Goal-Oriented Requirements Engineering, IEEE Transactions on Software Engineering, v.26 n.10, p.978-1005, October 2000
Vina Ermagan , Jun-ichi Mizutani , Kentaro Oguchi , David Weir, Towards Model-Based Failure-Management for Automotive Software, Proceedings of the 4th International Workshop on Software Engineering for Automotive Systems, p.8, May 20-26, 2007
Felix C. Grtner, Fundamentals of fault-tolerant distributed computing in asynchronous environments, ACM Computing Surveys (CSUR), v.31 n.1, p.1-26, March 1999
Anish Arora , Sandeep S. Kulkarni, Designing Masking Fault-Tolerance via Nonmasking Fault-Tolerance, IEEE Transactions on Software Engineering, v.24 n.6, p.435-450, June 1998
formal methods;stepwise design;correctors;graceful degradation;dependability;compositional design;fault-tolerance;detectors;interference-freedom