% The Chicago Journal of Theoretical Computer Science, Volume 1998, Article 4
% Published by MIT Press, Cambridge, Massachusetts USA
% Copyright 1998 by Massachusetts Institute of Technology
%
\newtoks\rstyle
\rstyle={cjlook}
%
\documentclass[v1.1,published]{cjstruct}
%
% Local style resources for this article.
%
\usestyleresource{amstext}
\usepackage{xspace}
\usepackage{eepic}
\usepackage{epic}
%
% Local macro definitions for this article.
%
\catcode`\@=11
\ifx\nopagebreakbeginpar\undeftex
\newcommand{\nopagebreakbeginpar}{\@beginparpenalty10000}
\fi
\ifx\nopagebreakendpar\undeftex
\newcommand{\nopagebreakendpar}{\@endparpenalty10000}
\fi
\ifx\nopagebreakinteritem\undeftex
\newcommand{\nopagebreakinteritem}{\@itempenalty10000}
\fi
\catcode`\@=12
%
\newcommand{\prooffontshape}{\fontshape{n}\selectfont}
%
\newcommand{\setof}[2]{\left\{\,#1:#2\,\right\}}
\tolerance=9000
\newcommand{\plusthree}{\ensuremath{+}\xspace}
\newcommand{\minusthree}{\ensuremath{-}\xspace}
\newcommand{\ad}{\wedge}
\newcommand{\union}{\cup}
\newcommand{\pindent}{\hspace*{20pt}}
% \setcounter{lemma}{0}
\newcommand{\prgmark}{\rule{\textwidth}{1pt}}
\def\sqr{{\vcenter{\vbox{\hrule height.4pt
\hbox{\vrule width.4pt height5pt \kern5pt
\vrule width.4pt} \hrule height.4pt}}}}
\renewcommand{\comment}[1]{\mbox{\{#1\}}}
\newcommand{\assigned}{\mathrel{:=}}
\def\registered{\({}^{\ooalign%
{\hfil\raise.07ex\hbox{{\tiny\textup{R}}}%
\hfil\crcr\scriptsize\mathhexbox20D\cr}}\)}
%
% end of local macro definitions for this article
%
\begin{document}
%
\begin{articleinfo}
%
\publisher{The MIT Press}
%
\publishercomment{%
{\Large
\begin{center}
Volume 1998, Article 4\\
\textit{7 December 1998}
\end{center}
}
\par\noindent
ISSN 1073--0486\@. MIT Press Journals, Five Cambridge Center, Cambridge, MA
02142-1493 USA; (617)253-2889;
\emph{journals-orders@mit.edu, journals-info@mit.edu}\@.
Published one article at a time in \LaTeX\ source form on the
Internet\@. Pagination varies from copy to copy\@. For more
information and other articles see:
\begin{itemize}
\item \emph{http://mitpress.mit.edu/CJTCS/}
\item \emph{http://www.cs.uchicago.edu/publications/cjtcs/}
\item \emph{ftp://mitpress.mit.edu/pub/CJTCS}
\item \emph{ftp://cs.uchicago.edu/pub/publications/cjtcs}
\end{itemize}
\sentence
\par\noindent
The \emph{Chicago Journal of Theoretical Computer Science} is
abstracted or indexed in \emph{Research Alert,\registered
SciSearch,\registered Current Contents\registered/Engineering
Computing \& Technology}, and \emph{CompuMath Citation Index\@.\registered}
}
%
\copyrightstmt{%
\copyright 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;
\emph{journals-rights@mit.edu}\@.\pagebreak[2]
}
%
\journal{Chicago\nolinebreak[1] Journal of Theoretical Computer\nolinebreak[1] Science}
\journalcomment{%
The \emph{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\@.
\par
\begin{trivlist}
\item[\emph{Editor in chief:}] Janos Simon
\item[\emph{Consulting editors:}]
Joseph Halpern, Stuart A.\ Kurtz, Raimund Seidel
\item[\emph{Editors:}]
\begin{tabular}[t]{lll}
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\'o 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
\end{tabular}
\vspace{1ex}
\item[\emph{Managing editor:}] Michael J.\ O'Donnell
\vspace{1ex}
\item[\emph{Electronic mail:}] \emph{chicago-journal@cs.uchicago.edu}
\end{trivlist}
\sentence
}
%
\bannerfile{cjtcs-banner.tex}
%
\volume{1998}
%
\articleid{4}
%
\selfcitation{
@article{cj98-04,
author={S. Kulkarni and A. Arora},
title={Multitolerance in Distributed Reset},
journal={Chicago Journal of Theoretical Computer Science},
volume={1998},
number={4},
publisher={MIT Press},
month={December},
year={1998}
}
}
%
\begin{retrievalinfo}
\end{retrievalinfo}
%
\title{Multitolerance in Distributed Reset}
\shorttitle{Multitolerance}
% \editorname{?}
% \editorcomment{%
% }
\begin{authorinfo}
%
% Correction to error in cjstruct.sty version 1.1.
%
\def\fixversion{1.1}
\ifx\cjversion\fixversion
\renewcommand{\printname}[1]{
\global\authorstring={#1}
\global\authorstrue
\ifinfo\item Printed name: #1\fi
}
\fi
%
% End of correction.
\printname{Sandeep S. Kulkarni}
\collname{}{Kulkarni, Sandeep S.}
\begin{institutioninfo}
\instname{The Ohio State University}
\department{Department of Computer and Information Science}
\address{}{Columbus}{Ohio}{43210}{USA}
\end{institutioninfo}
\email{kulkarni@cis.ohio-state.edu}
\end{authorinfo}
\begin{authorinfo}
\printname{Anish Arora}
\collname{}{Arora, Anish}
\begin{institutioninfo}
\instname{The Ohio State University}
\department{Department of Computer and Information Science}
\address{}{Columbus}{Ohio}{43210}{USA}
\end{institutioninfo}
\email{anish@cis.ohio-state.edu}
\end{authorinfo}
%
\shortauthors{Kulkarni and Arora}
%
\support{
Research supported in part by NSF grant CCR-93-08640 and OSU grant 221506\@.
}
%
\begin{editinfo}
\published{7}{12}{1998}
\end{editinfo}
%
\end{articleinfo}
%
\begin{articletext}
\begin{abstract}
%
\noindent
A reset of a distributed system is safe if it does not complete
``prematurely,'' i.e., without having reset some process in the
system\@. Safe resets are possible in the presence of certain faults,
such as process fail-stops 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\@.
%
\end{abstract}
\asection{1}{Introduction} \label{sec:introduction}
%
\apar{1-1}
A principal requirement of modern distributed systems, such as the
evolving national and global information infrastructures, is
robustness\@. \emph{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\@.
%
\apar{1-2}
In systems that are subject to multiple fault classes, designing the
same 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''
\cite{cj98-04-01}, that is, tolerant to each of a number of
fault classes, in a manner that is best suited to each fault class\@.
%
\apar{1-3}
In this paper, we present a bounded-memory multitolerant, distributed
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 \cite{cj98-04-02}, 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\@.
%
%
\apar{1-4}
Below, we first define the reset problem and what it means for a reset
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\@.
%
\apar{1-5}
\textbf{Distributed Reset.}
A distributed-reset program consists of two modules 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:
%
\begin{itemize}
\item
every reset operation is \emph{nonpremature}, i.e., if the reset
operation completes, the program state is reachable from the given
global state; and
\item
every reset operation \emph{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\@.
\end{itemize}
%
\apar{1-6}
The definition captures the intuition that resetting the distributed
program 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\@.
%
\apar{1-7}
Observe that to reset the program state to the given global state, the
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 \emph{and} all
processes have been reset in a reset operation, then the current
program state is reachable from the corresponding global state.
%
\apar{1-8}
\textbf{Masking Tolerance.}
The ideal fault tolerance for distributed reset is 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\@.
%
\apar{1-9}
Consider a fault that fail-stops a process and repairs it
instantaneously\@. 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 \emph{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\@.
%
\apar{1-10}
\textbf{Stabilizing Tolerance.}
An alternative fault tolerance for distributed 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\@.
%
\apar{1-11}
Stabilizing tolerance is ideal when an arbitrary state may be
reached in 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
\cite{cj98-04-03}\@. In such cases, masking tolerance cannot be designed,
because the fault itself may perturb the program to a state where the
reset operation has completed prematurely\@.
%
\apar{1-12}
Since arbitrary states can be reached in the presence of arbitrary
transient 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\@.
%
\apar{1-13}
\textbf{Multitolerant Reset.}
As motivated above, the best-suited tolerance 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\@.)
%
\apar{1-14}
It is important to emphasize that our reset program is not just a
stabilizing 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\@.
%
\apar{1-15}
In principle, to design a multitolerant reset program, the initiator
of the 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\@.
%
\apar{1-16}
Also, adding such a multitolerant detector to a stabilizing reset
program 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\@.
%
\apar{1-17}
Both these problems are further complicated if the program uses
bounded memory\@. In the masking reset, when the initiator completes
the reset operation, 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\@.
%
\apar{1-18}
(Notice that sequence numbers for old reset operations may exist
in the 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\@.)
%
\apar{1-19}
The complication due to bounded memory is more severe in designing
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\@.
%
\apar{1-20}
As discussed in Section 8, our bounded-memory
multitolerant solution for distributed reset is also useful in
designing a bounded-memory multitolerant solution for any total
program \cite{cj98-04-04}, 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\@.
%
\apar{1-21}
\textbf{Related Work.}
To our knowledge, this is the first bounded-memory multitolerant
distributed-reset program\@. In fact, we are not aware of a bounded-memory
distributed-reset program that is masking tolerant to fail-stops and
repairs\@. We note that Afek and Gafni \cite{cj98-04-05} 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\@.
%
\apar{1-22}
While little work has been done on bounded-memory masking tolerant
resets, bounded-memory stabilizing tolerant resets have received more
attention \cite{cj98-04-02,cj98-04-06,cj98-04-07,cj98-04-08,cj98-04-09,
cj98-04-10,cj98-04-11}\@. All of these programs
are stabilizing tolerant to fail-stops and repairs, but they are not
masking tolerant to them\@. Specifically, in the presence of fail-stops
and repairs, they allow premature completion of distributed resets\@.
%
\apar{1-23}
Masuzawa has presented a reset program \cite{cj98-04-12} that tolerates two
fault 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\@.
%
\apar{1-24}
\textbf{Outline of the Paper.}
In light of the above discussion, we design a distributed 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 \cite{cj98-04-01} for the foundations
of this stepwise design of multitolerance\@.)
%
\apar{1-25}
The rest of the paper is organized as follows: in Section
2, we define 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\@.
\asection{2}{Preliminaries} \label{sec:notations}
%
\apar{2-1}
In this section, we first recall a formal definition of programs, faults,
and fault tolerances \cite{cj98-04-13}\@. We then state our assumptions about the
distributed systems considered in this paper\@.
%
\apar{2-2}
\textbf{Programs.}
A \emph{program} is a set of variables and a finite set of actions\@. Each variable has
a predefined domain\@. Each action is uniquely identified by a name, and is of
the form:
%
\[
\langle \mathrm{name} \rangle:: \langle \mathrm{guard} \rangle \longrightarrow
\langle \mathrm{statement} \rangle
\]
%
\apar{2-3}
The \emph{guard} of an action is a boolean expression over the program variables\@. The
\emph{statement} of an action updates zero or more program variables\@. An action can
be executed only if its guard evaluates to \emph{true}\@. To execute an action, the
statement of that action is executed atomically\@.
%
\apar{2-4}
\textit{State and State Predicate.}
A state of program \(p\) is defined by a value 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 \emph{true} in that state\@.
\apar{2-5}
\textit{Closure.}
Let \(S\) be a state predicate of \(p\)\@. An action of \(p\) preserves \(S\)
if 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\)\@.
%
\apar{2-6}
\textbf{Computation.}
A computation of \(p\) is a fair, maximal sequence of steps; 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 \emph{false} in the final
state\@.
%
\apar{2-7}
\textit{The Invariant Predicate.}
One state predicate of \(p\) is distinguished as 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 \)\@.
%
\apar{2-8}
We assume that in all computations of \(p\) that start from a state
where the invariant holds, the invariant predicate holds throughout\@.
In other words, the 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 \emph{true} at states where the invariant holds; the state
predicate \emph{false} provides a trivial example of such a predicate\@.
%
\apar{2-9}
Techniques for the design of the invariant predicate have been
articulated by Dijkstra \cite{cj98-04-14}, using the notion of
auxiliary variables, and by Gries \cite{cj98-04-15}, 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 \cite{cj98-04-16}\@.
%
\apar{2-10}
\textit{Convergence.}
A state predicate \(Q\) converges to a state predicate \(R\)
in \(p\) 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\@.
%
\apar{2-11}
\textbf{Faults.}
The faults that a program is subject to are systematically represented
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\@.
%
\apar{2-12}
\textit{The Fault Span.}
The fault span of \(p\), with respect to a set of fault actions \(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\)\@.
%
\apar{2-13}
\textbf{Fault Tolerances.}
Let \(p\) be a program with the invariant \(S\), and let \(F\) be 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:
\begin{itemize}
\item inclusion: \(T \! \Leftarrow \! S\),
\item closure: \(T\) is closed in \ \(F\), and
\item convergence: \ \(T\) converges to \(S\) in \(p\).
\end{itemize}
%
\apar{2-14}
This definition may be understood as follows\@. At any state where the
invariant \(S \) holds, executing an action in \(p\) yields a state where
\(S\) continues 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\@.
%
\apar{2-15}
In the context of multitolerance, it is important to note that there
may 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\@.
%
\apar{2-16}
When the invariant \(S\) is clear from the context, we omit \(S\)\@. Thus,
the statement ``\(p\) is \(F\)-tolerant'' abbreviates ``\(p\) is
\(F\)-tolerant for the invariant of \(p\).''
%
\apar{2-17}
\textbf{Types of Fault Tolerances.}
The definition of fault tolerance lets us formally distinguish various
types of fault tolerances, such as \emph{masking}, \emph{nonmasking}, and
\emph{stabilizing}:
%
\begin{enumerate}
\item 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\)\@.
\item 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\@.
\item When the definition is instantiated so that \(T\) is identical to \emph{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\@.
\end{enumerate}
%
\apar{2-18}
\textbf{Multitolerance.}
Let \(p\) be a program with invariant \(S\)\@. Let \(F1, F2,...,Fn\) be \(n\)
fault classes\@. We say that \(p\) is multitolerant to \(F1, F2,...,Fn\)
if and only if for each fault class \(Fj\), \(p\) is \(Fj\)-tolerant for \(S\)\@.
%
\apar{2-19}
Informally, the definition can be understood as follows: in the presence
of faults in \(Fj\), the program is perturbed to a state where the
fault span \(Tj\) holds\@. After faults in \(Fj\) stop occurring, \(p\)
recovers to a state where \(S\) is (re)satisfied\@. It is important to
note that \(Tj\) may be different for each fault class \(Fj\),
and for each \(Fj\), the tolerance of \(p\) to \(Fj\) may also be different\@.
%
\apar{2-20}
This definition of multitolerance captures that the effect of
different fault 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, \emph{true}, may allow a reset to complete prematurely\@.
%
\apar{2-21}
\textbf{System Assumptions.}
A distributed system consists of processes, each with a unique integer
identifier, and bidirectional channels, each connecting a unique pair of
processes\@. At any time, a process is either \emph{up} or \emph{down}\@.
Only up processes execute their actions\@.
%
\apar{2-22}
As mentioned previously, system execution may be affected by faults.
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\@.
%
\begin{alabsubtext}{Remark}{1}{}
\rm
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\@.''
\end{alabsubtext}
\asection{3}{Outline of the Solution} \label{sec:outline}
%
\apar{3-1}
Recall that in accordance with our approach to designing
multitolerance we 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 fail-stops and repairs is preserved\@. In this
section, we outline the structure of each of these three
programs and their proofs of correctness\@.
%
\apar{3-2}
\textit{The Fault-Intolerant Program.}
We use a variation of the diffusing computation 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 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\@.
%
\apar{3-3}
\textit{Adding Masking Tolerance.}
In the presence of fail-stops and repairs, the tree may become
partitioned\@. Hence, the diffusing computation initiated
by a root process may not reach all processes in the system\@.
%
\apar{3-4}
To add masking tolerance, it suffices that we ensure the following
two conditions for every distributed reset:
\begin{enumerate}
\item eventually, the local states of all processes are reset, and
\item in the interim, no diffusing computation completes incorrectly\@.
\end{enumerate}
%
\apar{3-5}
To achieve condition 1, we ensure that eventually the tree spanning all 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 \cite{cj98-04-17} 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\@.
%
\apar{3-6}
To achieve condition 2, we ensure that when the root process completes a
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 \emph{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 \emph{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 \emph{false}, then the parent of \(j\)
completes that diffusing computation with the result \emph{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 \emph{false}\@. It follows that when the root
completes the diffusing computation with the result \emph{true}, all
processes have participated in the diffusing computation\@.
%
\apar{3-7}
Finally, if a root completes a diffusing computation with the result
\emph{false}, 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\@.
%
\apar{3-8}
(We reemphasize that the challenging part of this solution is how \(j\)
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\@.)
%
\apar{3-9}
\textit{Adding Stabilizing Tolerance.}
To design stabilizing tolerance into the 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\@.
%
\asubsection{3.1}{Outline of the Proof} \label{sec:outproof}
%
\apar{3.1-1}
In accordance with the formal definition of a fault-tolerant program
given in Section 2, the proof of correctness of all
programs in this paper is given in terms of their invariant and
fault-span predicates\@.
%
\apar{3.1-2}
For the fault-intolerant program \(R\), we exhibit an invariant \(S_R \)\@.
In other 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\@.
%
\apar{3.1-3}
In the presence of fail-stops and repairs, program \(R\) may be
perturbed to 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 fail-stops 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 \textit{MR}\@. Thus, for \textit{MR},
the invariant is \(S_{MR}\), \(S_{MR} = T_R\;\ad\;D\)\@.
By definition, the fault span of \textit{MR} is identical to
\(S_{MR}\)\@. In other words, we show that if an action of \textit{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\@.
%
\apar{3.1-4}
In the presence of transient faults, program \textit{MR} may be perturbed to
an arbitrary state\@. Hence, the fault span of our stabilizing-tolerant
program, \textit{MSR}, is the predicate \emph{true}\@. The invariant of the
stabilizing-tolerant program is the same as that of the program \textit{MR},
i.e., \(S_{MR}\)\@. As mentioned above, to add stabilizing tolerance to
transient faults, we add convergence actions to program \textit{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 \textit{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 \textit{MR} are
executed\@. It follows that eventually a root process will declare that
the reset is complete\@.
%
\begin{figure*}[htbp]
\setlength{\unitlength}{0.00083333in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
\reset@font\fontsize{#1}{#2pt}%
\fontfamily{#3}\fontseries{#4}\fontshape{#5}%
\selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(6350,3864)(0,-10)
\put(1917,117){\arc{210}{1.5708}{3.1416}}
\put(1917,1032){\arc{210}{3.1416}{4.7124}}
\put(5832,1032){\arc{210}{4.7124}{6.2832}}
\put(5832,117){\arc{210}{0}{1.5708}}
\path(1812,117)(1812,1032)
\path(1917,1137)(5832,1137)
\path(5937,1032)(5937,117)
\path(5832,12)(1917,12)
\put(1167,117){\arc{210}{1.5708}{3.1416}}
\put(1167,2232){\arc{210}{3.1416}{4.7124}}
\put(5832,2232){\arc{210}{4.7124}{6.2832}}
\put(5832,117){\arc{210}{0}{1.5708}}
\path(1062,117)(1062,2232)
\path(1167,2337)(5832,2337)
\path(5937,2232)(5937,117)
\path(5832,12)(1167,12)
\put(162,3462){\makebox(0,0)[lb]{\smash{{{\SetFigFont{14}{16.8}{\rmdefault}{\bfdefault}{\updefault}Stabilizing and Masking Program MSR}}}}}
\put(1287,1962){\makebox(0,0)[lb]{\smash{{{\SetFigFont{14}{16.8}{\rmdefault}{\bfdefault}{\updefault}Masking Program MR}}}}}
\put(2037,732){\makebox(0,0)[lb]{\smash{{{\SetFigFont{14}{16.8}{\rmdefault}{\bfdefault}{\updefault}Fault-Intolerant Program R}}}}}
\put(117,117){\arc{210}{1.5708}{3.1416}}
\put(117,3732){\arc{210}{3.1416}{4.7124}}
\put(5832,3732){\arc{210}{4.7124}{6.2832}}
\put(5832,117){\arc{210}{0}{1.5708}}
\path(12,117)(12,3732)
\path(117,3837)(5832,3837)
\path(5937,3732)(5937,117)
\path(5832,12)(117,12)
\put(387,3192){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Stabilizing tolerant to transient faults (fault span = true)}}}}}
\put(387,2922){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Masking tolerant to fail-stops and repairs (fault span = \(S_{MSR}\))}}}}}
\put(887,2652){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Invariant = \(S_{MSR}\)}}}}}
\put(1512,1692){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Masking tolerant to fail-stop and repair (fault span = \(S_{MR}\))}}}}}
\put(2112,1422){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Invariant = \(S_{MR}\)}}}}}
\put(2537,462){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Invariant = \(S_R\)}}}}}
\end{picture}
}
\afigcap{1}{Structure of the program and its proof} \label{fig:struct}
\end{figure*}
%
\asection{4}{Fault-Intolerant Distributed Reset} \label{sec:intolerant}
%
\apar{4-1}
In this section, we describe a straightforward distributed-reset
program in 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\@.
%
\apar{4-2}
When the root process initiates a distributed reset, it marks its
state as \emph{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 \emph{reset}, resets its
local state, and propagates the reset wave to its children\@. We refer to
these propagations as \emph{the propagation of the reset wave}\@.
%
\apar{4-3}
When a leaf process \(j\) propagates a reset wave, \(j\) completes the reset wave,
marks its state as \emph{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 \emph{the completion of the reset wave}\@.
%
\apar{4-4}
It follows that when a process completes a reset wave, all its descendents
have completed that reset wave\@. In particular, when the root process 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\@.
%
\apar{4-5}
\textbf{Variables.}
As described above, every process \(j\) maintains the following variables:
%
\begin{itemize}
\item \(st.j\), the state of \(j\): the state is \emph{reset} if \(j\) is
propagating a reset wave; otherwise, it is \emph{normal};
\item \(sn.j\), the sequence number of \(j\): the sequence number of \(j\) is either
0 or 1; and
\item \(par.j\), the parent of \(j\): the parent of the root process is set to
itself.
\end{itemize}
%
\apar{4-6}
\textbf{Actions.}
As described above, program \(R\) consists of three actions at each process \(j\)\@.
Action \textit{R1} lets \(j\) initiate a new reset wave if \(j\) is a root process\@.
Action \textit{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 \textit{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\@.
%
\apar{4-7}
Formally, the actions of the program at process \(j\) are shown in Figure~2 (let
\(ch.j\) denote the set of children of \(j\)):
%
\begin{tabbing}
\\
\prgmark\\
\= \(\textit{R1} ::\) \= \(\longrightarrow\) \= \(par.j\!=\!j\;\;\ad\;\;st.j\!=\!normal\ \;\ad\;\;\) \{\(j\) needs to initiate a new reset wave\} \kill
\> \(\textit{R1} ::\) \> \> \(par.j = j \ad st.j = \textit{normal} \; \ad\) \comment{\(j\) needs to initiate a new reset wave}\\
\> \> \(\longrightarrow\) \> \(st.j,\;sn.j := \textit{reset},\;sn.j\! \oplus \!1;\;\;\) \comment{reset local state of \(j\)}\\
\ \\
\>\textit{R2} \(::\)\> \> \(st(par.j)\!=\!\textit{reset}\;\;\ad\;\;sn.j\!\not=\!sn.(par.j)\) \\
\> \> \(\longrightarrow\) \> \(st.j,\;sn.j:=\textit{reset},\;sn.(par.j);\;\;\) \comment{reset local state of \(j\)}\\
\ \\
\>\textit{R3} \(::\)\> \> \(st.j = \textit{reset}\;\ad\;(\forall k : k\!\in\!ch.j : sn.j\!=\!sn.k\;\ad\;st.k\!\not=\!\textit{reset})\) \\
\> \> \(\longrightarrow\) \> \(st.j:=normal;\;\;\) \comment{\textbf{if} \(par.j\!=\!j\), \textbf{then} declare reset complete}\\
\prgmark\\
\afigcap{2}{Actions of program \(R\) at process \(j\)}
\end{tabbing}
%
\apar{4-8}
\textbf{Invariant.}
Observe that if both \(j\) and \(par.j\) are propagating a reset wave, then they have
the same sequence number\@. Also, if \(par.j\) is in the \emph{normal} state, then \(j\) is
also in the \emph{normal} state and has the same sequence number as \(par.j \)\@. Hence, the
predicate \(GD = (\forall j :: Gd.j)\) is in the invariant of the program, where:
%
{\small
\begin{tabbing}
\(Gd.j\) \= = \=\(((st.(par.j) = \textit{reset} \ad st.j = \textit{reset})\) \= \(\Rightarrow sn.j = sn.(par.j)) \; \ad\)\\
\> \>\(((st.(par.j) \not = \textit{reset})\) \> \(\Rightarrow (st.j \not= \textit{reset} \ad sn.j = sn.(par.j)))\)
\end{tabbing}
}
%
\apar{4-9}
Moreover, the invariant of the program is:
\[
S_R = GD \ad \hbox{graph of the parent relation forms a tree\@.}
\]
\begin{alabsubtext}{Remark}{2}{}
\rm
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 \cite{cj98-04-02}, and is not
discussed in this paper\@.
\end{alabsubtext}
%
\asection{5}{Masking Fault-Tolerant Distributed Reset} \label{sec:maskreset}
%
\apar{5-1}
In this section, we transform the fault-intolerant program of Section
4 to add 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:
%
\begin{itemize}
\item after faults stop occurring, the program eventually reaches a state
from where no distributed reset ever completes incorrectly; and
\item when a root process declares that a distributed reset has
completed, all up processes have participated in that reset
wave\@.
\end{itemize}
%
\apar{5-2}
We design the masking-tolerant program in two stages\@. In the first stage, 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 \cite{cj98-04-18} for the foundations of this two-stage method
for adding masking tolerance\@.)
%
\apar{5-3}
In Section 5.1, we design the nonmasking program to
tolerate fail-stop and repair faults\@. Then, in Section 5.2, we
restrict the actions of the nonmasking program, so that the resulting program
is masking-fault tolerant\@.
%
\asubsection{5.1}{Nonmasking Fault-Tolerant Distributed Reset} \label{sec:nonmasking}
%
\apar{5.1-1}
Observe that if the program reaches a state where the invariant \(S_R\)
holds, 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\@.
%
\apar{5.1-2}
To construct a spanning tree, we use Arora's program for tree
maintenance \cite{cj98-04-17}, 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
\cite{cj98-04-17} for the proof of the nonmasking program\@.
%
\apar{5.1-3}
The program merges multiple trees such that no cycles are formed: each
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\@.
%
\apar{5.1-4}
The program has actions to let each process detect if it is in
an unrooted 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, the parent tree is
(re)constructed\@.
%
\apar{5.1-5}
To restore \(Gd.j\) at every process, we proceed as follows. We ensure
that 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\@.
%
\apar{5.1-6}
\textbf{Variables.}
Every process \(j\) maintains the following variables:
%
\begin{itemize}
\item \(col.j\), the color of the process \(j\): the color of \(j\)
is either green or red; and
\item \(root.j\), the root of the process \(j\): the identifier of the process that
\(j\) believes to be the root\@.
\end{itemize}
%
\apar{5.1-7}
\textbf{Actions.}
Program \textit{NR} consists of six actions for each process \(j\)\@. The first
three actions implement the reset wave\@. Action \textit{NR1} is the initiation
action; it is the same as action \textit{R1}\@. Action \textit{NR2} is the
propagation action; it is a restricted version of action \textit{R2}, where
\(j\) executes the action \textit{NR2} only if \(j\) and \(par.j\) are green and in
the same tree\@. Action \textit{NR3} is the completion action; it is a
restricted version of \textit{R3}, where \(j\) executes action \textit{R3} only if
\(col.j\) is green and the \(root\) value of the children of \(j\) is the
same as \(root.j\)\@.
%
\apar{5.1-8}
The remaining three actions maintain a spanning tree\@. Action \textit{NR4}
deals 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 \textit{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 \textit{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\)\@.
%
\apar{5.1-9}
Formally, the actions of program \textit{NR} at process \(j\) are as shown in Figure~3
(let \(Adj.j\) denote the neighbors of \(j\)):
%
\begin{tabbing}
\prgmark \\
\hspace*{0em} \= \(\textit{NR1} ::\) \hspace*{0em} \= \hspace*{2em} \= \(\textit{R1}\)\\
\ \\
\> \textit{NR2} \(::\) \>\> \(root.j\!=\!root.(par.j)\;\ad\;col.(par.j)\!=\!\mathrm{green}\;\ad\)\\
\>\>\> \(st(par.j)\!=\!\textit{reset}\;\ad\;\;sn.j\!\not=\!sn.(par.j)\) \\
%
\>\> \(\longrightarrow\) \> \(st.j,\;sn.j:=\textit{reset},\;sn.(par.j);\;\;\)
\comment{reset local state of \(j\)}\\
\ \\
\>\textit{NR3}\(::\)\>\> \(st.j\!=\!\textit{reset}\;\ad\;col.j\!=\!\mathrm{green}\)\\
\>\>\> \((\forall k : k\!\in\!ch.j :\) \= \(root.j\!=
\!root.k\;\ad\;sn.j\!=\!sn.k\;\ad\;st.k\!\not=\!\textit{reset})\) \\
%
\>\> \(\longrightarrow\) \> \(st.j:=normal;\;\;\) \textbf{if} \(par.j\!=\!j\),
\textbf{then} \comment{declare reset complete}\\
\ \\
\> \textit{NR4} \(::\) \>\> \(col.j \! = \! \mathrm{green} \, \wedge\; (par.j \! \not \in
\! Adj.j \! \cup \! \{j\} \, \vee \, col.(par.j) \! =
\! \mathrm{red})\) \\
\>\> \(\longrightarrow\) \> \(col.j := \mathrm{red}\)\\
\ \\
\> \textit{NR5} \(::\) \>\> \(col.j \! = \! \mathrm{red} \, \ad \; (\forall k: k \! \in \! Adj.j: par.k \! \neq \! j)\) \\
\>\> \(\longrightarrow\) \> \(col.j, \;par.j,\; root.j := \mathrm{green},\; j,\; j\)\\
\ \\
\> \textit{NR6} \(::\) \>\> \(k \! \in \! Adj.j \; \ad \; root.j \! < \! root.k \;
\ad \; col.j \! = \! \mathrm{green} \; \ad \; col.k \! = \! \mathrm{green}\)\\
\>\> \(\longrightarrow\) \> \(par.j, root.j, := k, root.k ;\; st.j, sn.j := st.k, sn.k\) \\
\prgmark \\
\afigcap{3}{Actions of program \(NR\) at process \(j\)}
\end{tabbing}
%
\asubsubsection{5.1.3}{Fault Actions}
The fail-stop and repair actions are shown in Figure~4\@.
%
\begin{tabbing}
\prgmark \\
\hspace*{0em} \= \(fail\)-\(stop ::\) \hspace*{0.75em} \= \(up.j\) \hspace*{2em} \= \(\longrightarrow\) \hspace*{2em} \= \(up.j := false\)\\
\> \(repair ::\) \> \(\neg up.j\) \> \(\longrightarrow\) \> \(up.j, par.j, root.j, col.j := true, j, j, \mathrm{red}\)\\
\prgmark \\
\afigcap{4}{Fail-stop and repair actions of program \(NR\)}
\end{tabbing}
%
\apar{5.1-10}
\textbf{Fault Span and Invariant.}
From Arora's tree-maintenance program, 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_{TREE}\) is in the fault span, where:
%
\begin{tabbing}
\(T_{TREE}\) = {\small the graph of the parent relation is a forest} \(\wedge \;(\forall j : up.j : T1.j)\), {\small where}\\
\hspace*{2em}\= \(T1.j = \) \= \(((col.j\! =\! \mathrm{red} \;\;\Rightarrow \;(par.j \! \not
\in \! Adj.j \! \cup \! \{j\} \;\;\vee\;\; col(par.j)\! =\! \mathrm{red}))\;\ad\)\\
\>\> \((par.j \!=\! j\; \Rightarrow \;root.j\! =\! j)\;\;\; \wedge\;\;\;\)
\((par.j \!\not =\! j \;\Rightarrow \;root.j \!>\! j) \;\; \wedge\) \\
\>\> \((par.j \!\in\! Adj.j \;\;\Rightarrow \;(root.j \!\leq\! root.(par.j) \;\vee
\;col(par.j) \! = \! \mathrm{red}\))))
\end{tabbing}
%
\apar{5.1-11}
Observe that \(Gd.j\) is preserved when \(root.j\) is the same as \(root.(par.j)\), and
\(col.(par.j)\) is green\@. Hence, the predicate \(NGD = (\forall j :: NGd.j)\) is in
the fault span, where:
%
\[
NGd.j \;\;= \;\;(root.j\!=\!root.(par.j)\;\ad\;col.(par.j)\!=\! \mathrm{green} \;\;\;\; \Rightarrow\;\;\;\; Gd.j)
\]
%
Thus, the fault span of the program is:
%
\[T_{NR}\;\; =\;\; T_{TREE}\;\ad\;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}\;\ad\;S_R\;\ad\;(\forall j, k ::
par.j\!\in\!Adj.j\;\ad\;col.j\!=\!\mathrm{green} \;\ad\; root.j\!=\!root.k)
\]
%
\begin{alabsubtext}{Theorem}{1}{}
Program \textit{NR} is nonmasking tolerant to fail-stop and repair faults for
invariant \(S_{NR}\) and fault span \(T_{NR}\)\@.
\end{alabsubtext}
%
\asubsection{5.2}{Enhancing Tolerance to Masking} \label{sec:check}
%
\apar{5.2-1}
Program \textit{NR}, being nonmasking tolerant, allows a reset operation to
complete prematurely\@. To enhance the tolerance of \textit{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 \emph{false},
then the parent of \(j\) completes that reset wave with the result
\emph{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 \emph{false}\@. It follows that when the root
completes the reset wave with the result \emph{true}, all processes have
participated in the reset wave\@.
%
\apar{5.2-2}
It remains to specify how a process detects whether its neighbors have
propagated the current wave\@. One possibility is for \(j\) to detect
whether the 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\@.
%
\apar{5.2-3}
Let the initial state be as shown in Figure~5a\@. Process \(k\) is the
root, 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:
%
\begin{figure}[htp]
\vspace*{120ex}
\special{psfile=cj9804f5.eps hoffset=0 voffset=100}
\afigcap{5}{Detecting whether a neighbor is reset in the current reset operation}
\label{fig:whyabort2}
\end{figure}
%
\begin{itemize}
\item Process \(n\) fails\@.
\item Process \(k\) completes its reset wave and initiates a new reset
wave with sequence number 1 (Figure~5b)\@.
\item Process \(j\) separates from the tree, changes its parent to
\(k\), and propagates the reset wave with sequence number 1 (Figure~5c)\@.
\item 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\@.
\item 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)\@.
\item 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\@.
\end{itemize}
%
\apar{5.2-4}
From the above computation, we observe that after \(j\) changes its
tree, it cannot safely detect whether \(l\) is in the same wave as \(j\)
during the subsequent two waves\@.
%
\apar{5.2-5}
Fortunately, in the third wave after \(j\) changes its tree, \(j\) can
safely detect whether \(l\) is in the same wave, provided \(j\) and \(l\) do
not change their trees in the interim\@. Returning to our example:
%
\begin{itemize}
\item 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)\@.
\item 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)\@.
\end{itemize}
%
\apar{5.2-6}
Observe that starting from the state in Figure~5h, \(j\) can complete
its reset 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\@.
%
\begin{alabsubtext}{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 \textit{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\)\@.
\end{alabsubtext}
%
\apar{5.2-7}
We use Lemma 1 to specify how \(j\) detects whether its neighbors have
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 \emph{new}
values are zero\@.
%
\apar{5.2-8}
Thus, \emph{new} implements the ``result'' associated with the reset wave\@.
The \emph{new} value being zero is equivalent to the result being \emph{true}, and
the \emph{new} value being nonzero is equivalent to the result being
\emph{false}\@. Therefore, if the \emph{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 \(new.(par.(par.j))\) to
a nonzero value, and so on\@. Thus, when the initiator completes the
reset wave, its \emph{new} value is nonzero, and the initiator concludes
that the reset wave has completed incorrectly\@.
%
\apar{5.2-9}
As mentioned in Section 3, if the initiator detects
that the reset wave has 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 \emph{new} value to 2\@.
%
\apar{5.2-10}
\textbf{Variables.}
As described above, each process \(j\) additionally maintains the variable
\(new.j\), which is either 0, 1, or 2\@.
%
\apar{5.2-11}
\textbf{Actions.}
Program \textit{MR} consists of six actions for each process \(j\)\@. The first
three actions implement the reset wave\@. Action \textit{MR1} is the initiation
action; it is the same as action \textit{NR1}\@. Action \textit{MR2} is the
propagation action; it is the same as action \textit{NR2}\@. Action \textit{MR3} is
the completion action; it is a restricted version of \textit{NR3}, where \(j\)
executes action \textit{NR3} only if the predicate \((\forall l : l \! \in \!
Adj.j : root.j\!=\!root.l\;\ad\;sn.j\!=\!sn.l)\) holds\@. Also, \(j\)
updates the variable \emph{new} as described above\@. If the initiator
completes a reset wave incorrectly, it initiates a new reset wave\@.
Actions \textit{MR4}, \textit{MR5}, and \textit{MR6} maintain a spanning tree\@.
When \(j\) changes its
tree, by executing actions \textit{NR5} and \textit{NR6}, \(j\) sets the \emph{new} value of
\(j\) and the old parent of \(j\) to 2\@.
%
\apar{5.2-12}
Formally, the actions for the process \(j\) are as in Figure~6 (for
simplicity, we let actions \textit{MR3}, \textit{MR5}, and \textit{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\).)
%
\apar{}
{\footnotesize
\begin{tabbing}
\prgmark \\
\= \(\textit{MR1} ::\) \hspace*{0.75em} \= \(\textit{NR1}\)\\
\ \\
\> \(\textit{MR2} ::\) \hspace*{0.75em} \> \textit{NR2}\\
\ \\
\> \(\textit{MR3} ::\) \> \(st.j = \textit{reset} \ad col.j = \mathrm{green} \ad\) \hspace*{0.5em} \= \= \(\longrightarrow\) \= \(st.j := normal;\)\\
\>\> \((\forall l : l \in Adj.j :\) \= \(root.l = root.j \ad\)
\>\> \bfseries{if} (\(\exists l : l \!\in\!Adj.j \! \union \! \{ j \} : new.l\!>\!0\)), \bfseries{then}\\
\>\>\> \(sn.j\!=\!sn.l)\;\;\ad\;\)
\>\> \hspace*{1em} \= \bfseries{if} \((par.j\!=\!j)\), \bfseries{then}\\
\>\> \((\forall l : l \! \in \! ch.j : st.l \! \not = \! \textit{reset})\)
\>\>\>\> \hspace*{1em} \= \(st.j,\;sn.j := \textit{reset}, sn.j\! \oplus\!1\);\\
\>\>\>\>\>\>\> \{reset local state of \(j\)\}\\
\>\>\>\>\>\> \bfseries{else}\\
\>\>\>\>\>\>\>\(new.(par.j) := max(new.(par.j), 1)\)\\
\>\>\>\>\> \bfseries{else if} \((par.j\!=\!j)\) {\textbf then} \hspace*{0.5em} \textmd{\{declare reset} \\
\>\>\>\>\> \(new.j := max(0, new.j \! - \! 1)\) \hspace*{0.75em} complete\};\\
\> \(\textit{MR4} ::\) \> \(\textit{NR4}\)\\
\ \\
\> \(\textit{MR5} ::\) \> \(col.j \! = \! \mathrm{red} \, \ad\)
\>\> \(\longrightarrow\) \> \(col.j, \;par.j,\; root.j := \mathrm{green},\; j,\; j\);\\
\>\> \((\forall k: k \! \in \! Adj.j: par.k \! \neq \! j)\)
\>\>\> \(new.j, new.(par.j) := 2, 2\)\\
\ \\
\> \(\textit{MR6} ::\) \> \(k \! \in \! Adj.j \;\; \ad \;\; root.j \! < \! root.k\; \ad\)
\>\> \(\longrightarrow\) \> \(par.j, root.j := k, root.k \); \\
\>\> \(col.j \! = \! \mathrm{green}\;\; \ad\;\; col.k \! = \! \mathrm{green}\)
\>\>\> \(st.j, sn.j := st.k, sn.k\); \\
\>\>\>\>\> \(new.j, new.(par.j) := 2, 2\)\\
\prgmark \\
\afigcap{6}{\normalsize Actions of program \(MR\) at process \(j\)}
\end{tabbing}
}
%
\apar{5.2-13}
\textbf{Fault Actions.}
As described above, when a process \(j\) fail-stops, \(par.j\) 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 \emph{new} value to 2\@. When a process \(j\) is repaired, \(j\) sets
\(new.j\) to 2\@. Formally, the actions are described in Figure~7\@.
%
\begin{tabbing}
\prgmark \\
\emph{fail-stop}\(::\)\= \(\;\,\,up.j\;\;\) \= \(\longrightarrow\) \= \(up.j := false\); \((\forall l : l \! \in Adj.j : new.l:=2)\)\\
\emph{repair}\(::\) \> \(\neg up.j\) \> \(\longrightarrow\) \> \(up.j, par.j, root.j, col.j, d.j, new.j := true, j, j, \mathrm{red}, 0, 2\)\\
\prgmark \\
\afigcap{7}{Fail-stop and repair actions of program \(MR\)}
\end{tabbing}
%
\begin{alabsubtext}{Remark}{3}{}
\rm
In the fail-stop action, we have overloaded the operator \(\forall\) 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\@.
\end{alabsubtext}
%
\apar{5.2-14}
\textbf{Invariant.}
While we relegate the detailed invariant (\(S_{MR}\)) of the masking 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:
%
\begin{description}
\item [\(X.j =\)] \(\{ j \}\) \textbf{if} \(par.j\!=\!j\;\vee\; par.j \! \not \in Adj.j\;\vee\; col.j \! = \! \mathrm{red}\;\vee\; root.j \! \not = \!root.(par.j)\)\\
\(\{ j \} \union X.(par.j)\) \textbf{otherwise}
\item[\(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 \textit{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
\item[\(des.j.k =\)] {\(\{ j \}\; \union \;(\bigcup l: l \in pc.j.k : des.l.k)\)}
\item[\(nbrs(des.j.k) =\)] {\(des.j.k \union \{ l : \exists j :: (l \! \in Adj.j \;\ad\;j\!\in des.j.k) \}\)}
\item[\(\mathit{failed.k} =\)] set of processes that repaired after \(k\) started its reset wave
\end{description}
%
\apar{5.2-15}
Intuitively, \(X.j\) is the set of ancestors of \(j\) that have the same
root value 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\)\@.
%
\apar{5.2-16}
When \(j\) completes a reset wave initiated by \(k\), \(j\) detects whether
all of 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 \(\textit{failed.k}\))\@. Thus,
\(nbrs(des.j.k)\) is a subset of (\(des.k.k\! \union \! \textit{failed.k}\))\@.
%
\apar{5.2-17}
Observe that when a process \(j\), such that \(k \! \in \! X.j\),
completes a reset wave, \(j\) detects the predicate \(nbrs(des.j.k)\!
\subseteq \! (des.k.k \! \union \! \textit{failed.k})\) by checking \(new.j\)
and the \emph{new} values of its neighbors\@. If \(j\) cannot conclude that
\(nbrs(des.j.k)\! \subseteq \! (des.k.k \union \textit{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:
%
\begin{tabbing}
\(I1 = \) \=(\=\(k \in X.j \ad new.j = 0 \; \ad \)\\
\> \>\(st.j \not = \textit{reset} \ad\)\\
\> \>\(st.k = \textit{reset} \ad sn.j = sn.k) \Rightarrow\) \=
\(nbrs(des.j.k)\! \subseteq \! (des.k.k \! \union \! \textit{failed.k})\;\vee\)\\
\>\>\> \(new.(par.j) \! > \! 0\;\vee\)\\
\>\>\> \((par.j\!\not = j \; \ad \; st.(par.j) \! \not = \! \textit{reset})\)\\
\end{tabbing}
%
\apar{5.2-18}
Finally, the predicates \(T_{TREE}\) and \(NGD\) are in the invariant\@. \\
%
\begin{alabsubtext}{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)\subseteq
(des.k.k\!\union\!\textit{failed.k})\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Theorem}{2}{}
Program MR is masking tolerant to fail-stop and repair faults for
invariant \(S_{MR}\)\@.
\end{alabsubtext}
%
\asection{6}{Stabilizing- and Masking-Tolerant Distributed Reset} \label{sec:stabmaskreset}
%
\apar{6-1}
In this section, we transform program \textit{MR} to add stabilizing tolerance to
transient faults\@. To this end, we add
convergence actions to program \textit{MR} that restore it from an arbitrary
state to a state where \(S_{MR}\) holds\@.
%
\apar{6-2}
We proceed as follows. Since each state where \(S_{MR}\) holds satisfies
\(T_{TREE}\) and \(NGD\), we add convergence actions to program \textit{MR} that restore
it from an arbitrary state to a state where \(T_{TREE}\;\ad\;NGD\) holds\@.
Further, we show that starting from a state where
\(T_{TREE}\) and \(NGD\) hold, the program converges to a state where \(S_{MR}\)
holds\@.
%
\apar{6-3}
By the definitions of \(T_{TREE}\) and \(NGD\),
\(T_{TREE}\;\ad\;NGD\) may be violated if any of the following three
conditions hold:
%
\begin{enumerate}
\item the graph of the parent relation contains cycles,
\item there exists a process \(j\) such that \(T1.j\) is violated, or
\item there exists a process \(j\) such that \(NGd.j\) is violated.
\end{enumerate}
%
\apar{6-4}
To handle condition 1, each cycle in the graph of the parent relation is 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\!\in\!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\)\@.
%
\apar{6-5}
To handle condition 2, whenever \(T1.j\) is violated, \(j\) corrects \(T1.j\)
by separating from the tree and setting \(par.j\) and \(root.j\) to \(j\)\@.
%
\apar{6-6}
To handle condition 3, whenever \(NGd.j\) is violated, \(j\) corrects \(NGd.j\) by copying
the state and sequence number values from its parent\@.
%
\apar{6-7}
\noindent{\bf Variables.} \
As described above, each process maintains a variable \(d.j\) to denote the
distance of \(j\) from \(root.j\) in the graph of the parent relation\@.
%
\apar{6-8}
\textbf{Actions.}
Program \textit{MSR} consists of nine actions for each process \(j\)\@. Actions
\textit{MSR1}--\textit{MSR6} construct the spanning tree and implement the reset wave; they
are identical to the actions \textit{MR1}--\textit{MR6}\@. Action \textit{MSR7}
corrects \(d.j\)
whenever \(par.j\!\in\!Adj.j\) and \(d.(par.j)\!<\!K\), by setting \(d.j\) to
\(d.(par.j)\!+\!1\)\@. Action \(\textit{MSR8}\) is executed when \(d.j\) exceeds \(K\) or \(T1.j\)
is violated\@. As described earlier, when \(j\) executes \textit{MSR8}, \(j\) sets \(par.j\)
and \(root.j\) to \(j\) and \(d.j\) to zero\@. Since \(j\) changes its tree in action
\textit{MSR8}, \(j\) sets both \(new.j\) and the \(new\) of the old parent of \(j\) to 2\@.
Action \textit{MSR9} is executed when \(j\) violates \(NGd.j\)\@. Additionally, \(j\) corrects \(NGd.j\) by
copying the state and sequence number from its parent\@.
%
\apar{6-9}
Formally, the actions are as shown in Figure~8\@.
\begin{tabbing}
\prgmark \\
\hspace*{0em} \= \(\textit{MSR1} ::\) \hspace*{0em} \= \hspace*{2em} \= \kill
\> \(\textit{MSR1} ::\) \> \(\textit{MR1}\)\\
\hspace*{7.5em}\(\vdots\)\\
\> \(\textit{MSR6} ::\) \> \(\textit{MR6}\)\\
\> \(\textit{MSR7} ::\) \>\>
\(par.j\!\in\!Adj.j\;\ad\;d.j\!\not=\!d.(par.j)+1\;\ad\;d.(par.j)\!\> \(\longrightarrow\) \> \(d.j := d.(par.j)+1\)\\
\ \\
\> \(\textit{MSR8} ::\) \>\> \(d.j\!\geq\!K\;\vee\;\neg T1.j\;\vee\;\) \((par.j\!=\!j\;\ad\;d.j\!\not=\!0)\) \\
\>\> \(\longrightarrow\) \> \(par.j, col.j, root.j, d.j, new.j, new.(par.j) := j, \mathrm{red}, j, 0, 2, 2\)\\
\ \\
\> \(\textit{MSR9} :\) \>\> \(\neg NGd.j\)\\
\>\> \(\longrightarrow\) \> \(st.j, sn.j := st.(par.j),sn.(par.j)\)\\
\prgmark\\
\afigcap{8}{Actions of program \(MSR\) at process \(j\)}
\end{tabbing}
%
\apar{6-10}
\textbf{Invariant.}
The invariant of the stabilizing and masking program \textit{MSR} is:
%
\[S_{MSR} = S_{MR}\]
%
\apar{6-11}
As mentioned in Section 3.2, to preserve the masking tolerance
to fail-stop and repair faults, we prove the following lemma\@.
%
\begin{alabsubtext}{Lemma}{3}{}
Actions \(\textit{MSR7}\)--\(\textit{MSR9}\) preserve \(S_{MR}\),
and do not execute indefinitely after
program \(\textit{MSR}\) reaches a state in \(S_{MR}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Theorem}{3}{}
Program \(\textit{MSR}\) is masking tolerant to fail-stop and repair faults, and is
stabilizing tolerant to transient faults for invariant \(S_{MSR}\)\@.
\end{alabsubtext}
%
\apar{6-12}
\begin{alabsubtext}{Remark}{4}{}
\rm
Since the program \(\textit{MSR}\) is masking tolerant to fail-stop and repair
faults, the fault span in the presence of fail-stop and repair faults,
\(T1\), is identical to the invariant \(S_{MSR}\)\@. Since the \(\textit{MSR}\) is
stabilizing tolerant to transient faults, the fault span in the
presence of transient faults, \(T2\), is \emph{true}\@.
\end{alabsubtext}
%
\begin{figure*}[htbp]
\vspace{100ex}
\setlength{\unitlength}{0.00066666in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
\reset@font\fontsize{#1}{#2pt}%
\fontfamily{#3}\fontseries{#4}\fontshape{#5}%
\selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(0,0)(0,0)
\put(3192,5121){\arc{210}{1.5708}{3.1416}}
\put(3192,5736){\arc{210}{3.1416}{4.7124}}
\put(5607,5736){\arc{210}{4.7124}{6.2832}}
\put(5607,5121){\arc{210}{0}{1.5708}}
\path(3087,5121)(3087,5736)
\path(3192,5841)(5607,5841)
\path(5712,5736)(5712,5121)
\path(5607,5016)(3192,5016)
\put(2292,5121){\arc{210}{1.5708}{3.1416}}
\put(2292,7611){\arc{210}{3.1416}{4.7124}}
\put(5607,7611){\arc{210}{4.7124}{6.2832}}
\put(5607,5121){\arc{210}{0}{1.5708}}
\path(2187,5121)(2187,7611)
\path(2292,7716)(5607,7716)
\path(5712,7611)(5712,5121)
\path(5607,5016)(2292,5016)
\dashline{60.000}(3162,5841)(2187,5841)
\dashline{60.000}(2262,7716)(912,7716)
\put(1017,5121){\arc{210}{1.5708}{3.1416}}
\put(1017,8571){\arc{210}{3.1416}{4.7124}}
\put(5607,8571){\arc{210}{4.7124}{6.2832}}
\put(5607,5121){\arc{210}{0}{1.5708}}
\path(912,5121)(912,8571)
\path(1017,8676)(5607,8676)
\path(5712,8571)(5712,5121)
\path(5607,5016)(1017,5016)
\dashline{60.000}(987,8691)(12,8691)
\put(117,5121){\arc{210}{1.5708}{3.1416}}
\put(117,10296){\arc{210}{3.1416}{4.7124}}
\put(5607,10296){\arc{210}{4.7124}{6.2832}}
\put(5607,5121){\arc{210}{0}{1.5708}}
\path(12,5121)(12,10296)
\path(117,10401)(5607,10401)
\path(5712,10296)(5712,5121)
\path(5607,5016)(117,5016)
\put(1062,9666){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\bfdefault}{\updefault}Stabilizing and Masking Program \(MSR\)}}}}}
\put(1062,9231){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Actions \emph{MSR--9} converge to \(S_\mathrm{MR}\)}}}}}
\put(1887,8166){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\bfdefault}{\updefault}Masking Program \(MR\)}}}}}
\put(1287,7326){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gNR3\)}}}}}
\put(1287,6891){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR3\)}}}}}
\put(1287,6621){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR4\)}}}}}
\put(1287,6351){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR5\)}}}}}
\put(2587,7101){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\bfdefault}{\updefault}Nonmasking Program \emph{NR}}}}}}
\put(2587,6591){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Actions \emph{NR4--6} to maintain tree}}}}}
\put(2487,5166){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gR3\)}}}}}
\put(2487,5451){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gR2\)}}}}}
\put(3100,5466){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Fault-intolerant program, \(R\)}}}}}
\put(3100,5166){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Actions \(R1-3\)}}}}}
%
\put(1537,4191){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\bfdefault}{\updefault}Legend:}}}}}
\put(1837,3741){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}Action \(Yi\) of program \(Y\) is obtained by action \(Xi\) of program \(X\)}}}}}
\put(1837,3471){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}with \(gXi\) added to the guard of \(Xi\) and \(sXi\) added to the statement}}}}}
\put(1837,3201){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}of \(Xi\). Unless explicitly mentioned, \(gXi\) is true and \(sXi\) is skip}}}}}
\put(1837,2451){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gR2 = (root.j = root.(par.j))\) and \(col.(par.j) = \) green}}}}}
\put(1837,2151){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gR3 = \mbox{(forall } k : k \mbox{ in } ch.j : root.j = root.k \mbox{ and } col.j = \) green)}}}}}
\put(1837,1536){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(gNR3 = \mbox{(forall } l : l \mbox{ in } Adj.j : root.j = root.l \mbox{ and } sn.j = sn.l)\)}}}}}
\put(1837,936){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR3 = \mbox{ update } new.j, new.(par.j)\)}}}}}
\put(1837,636){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR4 = new.j, new.(par.j) := 2, 2\)}}}}}
\put(1837,336){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\rmdefault}{\mddefault}{\updefault}\(sNR5 = new.j, new.(par.j) := 2, 2\)}}}}}
\end{picture}
}
\afigcap{9}{Composition of the masking- and stabilizing-reset program (\emph{MSR})} \label{fig:maskstab}
\end{figure*}
%
\asection{7}{Bounding the Sequence Numbers\\ of Multitolerant Applications} \label{sec:impact}
%
\apar{7-1}
In this section, we discuss how applications use the bounded sequence
numbers 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\@.
\asubsection{7.1}{Need for Incarnation Numbers}
%
\apar{7.1-1}
If the sequence numbers associated with the distributed
resets are unbounded, 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\@.
%
\apar{7.1-2}
We therefore introduce an \emph{incarnation number} for each process\@.
Two 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\@.
%
\apar{7.1-3}
It turns out that a bound of two on the incarnation number is
insufficient\@. 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 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\@.
%
\begin{figure*}[htbp]
\setlength{\unitlength}{0.00024in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
\reset@font\fontsize{#1}{#2pt}%
\fontfamily{#3}\fontseries{#4}\fontshape{#5}%
\selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(18661,4290)(0,-10)
\put(12300,3193){\blacken\ellipse{100}{100}}
\put(12300,3193){\ellipse{100}{100}}
\path(12525,2193)(12900,2193)
\path(12660.000,2133.000)(12900.000,2193.000)(12660.000,2253.000)
\put(11625,3768){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}Legend}}}}}
\put(14400,2568){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}failed process}}}}}
\put(14400,3093){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}up process}}}}}
\put(13050,2043){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}\emph{k}}}}}}
\put(14400,2043){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}parent of \emph{j} is \emph{k}}}}}}
\put(12300,1518){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}\emph{j}, 0}}}}}
\put(14400,1518){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}incarnation number of \emph{j} is 0}}}}}
\put(12300,2043){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}\emph{j}}}}}}
\put(12525,2568){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}\emph{j}:}}}}}
\put(12525,3093){\makebox(0,0)[lb]{\smash{{{\SetFigFont{10}{10}{\familydefault}{\mddefault}{\updefault}\emph{j}:}}}}}
\put(300,4218){\blacken\ellipse{100}{100}}
\put(300,4218){\ellipse{100}{100}}
\put(1500,4218){\blacken\ellipse{100}{100}}
\put(1500,4218){\ellipse{100}{100}}
\put(2700,4218){\blacken\ellipse{100}{100}}
\put(2700,4218){\ellipse{100}{100}}
\put(600,2418){\blacken\ellipse{100}{100}}
\put(600,2418){\ellipse{100}{100}}
\put(1800,2418){\blacken\ellipse{100}{100}}
\put(1800,2418){\ellipse{100}{100}}
\put(4350,2418){\blacken\ellipse{100}{100}}
\put(4350,2418){\ellipse{100}{100}}
\put(5550,2418){\blacken\ellipse{100}{100}}
\put(5550,2418){\ellipse{100}{100}}
\put(5400,4218){\blacken\ellipse{100}{100}}
\put(5400,4218){\ellipse{100}{100}}
\put(6600,4218){\blacken\ellipse{100}{100}}
\put(6600,4218){\ellipse{100}{100}}
\put(4200,4218){\blacken\ellipse{100}{100}}
\put(4200,4218){\ellipse{100}{100}}
\put(9300,4143){\blacken\ellipse{100}{100}}
\put(9300,4143){\ellipse{100}{100}}
\put(10500,4143){\blacken\ellipse{100}{100}}
\put(10500,4143){\ellipse{100}{100}}
\put(8100,4143){\ellipse{100}{100}}
\put(4350,2418){\blacken\ellipse{100}{100}}
\put(4350,2418){\ellipse{100}{100}}
\put(12300,2668){\ellipse{100}{100}}
\path(1500,4218)(2700,4218)
\path(1740.000,4278.000)(1500.000,4218.000)(1740.000,4158.000)
\path(300,4218)(1500,4218)
\path(540.000,4278.000)(300.000,4218.000)(540.000,4158.000)
\path(600,2418)(1800,2418)
\path(1560.000,2358.000)(1800.000,2418.000)(1560.000,2478.000)
\path(5400,4218)(6600,4218)
\path(5640.000,4278.000)(5400.000,4218.000)(5640.000,4158.000)
\path(4200,4218)(5400,4218)
\path(4440.000,4278.000)(4200.000,4218.000)(4440.000,4158.000)
\path(9300,4143)(10500,4143)
\path(10260.000,4083.000)(10500.000,4143.000)(10260.000,4203.000)
\path(8100,4143)(9300,4143)
\path(4350,2418)(5550,2418)
\path(5310.000,2358.000)(5550.000,2418.000)(5310.000,2478.000)
\put(0,3843){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}3, 0}}}}}
\put(1200,3843){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}1, 0}}}}}
\put(2550,3843){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}2, 0}}}}}
\put(300,1968){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}1, 1}}}}}
\put(1650,1968){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}2, 1}}}}}
\put(4050,1968){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}1, 1}}}}}
\put(5400,1968){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}2, 0}}}}}
\put(825,3018){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}(a)}}}}}
\put(5100,3018){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}(b)}}}}}
\put(9150,3018){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}(c)}}}}}
\put(900,1068){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}(d)}}}}}
\put(4725,1218){\makebox(0,0)[lb]{\smash{{{\SetFigFont{12}{12}{\familydefault}{\mddefault}{\updefault}(e)}}}}}
\put(3900,3768){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}3, 1}}}}}
\put(5100,3768){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}1, 1}}}}}
\put(6450,3768){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}2, 0}}}}}
\put(7800,3693){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}3, 1}}}}}
\put(9000,3693){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}1, 1}}}}}
\put(10350,3693){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}2, 0}}}}}
\end{picture}
}
\afigcap{10}{Insufficiency of two incarnation numbers}
\end{figure*}
\asubsection{7.2}{Designing Multitolerant Applications using Three Incarnation Numbers}
%
\apar{7.2-1}
It is possible to determine the current incarnation number if we
use ternary (\(0, 1, \textrm{or }2\)) incarnation numbers and follow the rule
that a new incarnation number \(B \plusthree 1\) can be created only if
the incarnation number \(B \minusthree 1\) does not exist in the system
(in this section, we let \plusthree and \minusthree 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\@.
%
\apar{7.2-2}
\textit{When to Reset the Local State of a Process.}
When process \(j\) propagates 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\@.
%
\apar{7.2-3}
\textit{When to Create a New Incarnation Number.}
As motivated above, all three incarnation numbers should not exist
simultaneously\@. Hence, we ensure that a process changes its
incarnation number from \(B\) to \(B \plusthree 1\) only if no process
with incarnation number \(B \minusthree 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 process with incarnation number \(B
\minusthree 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 \minusthree 1\)\@. Hence, when the root
process completes a reset wave successfully, it can safely increment
its incarnation number\@.
%
\apar{7.2-4}
\textit{When to Declare that Reset is Complete\@.}
When a root completes a reset wave successfully with incarnation
number \(B\), no process in the system has incarnation number \(B
\minusthree 1\)\@. It is, however, possible that some processes have
incarnation number \(B \plusthree 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
\emph{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\@.
%
\apar{7.2-5}
\textbf{Variables.}
Every process \(j\) maintains the following variables:
\begin{itemize}
\item \(inc.j\), the incarnation number: one of 0, 1, or 2, and
\item \(ares.j\), application result: a Boolean.
\end{itemize}
%
\apar{7.2-6}
\textbf{Actions.}
Program \textit{APP} consists of nine actions for each process \(j\)\@. The
first three actions implement the reset wave\@. These actions are
obtained by modifying actions \(\textit{MSR1}\)--\(\textit{MSR3}\) to update \emph{inc} and \emph{ares}
appropriately\@. Action \textit{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 \textit{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 \textit{APP3} is the completion action; whenever \(j\) completes a
reset wave, \(j\) sets \(ares.j\) to \emph{true} if
and only if all children of \(j\) have the
same incarnation number and their application result is \emph{true}\@. Finally,
the remaining actions \textit{APP4}--\textit{APP9} break cycles in the graph of parent
relation and maintain the underlying tree; these actions are identical
to the actions \textit{MSR4}--\textit{MSR9} of program \textit{MSR}\@.
%
{\small
\begin{tabbing}
\prgmark \\
\textit{APP1} \(::\) \= \(\longrightarrow\) \= \kill
\textit{APP1} \(::\) \> \> \(par.j\!=\!j\;\ad\;st.j = \textit{normal}\; \ad\) \{\(j\) needs to initiate a new reset wave\}\\
\> \(\longrightarrow\) \> \(st.j,\;sn.j := \textit{reset},\;sn.j\! \oplus \!1\);\\
\>\> \textbf{if} (\(new.j \! = \! 0)\) \textbf{then} \hspace*{2em} \(inc.j := inc.j \! \plusthree \! 1\); \{reset application state\} \\
\ \\
\textit{APP2} \(::\) \>\> \(root.j\!=\!root.(par.j)\;\ad\;col.(par.j)\!=\!\mathrm{green}\; \ad\;st(par.j)\!=\!\textit{reset}\)\\
\>\>\(\ad\;sn.j\!\not=\!sn.(par.j)\) \\
\> \(\longrightarrow\) \> \(st.j,\;sn.j:=\textit{reset},\;sn.(par.j);\)\\
\>\> \textbf{if} (\((inc.j \! \plusthree \! 1) = inc.(par.j))\)) \textbf{then}\\
\>\> \hspace*{2em} \(inc.j := inc.(par.j)\); \{reset application state\} \\
\ \\
\textit{APP3} \(::\) \>\> \(st.j \! = \! \textit{reset} \;\ad\;col.j \! = \! \mathrm{green}\;\ad\)\\
\>\>\((\forall l:l\in ch.j:st.l\not =\textit{reset}) \; \ad \)\\
\>\>\((\forall l:l\in Adj.j:root.l=root.j \ad sn.j=sn.l)\)\\
\> \(\longrightarrow\) \> \(st.j,ares.j := \textit{normal}, (\forall l : l \! \in \! ch.j : ares.l\;\ad\;(inc.j\!=\!inc.l));\)\\
\>\> \textbf{if} (\(\exists l : l \!\in\!Adj.j \! \union \! \{ j \} : new.l\!>\!0\)) \textbf{then}\\
\>\> \hspace*{2em} \= \textbf{if} \((par.j\!=\!j)\) \textbf{then} \(st.j,\;sn.j := \textit{reset}, sn.j\! \oplus\!1\);\\
\>\>\> \textbf{else} \(new.(par.j) := max(new.(par.j), 1)\)\\
\>\> \textbf{else if} \((par.j\!=\!j \;\ad\;ares.j)\) \textbf{then} \hspace*{2em} \{declare reset complete\}\\
\>\> \textbf{else if} \((par.j\!=\!j \;\ad\;\neg ares.j)\) \textbf{then}\\
\>\> \hspace*{2em} \= \(st.j, sn.j,inc.j := \textit{reset}, sn.j\! \oplus\!1,inc.j \plusthree 1;\)\\
\>\>\> \{reset application state\};\\
\>\> \(new.j := max(0, new.j \! - \! 1)\)\\
%
\ \\
%
\(APP4 ::\) \> \(\textit{MSR4}\)\\
\hspace*{5.5em}\(\vdots\)\\
\(APP9 ::\) \> \(\textit{MSR9}\)\\
\prgmark \\
\afigcap{11}{\normalsize Actions of program \emph{APP} at process \(j\)}
\end{tabbing}
}
%
\apar{7.2-7}
\textit{Outline of the Proof.}
We need to show that:
\begin{enumerate}
\item when a root process with incarnation number
\(B\) declares that a reset is complete, all processes have incarnation
number \(B\);
\item at most two incarnation numbers coexist at any invariant
state; and
\item after a reset operation is initiated at an invariant state,
the root process eventually declares that the reset is complete\@.
\end{enumerate}
%
\apar{7.2-8}
When \(j\) completes a reset wave, it checks that the
incarnation number of \(j\) is the same as its children\@. Thus, when
\(j\) completes its reset wave, it 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 \textit{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\@.
%
\apar{7.2-9}
To satisfy condition 2, we show that when a process creates a new incarnation
number \(B \plusthree 1\) after completing a reset wave with
incarnation number \(B\), no process has incarnation number \(B
\minusthree 1\)\@. Suppose not: consider the first process, say \(j\),
that has incarnation number \(B \minusthree 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 \minusthree 1\), since
\(par.j\) has propagated the reset wave and \(j\) is the first process to
change its incarnation number to \(B \minusthree 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 \plusthree
1\); and (3) if the incarnation number of \(par.j\) is \(B \plusthree 1\), then
before \(j\) propagates the reset wave, the incarnation number of \(j\) cannot
be \(B \minusthree 1\), as only two incarnation numbers coexist\@. Thus,
condition~2 above is satisfied\@.
%
\apar{7.2-10}
From \textit{MSR}, we know that eventually the root with incarnation number
\(B\) will either declare that reset is complete or initiate a new reset
wave with incarnation number \(B \plusthree 1\)\@. Upon propagation of this
reset wave, all processes with incarnation number \(B\) change their
incarnation number to \(B \plusthree 1\)\@. It follows that the root will
eventually declare that the reset is complete\@. Thus, condition 3 is satisfied\@.
\asection{8}{Conclusions} \label{sec:conclusion}
%
\apar{8-1}
In this paper, we presented a bounded-memory distributed reset
program 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\@.
%
\apar{8-2}
Distributed reset programs belong to the class of total programs
\cite{cj98-04-04}\@. 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 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\@.
%
\apar{8-3}
Our discussion of distributed reset has intentionally omitted how the
application 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\@.
%
\apar{8-4}
In our program, in stable states, the processes form a rooted tree
and 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 \cite{cj98-04-07,cj98-04-06}\@. 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\@.
%
\apar{8-5}
Finally, we reiterate that our assumption that the distributed reset
request 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 \cite{cj98-04-02} 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\@.
%
\asection{A}{Appendix} \label{sec:appendix}
%
\asubsection{A.1}{Proof of Masking-Fault Tolerance of Program \textit{MR}} \label{sec:corr}
%
\apar{A.1-1}
\textbf{Invariant for the Masking-Distributed Reset.}
As described in Section 5, the predicates
\(T_{TREE}\), \(NGD\), and \(I1\) are in the invariant, \(S_{MR}\), of the
masking reset\@. Here, we characterize the remaining predicates in
\(S_{MR}\)\@.
%
\apar{A.1-2}
First, we recall the definition of \(X.j\) from Section 5.2:
%
\begin{tabbing}
\hspace*{2em}
\= \(X.j \;= \;\) \= \(\{ j \}\) \hspace*{7.5em} \= \textbf{if} \= \(par.j\!=\!j\;\vee\;
par.j \! \not \in Adj.j\)\\
\>\>\>\>\(\vee\;col.j \! = \! \mathrm{red}\;\vee\; root.j \! \not = \!root.(par.j)\)\\
\>\> \(\{ j \} \union X.(par.j)\) \> \textbf{otherwise}\\
\end{tabbing}
%
\apar{A.1-3}
Intuitively, \(X.j\) denotes the green-colored ancestors of \(j\) that
have the same root value as \(j\)\@.
%
\apar{A.1-4}
For the following discussion (predicates \(I2\)--\(I8\)), we assume that
\(j\) and \(l\) are two processes such that \(k \! \in 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\! \in Adj.j\) (i.e., \(l\) is a process adjacent to
\(j\))\@.
%
\apar{A.1-5}
When \(j\) completes a reset wave, \(sn.j\) is the same as \(sn.l\)\@. The
predicate \(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 \emph{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:
%
\begin{tabbing}
\hspace*{0em} \= \(I2 = \) \= \kill
\> \(I2 = \)\> \((new.j \! \not = \! 2\;\;\ad\;\;new.l \! \not = \! 2)\)
\hspace*{0.75em} \= \(\Rightarrow \)
\hspace*{0.75em} \=
\hspace*{0.75em} \= \((st.j \! \not = \! reset \; \equiv \; sn.j \! = \! sn.l)\)\\
\>\>\>\> \(\vee\) \> \((\forall m : m \! \in X.l : sn.m \! = \! sn.l)\)\\
\end{tabbing}
%
\apar{A.1-6}
When \(j\) completes a reset wave and decrements \(new.j\) from 1 to 0,
\(j\) is in the reset state and \(sn.j\) is the same as \(sn.l\)\@. Thus,
from the predicate \(I2\), the second disjunct, \((\forall m : m \! \in
X.l : sn.m \! = \! sn.l)\), must be \emph{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
\emph{NGD})\@. Thus, the predicate \(I3\) is in the invariant, where:
%
\begin{tabbing}
\hspace*{0em} \= \(I3 = \) \= \kill
\> \(I3 = \)\> \((st.j\! \not = \! reset \;\ad\;sn.j \! = \! sn.k\) \\
\>\> \(\ad\; new.j \! = \! 0\;\;\ad\;\;new.l \! \not = \! 2)\)
\hspace*{2em} \= \(\Rightarrow \;\) \hspace*{0.65em}
\= \((\forall m : m \! \in X.l : sn.m \! = \! sn.k)\)\\
\end{tabbing}
%
\apar{A.1-7}
Consider the case where \(k\) starts a new reset wave by changing
\(sn.k\): From \(I3\), observe that all processes in \(X.l\) have the same
sequence number (in this case, different from \(sn.k\)) unless
\(k\!\in\!X.l\)\@. If \(k\!\in\!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:
%
\begin{tabbing}
\hspace*{0em} \= \(I4 = \) \= \kill
\> \(I4 = \) \> \((sn.j \not= sn.k\;\ad\;new.j = 0\) \=\\
\>\> \(\ad\;new.l \! \not= \! 2)\) \> \(\Rightarrow \) \= \hspace*{0.75em}
\= \((\forall m : m \! \in X.l : sn.m \! \not = \! sn.k)\)\\
\>\>\>\> \(\vee\) \> \((sn.l \! \not = \! sn.k\;\ad\;\)\\
\>\>\>\>\> \((\exists m : m \! \in X.l \!
\cap des.k.k : sn.m \! = \! sn.k))\)\\
\>\>\>\> \(\vee\) \> \((sn.l \! = \! sn.k \;\ad\;l \! \in des.k.k)\)\\
\end{tabbing}
%
\apar{A.1-8}
Starting from a state where \(I4\) holds, if \(j\) propagates a reset wave
initiated 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 \emph{NGD}, all ancestors of \(l\) have the same sequence number\@.
Thus, the predicate \(I5\) is in the invariant, where:
%
\apar{A.1-9}
{\small
\begin{tabbing}
\hspace*{0em} \= \(I3=\) \= \((sn.j = sn.k \ad st.j = reset \ad\)\= \(new.j = 0 \ad new.l \not = 2 )\) \= \(\Rightarrow\) \= \(\vee\) \= \((\forall m:m \in X.l:sn.m \not = sn.k)\)\kill
\> \(I5 = \) \> \((sn.j = sn.k \ad st.j = reset \ad\)\=\\
\> \> \(new.j = 0 \ad new.l \not = 2 )\) \> \(\Rightarrow\) \= \hspace*{0.5em} \= \((\forall m : m \in X.l : sn.m \not = sn.k)\)\\
\>\>\>\> \(\vee\) \> \((sn.l \not = sn.k \ad \)\\
\>\>\>\> \> \((\exists m : m \in X.l \cap des.k.k : sn.m = sn.k))\)\\
\>\>\>\> \(\vee\) \> \((sn.l = sn.k \ad l \in des.k.k)\)\\
\>\>\>\> \(\vee\) \> \((new.l = 1 \ad\)\\
\>\>\>\>\> \((\forall m : m \in X.l : sn.m = sn.k) \ad st.l \not = reset)\)
\end{tabbing}
}
%
\apar{A.1-10}
As claimed earlier, when a process \(j\) completes a reset wave, if
\(new.l\) and \(new.j\) are zero, then \(l\) has propagated the current reset
wave initiated by \(k\)\@. Thus, the predicate \(I6\) is in the invariant,
where:
%
\begin{tabbing}
\hspace*{0em} \= \(I3 = \) \hspace*{0.75em} \= \kill
\> \(I6 = \) \> \((sn.j \! = \! sn.k \! = \!sn.l\;\;\ad\;\;st.j\!=\!reset\;\;\ad\)
\hspace*{0.75em} \=\\
\>\> \(new.j \! = \! 0\;\;\ad\;\;new.l \! = \! 0) \) \> \(\Rightarrow \) \=
\hspace*{0.75em} \((l \! \in des.k.k)\)\\
\end{tabbing}
%
\apar{A.1-11}
When \(k\) starts a new reset wave, if \(sn.j\) is different from \(sn.k\),
\(j\) has not 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:
%
\begin{tabbing}
\hspace*{0em} \= \(I3 = \) \hspace*{0.75em} \= \kill
\> \(I7 = \)\> \( (new.j\!=\!0)\) \hspace*{1em} \=
\(\Rightarrow\) \hspace*{0.75em} \= \hspace*{0.75em} \=
\((sn.j \! \not = \! sn.k \;\Rightarrow\; pc.j.k \! = \! \phi)\)\\
\>\>\>\> \(\ad\)\> \((sn.j \! = \! sn.k \;\Rightarrow\; pc.j.k \! \in \! ch.j)\)
%
\end{tabbing}
%
\apar{A.1-12}
Finally, if \(j\) and \(par.j\) are propagating a reset wave initiated by
\(k\;\) and \(\;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:
%
\begin{tabbing}
\hspace*{0em} \= \(I8 = \hspace*{0.75em}
(par.j \in des.k.k \ad sn.j = sn.(par.j) \ad st.j = reset) \Rightarrow (j \in des.k.k)\)\\
\end{tabbing}
%
\apar{A.1-13}
Thus, the invariant of the masking distributed-reset program, \textit{MR}, is:
%
{\small
\begin{tabbing}
\(S_{MR} =\) \= \((NGD\;\ad\;T_{TREE}\;\ad\;(\forall j, l : k \! \in \! X.j \;\ad\;l \! \in \! Adj.j
\;\ad\;root.j\!=\!root.l\!=\!k : \)\\
\> \hspace*{12em}
\(I1\;\ad
I2\;\ad
I3\;\ad
I4\;\ad
I5\;\ad
I6\;\ad
I7\;\ad
I8\))\\
\end{tabbing}
}
%
\begin{alabsubtext}{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 \textit{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\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{4}{}
\prooffontshape
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\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 4}}
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{5}{}
At any state where \(S_{MR}\) holds, if a root process \(k\) declares that a
distributed reset has completed (by executing action \(\textit{MR3}\)), then
\(nbrs(des.k.k)\subseteq (des.k.k\!\union\!\textit{failed.k})\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{5}{}
\prooffontshape
When \(k\) declares that reset is complete by executing action \textit{MR3}, we
have:
%
\begin{tabbing}
\hspace*{2em} \=
\((\forall l : l \! \in \! (Adj.k \! \union \{ k \}) : new.l \! = \!0\;\ad\;
root.l \! = \! root.k \; \ad\; sn.l \! = \!sn.k)\;\;\;\ad\)\\
\> \((\forall l : l \! \in ch.k : st.j \! \not = \! reset)\;\;\;\ad\;\;\;(st.k\!=\!reset)\)\\
\(\Rightarrow\) \> \hspace*{2em} \= \{from \(I6, I1, I7\)\}\\
\> \((\forall l : l \! \in \! (Adj.k \! \union \{ k \}) : l \! \in \!
des.k.k)\;\;\;\ad\)\\
\> \((\forall l : l \! \in ch.k : nbrs(des.l.k) \! \subseteq \! (des.k.k \!
\union \! \textit{failed.k}))\;\;\;\ad\;\;\;(pc.k.k\!\subseteq \! ch.k)\)\\
\(\Rightarrow\) \>\> \{by predicate calculus\}\\
\> \((\forall l : l \! \in \! Adj.k : l \! \in des.k.k)\;\;\;\ad\)\\
\> \((\forall l : l \! \in pc.k.k : nbrs(des.l.k) \! \subseteq \! (des.k.k \!
\union \! \textit{failed.k}))\)\\
\(\Rightarrow\) \>\> \{by definition of \(des.k.k\)\}\\
\> \(nbrs(des.k.k) \! \subseteq \! (des.k.k\! \union \! \textit{failed.k})\)
\end{tabbing}
{\nopagebreakbeginpar\markendlst{Proof of Lemma 5}}
\end{alabsubtext}
%
\asubsection{A.2}{Proof of Stabilizing Fault Tolerance of Program \textit{MSR}} \label{sec:stabmaskproof}
%
\begin{alabsubtext}{Theorem}{4}{}
Program \textit{MSR} is masking tolerant to fail-stop and repair faults, and
stabilizing tolerant to transient faults for invariant \(S_{MSR}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Theorem}{4}{}
\prooffontshape
Here, we show that \textit{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 \cite{cj98-04-19}\@. In particular, we exhibit predicates \(S.1, S.2,
S.3,\) and \(S.4\), where:
%
\begin{tabbing}
\(S.1 =\) \= \(true\)\\
\(S.2 =\) \> \(NGD\)\\
\(S.3 =\) \> \(S.2 \; \ad\) \= graph of the parent relation forms a tree \(\ad\) \\
\> \> \((\forall j, k \) \= \(:: root.j = root.k \ad col.j = green \ad par.j \in Adj.j \ad\)\\
\> \> \>\((par.j = j \Rightarrow d.j = 0) \ad (par.j \not = j \Rightarrow d.j = d.(par.j)+1))\)\\
\(S.4 =\) \> \(S.3\;\ad\;S_{MSR}\)
\end{tabbing}
%
and show that for each \(i\), \(1\!\leq\!i\! < \!4\), \(S.i\) converges to
\(S.(i+1)\) in program \textit{MSR}\@. It follows that starting from an
arbitrary state, program \textit{MSR} reaches a state where \(S.4\) and, hence,
\(S_{MSR}\) hold\@.
%
\apar{A.2-1}
To prove \(S.1\) converges to \(S.2\), consider the set of processes for
which \(NGd.j\) is violated\@. When a process executes action \(\textit{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 \textit{MSR}\@.
%
\apar{A.2-2}
To prove that \(S.2\) converges to \(S.3\), we use a proof identical to
the convergence proof in Arora and Gouda's reset paper \cite{cj98-04-02}\@. 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
\(\textit{MSR4}\)--\(\textit{MSR9}\) are disabled\@. Actions \(\textit{MSR1}\)--\(\textit{MS3}\) trivially preserve
\(S.3\)\@. Thus, \(S.3\) is closed under execution of program \textit{MSR}\@. Also,
if the set of processes forms a rooted tree and all processes are
green, the predicate \(T_{TREE}\) holds trivially\@.
%
\apar{A.2-3}
To prove \(S.3\) converges to \(S.4\), we need to prove that the program
converges 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, is in the \emph{normal} state\@. We then prove that
in such a state, the predicates \(I1\)--\(I8\) hold\@.
%
\apar{A.2-4}
As mentioned above, in a state satisfying \(S.3\), only actions
\(\textit{MSR1}\)--\(\textit{MSR3}\) may be enabled\@.
If action \(\textit{MSR1}\) is executed, then \(k\)
is in the \emph{normal} state\@. Hence, to prove that eventually the program
reaches a state where \(k\) is in the \emph{normal} state, we can assume that
action \(\textit{MSR1}\) is not executed\@.
%
\apar{A.2-5}
Consider the variant function \( | \{ j : st.j \!= \! reset \} |\) + 2\(|
\{ j : sn.j \! \not = \! sn.k \} | \)\@. 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 \emph{normal} state\@.
%
\apar{A.2-6}
We now prove that when \(k\) is in the \emph{normal} state, the predicates
\(I1\)--\(I8\) hold\@. From \(NGD\), we have that all
processes are in the \emph{normal} state with the sequence number
\(sn.k\)\@. Hence, the following predicate is \emph{true} for each process \(j\):
%
\[(\forall j :: sn.j \! = \! sn.k\;\ad\;st.j\!\not =\!reset)\]
%
\apar{A.2-7}
Since \(k\) is not in the reset state, predicates \(I1, I5,\) and \(I6\) are
satisfied\@. Since all processes have the same sequence number, the
predicate \((\forall m : m \! \in 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 \emph{normal} state, predicates \(I4,
I7,\) and \(I8\) are also satisfied\@. Thus, when \(k\) is in the \emph{normal} state, the
predicate \(S_{MSR}\) holds\@.
%
\apar{A.2-8}
It now follows that starting from an arbitrary state, the program
execution converges to a state where the predicate \(S_{MSR}\) holds\@.
%
\apar{A.2-9}
To prove that \textit{MSR} is masking tolerant to fail-stops and repairs, we
show that newly added actions \(\textit{MSR7}, \textit{MSR8},\) and \(\textit{MSR9}\) do not interfere with the
actions of program \textit{MR}\@. Toward this end, we prove the following lemma\@.
{\nopagebreakbeginpar\markendlst{Proof of Theorem 4}}
\end{alabsubtext}
%
\begin{alabsubtext}{Lemma}{6}{}
Actions MSR7, MSR8, and MSR9 preserve \(S_{MR}\), and do not execute indefinitely
after program MSR reaches a state in \(S_{MR}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{6}{}
\prooffontshape
From the above proof, eventually the program reaches a state where
\(S.3\) is satisfied\@. In a state where \(S.3\) is satisfied, \(\textit{MSR7}\)--\(\textit{MSR9}\)
are disabled\@. Since \(S.3\) is closed in \textit{MSR}, these actions
remain disabled\@. Thus, actions \(\textit{MSR7}\)--\(\textit{MSR9}\) do not execute
indefinitely\@.
%
\apar{A.2-10}
Since action \(\textit{MSR7}\) does not update any variable in \(S_{MR}\) and
\(\textit{MSR9}\) is disabled in \(S_{MR}\), these two actions trivially preserve
\(S_{MR}\)\@. Observe that when \(j\) executes action \(\textit{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, \(\textit{MSR8}\) also preserves \(S_{MR}\)\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 6}}
\end{alabsubtext}
%
\asubsection{A.3}{Refinement to Low Atomicity} \label{sec:refinement}
%
\apar{A.3-1}
In program \textit{MR}, the actions \(\textit{MR3}, \textit{MR4},\)
and \(\textit{MR6}\) of process \(j\)
update the \(new.(par.j)\) variable of \(par.j\) simultaneously with
the variables of \(j\)\@. We now refine program \textit{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\@.
%
\apar{A.3-2}
In the refined version of \textit{MR}, for each of its neighbors \(k\), \(j\)
maintains a variable \(new.j.k\) as a local copy of the nonlocal
variable \(new.k\)\@. Whenever \(j\) needs to update the \emph{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, \textit{MR} is
modified as follows (the modification to \textit{MSR} is analogous):
%
\begin{enumerate}
\item Add a variable \(new.j.k\) in \(j\) for every neighbor \(k \)\@.
\item Replace the statements \(new.k:=m\) by \(new.j.k:= m \)\@.
\item Add the following two actions, the first to \(k\) and the second to \(j\):
%
\begin{itemize}
\item \(new.j.k > 0 \;\ad \; new.j.k > new.k\;\; \longrightarrow new.k:=new.j.k\)
\item \(new.j.k > 0 \;\ad \; new.j.k \leq new.k\;\; \longrightarrow new.j.k:=0\)
\end{itemize}
%
\item Replace action \(\textit{MR3}\) of \(j\) as follows:
\begin{itemize}
\item \((\forall j : j \in Adj.j : new.j.k = 0)\;\ad\;\mathrm{guard}\;\longrightarrow\;\textrm{statement}\)
\end{itemize}
where \emph{guard} and \emph{statement} denote the guard and statement
of action \(\textit{MR3}\), respectively\@.
\end{enumerate}
%
\apar{A.3-3}
With this refinement, the predicates \(I1\) and \(I7\) of the invariant \(S_{MR}\)
change as follows:
%
\begin{tabbing}
\hspace*{2em} \= \(I3 = \) \hspace*{0.75em} \= \kill
\> \(I1^{'} = \)\> \(I1 \;\vee\;new.j.(par.j)\!>\!0\)\\
\> \(I7^{'} = \)\> \( (new.j\!=\!0)\) \hspace*{1em} \=
\(\Rightarrow\) \hspace*{0.75em} \= \hspace*{0.75em} \=
\((sn.j \! \not = \! sn.k \;\Rightarrow\; pc.j.k \! = \! \phi)\)\\
\>\>\>\> \(\ad\)\> \((sn.j \! = \! sn.k \;\Rightarrow\; pc.j.k \! \in \! ch.j \)\\
\>\>\>\> \(\vee\)\> \( (\exists l : l \! \in \! Adj.j : new.l.j \!>\!0))\)
\end{tabbing}
%
\apar{A.3-4}
And the invariant \(S_{MR}\) changes as follows:
%
\begin{tabbing}
\(S_{MR}^{'} = (NGD\;\ad\;T_{TREE}\;\ad\) \= \((\forall j, l : j \! \in \! KERN.k \;\ad\;l \! \in \! Adj.j \)\\
\>\(\ad\;root.j\!=\!root.l\!=\!k : \)\\
\>
\(I1^{'}\;\ad
I2\;\ad
I3\;\ad
I4\;\ad
I5\;\ad
I6\;\ad
I7^{'}\;\ad
I8\)))\\
\end{tabbing}
%
\apar{A.3-5}
Finally, in the fail-stop action of program \textit{MR}, the state of all of its
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\@.
\asubsection{A.4}{An Illustration of Tree Correction} \label{sec:tree-correction}
%
\apar{A4.1-1}
We illustrate how the tree maintenance program constructs a tree in
the 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\@.
%
\begin{itemize}
\item Process 4 fail-stops and process 5 repairs (see Figure 12b)\@.
\item 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)\@.
\item Since the color of process 2---the parent of 1---is red, 1 sets
its color to red (Figure 12d)\@.
\item 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)\@.
\item Since 2 has no children, 2 changes its color
to green and sets its root value to 2 (Figure 12f)\@.
\item 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)\@.
\end{itemize}
%
\begin{figure*}[b]
\setlength{\unitlength}{0.00020in}
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
\reset@font\fontsize{#1}{#2pt}%
\fontfamily{#3}\fontseries{#4}\fontshape{#5}%
\selectfont}%
\fi\endgroup%
{\renewcommand{\dashlinestretch}{30}
\begin{picture}(23638,7722)(0,-10)
\put(0,2103){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,1,green}}}}}
\put(0,6303){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,4,green}}}}}
\put(1275,903){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,5,green}}}}}
\put(1500,5103){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,4,green}}}}}
\put(2025,3228){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(2850,2103){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,4,red}}}}}
\put(3075,6303){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,4,green}}}}}
\put(3225,903){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,green}}}}}
\put(3450,5103){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5}}}}}
\put(5325,2028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,1,green}}}}}
\put(6600,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,5,green}}}}}
\put(7350,3153){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(1950,7353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4,4,\emph{green}}}}}}
\put(6975,5028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,4,green}}}}}
\put(8925,5028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,red}}}}}
\put(5700,6228){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,4,green}}}}}
\put(7650,7353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(8175,2028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,2,green}}}}}
\put(8550,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,green}}}}}
\put(8550,6228){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,4,green}}}}}
\put(11100,6228){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,4,green}}}}}
\put(11250,2028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,5,green}}}}}
\put(12375,5028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,4,green}}}}}
\put(12525,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,5,green}}}}}
\put(13125,7353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(13275,3153){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(13950,6228){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,4,red}}}}}
\put(14100,2028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,5,green}}}}}
\put(14325,5028){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,green}}}}}
\put(14475,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,green}}}}}
\put(17175,6378){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}1,4,red}}}}}
\put(17400,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\updefault}3,4,\emph{green}}}}}}
\put(17400,1353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\itdefault}j}}}}}
\put(17625,1878){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\itdefault}j:}}}}}
\put(17625,2403){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\itdefault}j:}}}}}
\put(18150,1353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\itdefault}k}}}}}
\put(18450,5178){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}3,4,green}}}}}
\put(19200,7503){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\updefault}4}}}}}
\put(19500,828){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\updefault}\emph{root}.3=4 and \emph{col}.3=\emph{green}}}}}}
\put(19500,1878){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\updefault}failed process}}}}}
\put(19500,2403){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\updefault}up process}}}}}
\put(19500,1353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\familydefault}{\mddefault}{\updefault}parent of \emph{j} is \emph{k}}}}}}
\put(20025,6378){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}2,4,red}}}}}
\put(20400,5178){\makebox(0,0)[lb]{\smash{{{\SetFigFont{4}{4}{\rmdefault}{\mddefault}{\itdefault}5,5,green}}}}}
\put(2100,4353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(a)}}}}}
\put(7650,4353){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(b)}}}}}
\put(13050,4428){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(c)}}}}}
\put(19125,4503){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(d)}}}}}
\put(1950,78){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(e)}}}}}
\put(7200,153){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(f)}}}}}
\put(13275,78){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}(g)}}}}}
\put(16725,3078){\makebox(0,0)[lb]{\smash{{{\SetFigFont{8}{8}{\familydefault}{\mddefault}{\updefault}Legend}}}}}
\put(12700,6303){\blacken\ellipse{100}{100}}
\put(12700,6303){\ellipse{100}{100}}
\put(13900,6303){\blacken\ellipse{100}{100}}
\put(13900,6303){\ellipse{100}{100}}
\put(14575,5403){\blacken\ellipse{100}{100}}
\put(14575,5403){\ellipse{100}{100}}
\put(13300,7203){\ellipse{100}{100}}
\put(19375,5553){\blacken\ellipse{100}{100}}
\put(19375,5553){\ellipse{100}{100}}
\put(18775,6453){\blacken\ellipse{100}{100}}
\put(18775,6453){\ellipse{100}{100}}
\put(19975,6453){\blacken\ellipse{100}{100}}
\put(19975,6453){\ellipse{100}{100}}
\put(20650,5553){\blacken\ellipse{100}{100}}
\put(20650,5553){\ellipse{100}{100}}
\put(19375,7353){\ellipse{100}{100}}
\put(2200,1278){\blacken\ellipse{100}{100}}
\put(2200,1278){\ellipse{100}{100}}
\put(1600,2178){\blacken\ellipse{100}{100}}
\put(1600,2178){\ellipse{100}{100}}
\put(2800,2178){\blacken\ellipse{100}{100}}
\put(2800,2178){\ellipse{100}{100}}
\put(3475,1278){\blacken\ellipse{100}{100}}
\put(3475,1278){\ellipse{100}{100}}
\put(2200,3078){\ellipse{100}{100}}
\put(7525,1203){\blacken\ellipse{100}{100}}
\put(7525,1203){\ellipse{100}{100}}
\put(6925,2103){\blacken\ellipse{100}{100}}
\put(6925,2103){\ellipse{100}{100}}
\put(8125,2103){\blacken\ellipse{100}{100}}
\put(8125,2103){\ellipse{100}{100}}
\put(8800,1203){\blacken\ellipse{100}{100}}
\put(8800,1203){\ellipse{100}{100}}
\put(7525,3003){\ellipse{100}{100}}
\put(13300,5403){\blacken\ellipse{100}{100}}
\put(13300,5403){\ellipse{100}{100}}
\put(13450,1203){\blacken\ellipse{100}{100}}
\put(13450,1203){\ellipse{100}{100}}
\put(12850,2103){\blacken\ellipse{100}{100}}
\put(12850,2103){\ellipse{100}{100}}
\put(14050,2103){\blacken\ellipse{100}{100}}
\put(14050,2103){\ellipse{100}{100}}
\put(14725,1203){\blacken\ellipse{100}{100}}
\put(14725,1203){\ellipse{100}{100}}
\put(13450,3003){\ellipse{100}{100}}
\put(2425,5478){\blacken\ellipse{100}{100}}
\put(2425,5478){\ellipse{100}{100}}
\put(1825,6378){\blacken\ellipse{100}{100}}
\put(1825,6378){\ellipse{100}{100}}
\put(2425,7278){\blacken\ellipse{100}{100}}
\put(2425,7278){\ellipse{100}{100}}
\put(3025,6378){\blacken\ellipse{100}{100}}
\put(3025,6378){\ellipse{100}{100}}
\put(3700,5478){\ellipse{100}{100}}
\put(7900,5403){\blacken\ellipse{100}{100}}
\put(7900,5403){\ellipse{100}{100}}
\put(7300,6303){\blacken\ellipse{100}{100}}
\put(7300,6303){\ellipse{100}{100}}
\put(8500,6303){\blacken\ellipse{100}{100}}
\put(8500,6303){\ellipse{100}{100}}
\put(9175,5403){\blacken\ellipse{100}{100}}
\put(9175,5403){\ellipse{100}{100}}
\put(7900,7203){\ellipse{100}{100}}
\put(17500,1978){\ellipse{100}{100}}
\put(17500,2503){\blacken\ellipse{100}{100}}
\put(17500,2503){\ellipse{100}{100}}
\path(19375,7353)(18775,6453)
\path(18775,6453)(19975,6453)
\blacken\path(19735.000,6393.000)(19975.000,6453.000)(19735.000,6513.000)(19663.000,6453.000)(19735.000,6393.000)
\path(18775,6453)(19375,5553)
\path(19375,7353)(19975,6453)
\blacken\path(19558.051,7186.590)(19375.000,7353.000)(19458.205,7120.026)(19548.066,7093.400)(19558.051,7186.590)
\path(19375,5553)(20650,5553)
\path(19975,6453)(19375,5553)
\blacken\path(19891.795,6220.026)(19975.000,6453.000)(19791.949,6286.590)(19801.934,6193.400)(19891.795,6220.026)
\path(13300,7203)(12700,6303)
\path(12700,6303)(13900,6303)
\blacken\path(13660.000,6243.000)(13900.000,6303.000)(13660.000,6363.000)(13588.000,6303.000)(13660.000,6243.000)
\path(12700,6303)(13300,5403)
\path(13900,6303)(13300,5403)
\blacken\path(13816.795,6070.026)(13900.000,6303.000)(13716.949,6136.590)(13726.934,6043.400)(13816.795,6070.026)
\path(13300,7203)(13900,6303)
\blacken\path(13483.051,7036.590)(13300.000,7203.000)(13383.205,6970.026)(13473.066,6943.400)(13483.051,7036.590)
\path(13300,5403)(14575,5403)
\path(2200,3078)(1600,2178)
\path(1600,2178)(2800,2178)
\path(1600,2178)(2200,1278)
\path(2800,2178)(2200,1278)
\path(2200,3078)(2800,2178)
\blacken\path(2383.051,2911.590)(2200.000,3078.000)(2283.205,2845.026)(2373.066,2818.400)(2383.051,2911.590)
\path(2200,1278)(3475,1278)
\blacken\path(3235.000,1218.000)(3475.000,1278.000)(3235.000,1338.000)(3163.000,1278.000)(3235.000,1218.000)
\path(7525,3003)(6925,2103)
\path(6925,2103)(8125,2103)
\path(6925,2103)(7525,1203)
\path(8125,2103)(7525,1203)
\path(7525,3003)(8125,2103)
\blacken\path(7708.051,2836.590)(7525.000,3003.000)(7608.205,2770.026)(7698.066,2743.400)(7708.051,2836.590)
\path(7525,1203)(8800,1203)
\blacken\path(8560.000,1143.000)(8800.000,1203.000)(8560.000,1263.000)(8488.000,1203.000)(8560.000,1143.000)
\path(13450,3003)(12850,2103)
\path(12850,2103)(14050,2103)
\blacken\path(13810.000,2043.000)(14050.000,2103.000)(13810.000,2163.000)(13738.000,2103.000)(13810.000,2043.000)
\path(13450,3003)(14050,2103)
\blacken\path(13633.051,2836.590)(13450.000,3003.000)(13533.205,2770.026)(13623.066,2743.400)(13633.051,2836.590)
\path(13450,1203)(14725,1203)
\blacken\path(14485.000,1143.000)(14725.000,1203.000)(14485.000,1263.000)(14413.000,1203.000)(14485.000,1143.000)
\path(12850,2103)(13450,1203)
\blacken\path(13266.949,1369.410)(13450.000,1203.000)(13366.795,1435.974)(13276.934,1462.600)(13266.949,1369.410)
\path(14050,2103)(13450,1203)
\blacken\path(13533.205,1435.974)(13450.000,1203.000)(13633.051,1369.410)(13623.066,1462.600)(13533.205,1435.974)
\path(2425,7278)(1825,6378)
\path(1825,6378)(3025,6378)
\blacken\path(2785.000,6318.000)(3025.000,6378.000)(2785.000,6438.000)(2713.000,6378.000)(2785.000,6318.000)
\path(1825,6378)(2425,5478)
\path(3025,6378)(2425,5478)
\blacken\path(2941.795,6145.026)(3025.000,6378.000)(2841.949,6211.590)(2851.934,6118.400)(2941.795,6145.026)
\path(2425,7278)(3025,6378)
\blacken\path(2608.051,7111.590)(2425.000,7278.000)(2508.205,7045.026)(2598.066,7018.400)(2608.051,7111.590)
\path(2425,5478)(3700,5478)
\path(7900,7203)(7300,6303)
\path(7300,6303)(8500,6303)
\blacken\path(8260.000,6243.000)(8500.000,6303.000)(8260.000,6363.000)(8188.000,6303.000)(8260.000,6243.000)
\path(7300,6303)(7900,5403)
\path(8500,6303)(7900,5403)
\blacken\path(8416.795,6070.026)(8500.000,6303.000)(8316.949,6136.590)(8326.934,6043.400)(8416.795,6070.026)
\path(7900,7203)(8500,6303)
\blacken\path(8083.051,7036.590)(7900.000,7203.000)(7983.205,6970.026)(8073.066,6943.400)(8083.051,7036.590)
\path(7900,5403)(9175,5403)
\path(17725,1503)(18100,1503)
\path(17760.000,1443.000)(18000.000,1503.000)(17760.000,1563.000)
\end{picture}
}
\afigcap{12}{Tree correction} \label{fig:tree}
\end{figure*}
\clearpage
\asubsection{A.5}{Notation}
%
\begin{center}
\begin{tabular}[]{|p{17em} | p{9em}|}
\hline
\multicolumn{2}{|l|}{Symbols}\\
\hline
\(p\) & Program \\
\(F, F1, F2\) & Faults \\
\hline
\(D, S, T, I1\!-\!I8 \) & State predicates \\
\(R, NR, MR, MSR, APP\) & Programs \\
\(R1\!-\!R3, NR1\!-\!NR6, MR1\!-\!MR6\) & Actions \\
\( MSR1\!-\!MSR9, APP1\!-\!APP9\) & {}\\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}[]{|p{12em} | p{7em} | p{9em}|}
\hline
Variables & Domain & Read As\\
\hline
\(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\\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}[]{|p{12em} | p{7em} | p{9em}|}
\hline
\multicolumn{3}{|l|}{Propositional Connectives (in decreasing order of precedence)}\\
\hline
\(\neg \) & \multicolumn{2}{l|}{Negation} \\
\(\ad, \vee\) & \multicolumn{2}{l|}{Conjunction, disjunction} \\
\(\Rightarrow, \Leftarrow\) & \multicolumn{2}{l|}{Implication, consequence} \\
\(\equiv, \not \equiv\) & \multicolumn{2}{l|}{Equivalence, inequivalence} \\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}[]{|p{12em} | p{7em} | p{9em}|}
\hline
\multicolumn{3}{|l|}{First-Order Quantifiers}\\
\hline
\(\forall, \exists\) & \multicolumn{2}{l|}{Universal, existential} \\
\hline
\end{tabular}
\end{center}
%
\end{articletext}
%
\begin{articlebib}
\bibliographystyle{alpha}
\bibliography{cj98-04}
\end{articlebib}
%
\end{document}