\begin{figure}[htbp]
\centerline{\epsfbox{figs/org.eps}}
\caption{Organization of the book}
\label{fig:chapoutline}
\end{figure}
\begin{figure}[htbp]
\begin{center}
\begin{tabular}{|l | l|}
\hline
$N$ & The number of processes \\
$P_1,P_2,\ldots,P_{N}$ & Processes \\
$G$ & Global state \\
$E$ & Set of events\\
$e,f,g$ & Events\\
$s,t,u$ & Local states\\
$ \peim$ & Immediately precedes relation\\
$ \pe$ & Locally precedes relation\\
$ \leadsto$ & Remotely precedes relation\\
$\ra$ & Happened before relation\\
$\ras$ & Potential causality relation\\
$||$ & Concurrency relation\\
$S_i$ & Sequence of states on $P_i$\\
$next(e)$ & Event immediately after $e$\\
$prev(e)$ & Event immediately before $e$\\
$e.p$ & Process on which event $e$ is executed\\
\hline
\end{tabular}
\caption{ \label{tbl:model} Notation}
\end{center}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/first-1.1.eps}}
\caption{An example of topology of a distributed system}
\label{fig:topology}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/first-1.2.eps}}
\caption{A simple distributed program with two processes} 
\label{fig:process}
\end{figure}




\begin{figure}[htbp]
\centerline{\epsfbox{figs/first-2.1.eps}}
\caption{An example of a global state and a transition} 
\label{fig:global-trans}
\end{figure}

\begin{figure}[htbp]
\centerline{\epsfbox{figs/first-3.2.eps}}
\caption{A run in the event-based happened before model}
\label{fig:run}
\end{figure}
\begin{figure}[htbp]
\centerline{\epsfbox{figs/pot-causality.eps}}
\caption{A run in the event-based potential causality model}
\label{fig:pot}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/first-3.1.eps}}
\caption{A run in the event-based model}
\label{fig:run-event}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/2run.eps}}
\caption{A run in the state-based model}
\label{fig:run-state}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/noninterleaving.eps}}
\caption{Posets on states with no valid event based posets}
\label{fig:noncomp}
\end{figure}

\begin{figure}[htbp]
\centerline{\epsfbox{figs/2clock.eps}}
\caption[An illustration of a clock assignment]
{An illustration of a clock assignment that sets $C(u) = C(v)$.
\label{fig:clock}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \> $c$: integer initially $0$;\\
\\
\>send event $(s,send,t)$:\\
\>      \>// $s.c$ is sent as part of the message \\
\>      \>$t.c := s.c + 1;$\\
\\
\>receive event $(s,receive(u),t)$:\\
\>      \>$t.c := max(s.c, u.c) + 1;$\\
\\
\>internal event $(s,internal,t)$:\\
\>      \> $t.c := s.c + 1;$
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A logical clock algorithm\label{fig:logical}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> \> $v$: array[$1$..$N$] of integer\\
\> \> \>  initially $(\forall i: i \neq j : v[i] = 0) \mya (v[j] = 1)$;\\
\\
\>send event $(s,send,t)$:\\
\>	\>$t.v := s.v;$\\
\>	\>$t.v[j] := t.v[j] + 1;$\\
\\
\>receive event $(s,receive(u),t)$:\\
\>	\>{\bf for} $i := 1$ to $N$ {\bf do}\\
\>	\>	\>$t.v[i] := \max(s.v[i], u.v[i]);$\\
\>	\>$t.v[j] := t.v[j] + 1;$\\
\\
\>internal event $(s,internal,t)$:\\
\>	\> $t.v := s.v;$\\
\>	\>$t.v[j] := t.v[j] + 1;$\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A vector clock algorithm  \label{fig:vc1}}
\end{figure}


\begin{figure}
\begin{center}
\hspace*{-0.6in}
\centerline{\epsfbox{figs/VectorAlgoFig.eps}}
%\input{figs/VectorAlgoFig.latex}
%\vspace*{1.0in}
\caption{A sample execution of the vector clock algorithm \label{fig:vectorclock}}
\end{center}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> \> $v$: array[$1$..$N$] of integer\\
\> \> \>  initially $(\forall i: i \neq j : v[i] = 0) \mya (v[j] = 1)$;\\
\>      \>$ \{ initial(s) \Rightarrow (\forall i: i \neq s.p : s.v[i] = 0) \mya (s.v[s.p] = 1)$ \}\\
\\
\>send event $(s,send,t)$:\\
\>	\>$t.v := s.v;$\\
\>	\>$t.v[t.p] := t.v[t.p] + 1;$\\
\> \> \{$ (\forall i : i \neq t.p : t.v[i] = s.v[i]) \mya t.v[t.p] > s.v[t.p])$\}\\
\\
\>receive event $(s,rcv(u),t)$:\\
\>	\>{\bf for} $i := 1$ to $N$ {\bf do}\\
\>	\>	\>$t.v[i] := \max(s.v[i], u.v[i]);$\\
\>	\> \{$(\forall i : t.v[i] = \max(s.v[i],u.v[i]))$ \}\\
\\
\>internal event $(s,internal,t)$:\\
\>	\> $t.v := s.v;$\\
\>       \> \{$	t.v = s.v$\}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{The vector clock algorithm VC2 \label{fig:vc2}}
\end{figure}


\begin{figure}
%\hspace*{-0.6in}
\centerline{\epsfbox{figs/2VectorAlgoFig.eps}}
%\input{figs/VectorAlgoFig.latex}
%\vspace*{1.0in}
\caption{A sample execution of the vector clock algorithm VC2\label{fig:vclock}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> \> $v$: array[$1$..$N$] of integer\\
\> \> \>  initially $(\forall i: i \neq j : v[i] = 0) \mya (v[j] = 1)$;\\
\\
\>send event $(s,send,t)$:\\
\>	\>$t.v[t.p] := s.v[t.p]+1;$\\
\\
\>receive event $(s,rcv(u),t)$:\\
\>	\>$t.v[t.p] := \max(s.v[t.p], u.v[u.p])+1;$\\
\>      \>$t.v[u.p] := \max(u.v[u.p], s.v[u.p])$;\\
\\
\>internal event $(s,internal,t)$:\\
\>	\>$t.v[t.p] := s.v[t.p]+1;$\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A direct-dependency clock algorithm\label{fig:dd}}
\end{figure}

\begin{figure}[htbp]
\vspace*{0.2in}
\begin{center}
\setlength{\unitlength}{0.8pt}
\begin{picture}(300,150)
\put(  0,  0){\vector(1,0){300}}
\put(  0, 75){\vector(1,0){300}}
\put(  0,150){\vector(1,0){300}}
\put(-30,  3){$P_3$}
\put(-10,  3){(0,0,1)}
\put(-30, 78 ){$P_2$}
\put(-10, 78){(0,1,0)}
\put(-30, 153){$P_1$}
\put(-10,153){(1,0,0)}
\put(215,153){(2,0,0)}
\put( 30,150){\vector( 1,-1){75}}
\put( 67,122){1}
\put(105, 78){(1,2,0)}
\put(215, 78){(1,3,0)}
\put(140, 75){\vector( 1,-1){75}}
\put(183, 37){2}
\put(215, 3){(0,2,3)}
\end{picture}
\end{center}
%\vspace*{0.5in}
\caption{A sample execution of the direct-dependency clock algorithm.\label{fig:ddclockexample}}
\end{figure}



\begin{figure}[htbp]
\begin{center}
\input{figs/IntervalFig.latex}
\end{center}
\caption{State intervals}\label{fig:interval}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_k$::\\
\> {\bf var}\\
\> \> $M_k$: array[$1$..$N$, $1$..$N$] of integer \\
\> \> \> initially $(\forall i,j: (i \neq k) \vee (j \neq k) : M_k[i,j] =
0) \mya $\\
\> \> \> \> $(M_k[k,k] = 1)$;\\
\\
\>{To send a message:}\\
\> \> \> Tag message with $M_k[\cdot,\cdot];$   \\
\> \> \> $M_k[k,k] := M_k[k,k] + 1;$ // { increment local clock}\\
%
\\
\>{Upon receipt of a message tagged with $W[\cdot,\cdot]$ from process $w.p$:}\\
\> \> \> {\bf for} $i := 1$ {\bf to} $N$, $(i \neq k)$ {\bf do} \\
\> \> \> \> $M_k[i,\cdot] := max(M_k[i,\cdot], W[i,\cdot]);$ \\
\> \> \> {\bf for} $j := 1$ {\bf to} $N$ {\bf do} \\
\> \> \> \> $M_k[k, j] := max(M_k[k, j], W[w.p, j]);$\\
\> \> \> $M_k[k,k] := M_k[k,k] + 1;$ // {increment local clock}\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{\label{fig:mclk.alg}
        Algorithm for maintaining matrix clock $M_k[\cdot,\cdot]$ at
        $P_k$.
        }
\end{figure}

\begin{figure}[htbp]
\begin{center}
\input{figs/PredFig.latex}
\end{center}
\caption{Computing $pred.(pred.(k,n).i).j$ \label{fig:multipred}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \> $v$: depclock; // direct-dependency clock \\
\> \> $q$: array[$1..N$] of integer initially $(\infty, \infty, \ldots, \infty)$;\\
\\
%\> events:: \\
\> $request$:\\
\> \> $q[i] := v[i];$\\
\> \> send ($q[i]$) to all processes; // request messages\\
\> \\
\> $release$:\\
\> \> $q[i] := \infty;$\\
\> \> send ($q[i]$) to all processes; // release messages \\
\> \\
\> $receive(u)$:\\
\> \> $q[u.p] := u.q[u.p];$\\
\> \> {\bf if} $event(u) = request$ {\bf then} \\
\> \> \> send ack to process $u.p$; // acknowledge ``request'' 
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Lamport's algorithm for mutual exclusion\label{fig:lamport}}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/mutexProof.eps}}
\caption{Messages crossing a cut}
\label{fig:messageCut}
\end{figure}

\begin{figure}[htbp]
\centerline{\epsfbox{figs/dvector.eps}}
\caption{Proof for the induction case}
\label{fig:active vector}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \> $pendingQ$: list of process ids initially $null$;\\
\> \> $myts$: integer initially $\infty$;\\
\> \> $numOkay$: integer initially $0$;\\
\> \\
%\> events:: \\
\> $request$: \\
\> \> $myts := logical\_clock;$\\
\> \> send $request$ with $myts$ to all other processes;\\
\> \> $numOkay := 0;$\\
\> \\
\> $receive(u, request)$:\\
\> \> {\bf if} $(u.myts < myts)$ {\bf then} \\
\> \> \> send $okay$ to process $u.p$;\\
\> \> {\bf else} $append(pendingQ, u.p)$;\\
\> \\
\> $receive(u, okay)$:\\
\> \> $numOkay := numOkay + 1;$\\
\> \> {\bf if} $(numOkay = N-1)$ {\bf then} \\
\> \> \> enter\_critical\_section;\\
\> \\
\> $release$:\\
\> \> $myts := \infty;$\\
\> \> {\bf for} $j \in pendingQ$ {\bf do}\\
\> \> \> send {\em okay} to the process $j$;\\
\> \> $pendingQ := null;$\\
%\> \> {\bf endfor};\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Ricart and Agrawala's algorithm\label{fig:algricart}}
\end{figure}

\pagebreak
\newcommand{\false}{f\!alse}
\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \> $v$: array[$1$..$N$] of integer initially $\forall j:v[j]=0$;\\
\> \> $inCS$: boolean initially $\false$;\\
\> \\
\> To $request$:\\
\> \> $v[i] := v[i] + 1;$\\
\> \> send ($reques$t, $v$) to $P_0$;\\
\> \\
\> Upon $receive(token)$ from $P_0$:\\
\> \> $inCS := true;$\\
\> \\
\> To $release$:\\
\> \> send $token$ to $P_0$;\\
\> \> $inCS := \false;$\\
\> \\
\> Upon $receive(u)$: // program message\\
\> \> $v := max(v,u.v)$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A centralized algorithm for {client} processes\label{fig:client}}
\end{figure}

\pagebreak
\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_0$::\\
\> {\bf var}\\
\> \> $reqdone$: array[$1$..$N$] of integer initially $0$;\\
\> \> $reqlist$: list of ($pid, reqvector$) initially $null$;\\
\> \> $havetoken$: boolean initially $true$;\\
\> \\
%\> events:: \\
\> Upon $receive(u, request)$:\\
\> \> $append(reqlist, u)$;\\
\> \> {\bf if} $havetoken$ {\bf then} $checkreq()$;\\
\> \\
\> Upon $receive(u, token)$:\\
\> \> $ havetoken := true;$\\
\> \> $ checkreq();$\\
\> \\
\> $checkreq()$:\\
\> \> $eligible :=  \{w \in reqlist \: | \:  \forall j:j \neq w.p:w.v[j] \leq reqdone[j] \};$ \\
\> \> {\bf if} $ eligible \neq \{\}$ {\bf then} \\
\> \> \>    $w := first(eligible)$;\\
\> \> \>    $delete(reqlist,w)$;\\
\> \> \>    $reqdone[w.p] := reqdone[w.p] + 1$;\\
\> \> \>    send $token$ to $P_{w.p}$\\
\> \> \>    $havetoken := \false$;\\
\> \> {\bf endif}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A centralized algorithm for the coordinator process\label{fig:coord}}
\end{figure}


\pagebreak

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \> $v$: array[$1$..$N$] of integer initially $\forall j:v[j]=0$;\\
\> \> $inCS$: boolean initially $\false$;\\
\> \> $havetoken$: boolean initially $\false$ except for $P_0$;\\
\> \> $myreqlist$: list of ($pid, reqvector$) initially $null$;\\
\> \\
\> To $request$:\\
\> \> $v[i] := v[i] + 1;$\\
\> \> send $(request, v)$ to all processes (including itself);\\
\> \\
\> Upon $receive(request,u)$:\\
\> \> $v := max(v,u.v)$;\\
\> \> {\bf if} ($havetoken$) {\bf then} \\
\> \> \> $append(token.reqlist, u)$;\\
\> \> \> {\bf if} not $inCS$ {\bf then} $checkreq()$;\\
\> \> {\bf else} $append(myreqlist, u)$;\\
\>\\
\> $receive(u, token)$:\\
\> \> $inCS := true;$\\
\> \> $havetoken := true;$\\
%CHECK THIS
\> \> $append(token.reqlist, \{ u \: | \:  (u \in myreqlist) \wedge (u >
token.reqdone)\});$\\
\> \> $myreqlist := null;$\\
\> \\
\> $release$:\\
\> \> $inCS := \false;$\\
\> \> $checkreq()$;\\
\> \\
\> $receive(u)$: //program message\\
\> \> $v := max(v,u.v)$;\\
\\
\> $checkreq()$:\\
\> \> $eligible :=  \{w \in token.reqlist$ such that\\
\> \> \> \>   $\forall j:j \neq w.p: w.v[j] \leq token.reqdone[j] \}$; \\
\> \> {\bf if} $ eligible \neq \{\}$ {\bf then} \\
\> \> \>    $w := first(eligible)$ ;\\
\> \> \>    $delete(token.reqlist,w)$;\\
\> \> \>    $token.reqdone[w.p] := token.reqdone[w.p] + 1$;\\
\> \> \>    send $token$ to $P_{w.p}$;\\
\> \> \>    $havetoken := \false$;\\
\> \> {\bf endif}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A decentralized token-based algorithm for mutual exclusion\label{fig:suzuki}}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/conflict.eps}}
\caption{(a) Conflict graph (b) An acyclic orientation with $P_2$ and $P_4$ as sources (c) Orientation after $P_2$ and $P_4$ finish eating}
\label{fig:conflict}
\end{figure}


\newcommand{\fork}{f\!ork}
\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\>\>  $hungry, eating, thinking$: boolean;\\
\>\>  $\fork(f)$, $request(f)$,$dirty(f)$: boolean;\\
\> {initially}\\
\> \> 1. All forks are dirty.\\
\> \> 2. Every fork and request token are held by different philosophers.\\
\> \> 3. $H$ is acyclic.\\
\\
\> {To request a fork}:\\
\> \> {\bf if} $hungry$ and $request(f)$ and $\neg \fork(f)$ {\bf then} \\
\> \> \> send request token for fork $f$;\\
\> \> \> $request(f)$ := $\false$;\\
\\
\> {Releasing a fork}:\\
\> \> {\bf if} $request(f)$ and $\neg eating$ and $dirty(f)$ {\bf then} \\
\> \> \> send fork $f$;\\
\> \> \> $dirty(f)$ := $\false$;\\
\> \> \> $\fork(f)$ := $\false$;\\
\\
\> {Upon receiving a request token for fork $f$}:\\
\> \> $request(f)$ := $true$;\\
\\
\> {Upon receiving a fork $f$}:\\
\> \> $\fork(f)$ := $true$;\\
\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for dining philosophers problem \label{fig:din}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\>\>  $thirsty, drinking, tranquil$: boolean;\\
\>\>  $bot(b)$, $request(b)$,$need(b)$: boolean;\\
\>\>  {initially} \\
\> \> \> bottle and its request token are held by different philosophers.\\
\\
\> {To request a bottle $b$}:\\
\> \> {\bf if} $thirsty$, $request(b)$, $need(b)$, $\neg bot(b)$ {\bf then} \\
\> \> \> send request token for bottle $b$;\\
\> \> \> $request(b)$ := $\false$;\\
\\
\> {To release a bottle $b$}:\\
\> \> {\bf if} $request(b), bot(b)$ {\bf then}\\
\> \> \>      {\bf if} $\neg$ [ $need(b)$ and (($state$ = $drinking)$ or $\fork(f)$) ] {\bf then} \\
\> \> \> \> send bottle $b$;\\
\> \> \> \> $bot(b)$ := $\false$;\\
\\
\> {Upon receiving a request token for bottle $b$}:\\
 \> \> $request(b) := true$;\\
\\
\> {Upon receiving a bottle $b$}:\\
 \> \> $bot(b) := true$;\\
\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for drinking philosophers problem\label{fig:drinking}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \>   $myid$: integer ;\\
\> \>   $awake$: boolean initially $\false$;\\
\> \>   $leaderid$: integer initially $null$;\\
\\
\> To initiate election:\\
\> \>  send $(election, myid)$ to $P_{i-1}$;\\
\> \>        $awake := true$; \\
\\
\> Upon receiving a message $(election, j)$:\\
\> \>   {\bf if} $(j > myid)$ {\bf then}\\
\> \> \>  send $(election, j)$ to $P_{i-1}$;\\
\> \>   {\bf else if} $(j = myid)$ {\bf then}\\
\> \> \>  send $(leader, myid)$ to $P_{i-1}$;\\
\> \>   {\bf else if} $((j < myid) \wedge \neg awake)$ {\bf then}\\
\> \> \>  send $(election, myid)$ to $P_{i-1}$;\\
\> \>       $awake := true$; \\
\\
\> Upon receiving a message $(leader, j)$:\\
\> \>        $leaderid := j$; \\
\> \>    	if $(j \neq myid)$ then $send(leader,j)$ to $P_{i-1}$;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{{The leader election algorithm} at $P_i$ \label{fig:CR}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \>   $color$: $\{white, red\}$ initially $white$;\\
\> \> // assume $k$ incoming channels \\
\> \>   $chan$: array[$1$..$k$] of queues of messages initially $null$; \\
\> \>   $closed$: array[$1$..$k$] of boolean initially $\false$;\\
\> \\
\> $turn\_red()$ {\bf enabled if} $(color = white)$:\\
\> \>    save\_local\_state;\\
\> \>    $color$ := $red$;\\
\> \>      send (marker) to all neighbors;\\
\> \\
\> Upon $receive(marker)$ on incoming channel $j$:\\
\> \> {\bf if} (color = white) {\bf then} \\
\> \> \>   turn\_red();\\
\> \>  $closed[j]$ := $true$;\\
\> \\
\>  Upon $receive(program\_message)$ on incoming channel $j$:\\
\> \>   {\bf if} $(color = red) \wedge \neg closed[j]$ {\bf then} // append the message \\
\>\>  \>  $chan[j]$ := $append(chan[j], program\_message)$; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Chandy and Lamport's snapshot algorithm \label{fig:channels}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \> $G$: array[$1$..$N$] of integer initially $\forall i: G[i] := initial(i)$;\\
\\
       \> {\bf while} $\neg B(G)$ {\bf do}\\
       \>\>    Let $i$ be such that $forbidden(G,i)$;\\
       \>\>    {\bf if} ($G[i] = final(i)$) {\bf then return} $false$\\
       \>\>    {\bf else} $G[i] := next(G[i])$;\\
       \> {\bf endwhile};\\
       \> {\bf return} $true$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An efficient algorithm to detect a linear predicate\label{fig:alg}}
\end{figure}
\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
    \>{\bf var}\\
    \>\>$cut$: array[$1$..$n$] of {\bf struct} \\
    \>\>\>$v$: array[$1$..$n$] of integer; \\
    \>\>\>$color$: $\{red, green\}$;\\
    \>\> {\bf endstruct} initially $(\forall i: cut[i].color = red)$; \\
    \> \> $detect$: boolean initially $\false$;\\
    \>\\
    \>\>{\bf while} ($\exists i: (cut[i].color = red)$) {\bf do}\\
    \>\>\> {\bf if} $(q[i] = null)$ and $P_i$ terminated {\bf then return} $\false$;\\
    \>\>\>{\bf else} $cut[i].v$ := $receive(q[i])$;// advance the cut \\
    \>\>\>$paintState(i)$;\\
    \>\>{\bf endwhile};\\
    \>\\
    \>$detect$ := $true$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{WCP detection algorithm---checker process.
  \label{fig:checker-algorithm}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
    {$paintState(i)$}\\
    \>$cut[i].color$ := $green$;\\
    \>{\bf for} $j := 1$ {\bf to} $n$ {\bf do}\\
    \> \>{\bf if} $(cut[j].color = green)$ {\bf then}\\
    \> \>\>{\bf if} $(cut[i].v < cut[j].v)$ {\bf then} $cut[i].color := red$;\\
    \> \>\>{\bf else if} $(cut[j].v < cut[i].v)$ {\bf then} $cut[j].color := red$;\\
    \>{\bf endfor}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Procedure $paintState$. \label{fig:paintState}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \>  // number of questions asked for each level \\
\> \>  $num$: array[$1$..$m$] of integer initially $0$; \\
\\
\> On being asked to compare $P_i[k]$ and $P_j[l]$\\
\> \> {\bf if} $(k<l)$ {\bf then} return $P_i[k] < P_j[l]$;\\
\> \> {\bf if} $(l<k)$ {\bf then} return $P_j[l] < P_i[k]$;\\
\> \> {\bf if} $(l=k)$ {\bf then} \\
\> \> \> $num[k] := num[k] + 1$;\\
\> \> \> {\bf if} $(num[k] = n*(n-1)/2)$ {\bf then return} $P_i[k] < P_j[l]$;\\
\> \> \> {\bf else return} $P_j[l] || P_i[k];$\\
\> \> {\bf endif}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{The algorithm for the adversary \label{fig:adver}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
%\programspacing
\> {\bf var}\\
\> \> $candidate$: {\bf struct} \\
\> \> \> $myindex: 1..m$;\\
\> \> \> $depend$: list of $(pid: 1..N, stateindex: 1..m)$ ;\\
\> \> {\bf endstruct};\\
\> \> $G$: array[$1$..$N$] of stateindex initially $0$;\\
\> \> $color$: array[$1$..$N$] of $\{red, green\}$ initially $red$;\\
\> \> $q_1 \ldots q_N$: queue of $candidate$;\\
\> \> $detect$: boolean initially $\false$;\\
\\
\>\>{\bf while} ($\exists i : color[i] = red)$ {\bf do}\\
\>\>\> {\bf if} $(q[i] = null)$ and $P_i$ terminated {\bf then return} $\false$;\\
\>\>\> $candidate$ := $receive(q[i])$ ;\\
\>\>\>     {\bf if} $(candidate.myindex > G[i])$ {\bf then}\\
\>\>\>\>     $G[i] := candidate.myindex; $\\
\> \> \> \>  $color[i]:=green;$\\
\>\>\>     {\bf endif}\\
\>\>\>     {\bf for} $(j,k) \in candidate.depend$  {\bf do}\\
\>\>\>\>      {\bf if} $( k > G[j])$ {\bf then}\\
\>\>\>\>\>        $G[j]$ := $k$;\\
\>\>\>\>\>        $color[j]$ := $red$;\\
\>\>\>\>      {\bf endif} \\
\>\>\>     {\bf endfor}\\
\>\>   {\bf endwhile}\\
\\
\> detect:=true;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Checker process algorithm \label{f:monitor-wcp}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\>  {\bf var}\\
\> \>  // vector clock from the candidate state\\
\> \>  $candidate$: array[$1$..$n$] of integer initially $0$; \\
\\
\>   Upon receiving the token $(G,color)$ \\
\>  \>    {\bf while} $(color[i] = red)$ {\bf do}\\
\> \> \>  receive $candidate$ from application process $P_i$;\\
\> \> \>      {\bf if} $(candidate[i] > G[i])$ {\bf then}\\
\> \> \> \>      $G[i] := candidate[i]$;\\ 
\> \> \> \>      $color[i]:=green;$\\
\> \> \>      {\bf endif};\\
\> \>    {\bf endwhile};\\
\> \>      {\bf for} $j := 1$ {\bf to } $n$, $(j \neq i)$  {\bf do}\\
%\> \> \>       {\bf if} $(candidate[j] > G[j])$ {\bf then}\\
\> \> \>       {\bf if} $(candidate[j] \geq G[j])$ {\bf then}\\
\> \> \> \>         $G[j] := candidate[j]$;\\
\> \> \> \>         $color[j] := red$;\\
\> \> \>       {\bf endif} \\
\> \>      {\bf endfor}\\
\> \>      {\bf if} ($\exists j: color[j] = red)$ {\bf then} send token
to $M_j$;\\
\> \>      {\bf else} $detect := true$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Monitor process algorithm \label{f:monitor-dwcp}}
\end{figure}



\begin{figure}[thb]
\centerline{\epsfbox{figs/non-friendly.eps}}
\caption{The set of cuts satisfying the predicate is
  not a sublattice.} 
\label{f:example}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}								\\
\>\> $incsend, increcv$: {\bf list} of messages	initially $\emptyset$;\\
\>\>  $v$: vectorClock;\\
\>\>    $newinterval$: boolean initially $true$;	\\
									\\
\> To send $m$: 						\\
\>\>  $newinterval:=true$;							\\
\>\>  $incsend:= append(incsend, m)$; \\
									\\
\> Upon receive($m$): \\
\>\>  $newinterval:=true$;							\\
\>\>  $increcv:= append(increcv, m)$;\\
									\\
\> Upon $(local\_pred = true \wedge newinterval)$:\\
\>\>  $newinterval := \false$;						\\
\>\>  $send (v, incsend, increcv)$ to the checker process; 	\\
\>\>  $incsend:= \emptyset; increcv:=\emptyset$;					
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Application process algorithm for $P_i$ \label{f:application}}
%\caption{The vector algorithm. \label{f:vector}}			
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}								\\
\>    \>$S$, $R$: array[$1..n,1..n]$ of {\em list} of messages initially $null$;\\
\>    \>$CP$: array [$1..n,1..n$] of \{$F_s$, $F_r$, $T$\};\\
    \>\>$cut$: array[$1$..$n$] of {\bf struct} \\
    \>\>\>$v$: array[$1$..$n$] of integer; \\
    \>\>\>$color$: $\{red, green\}$;\\
\>    \>\>incsend, increcv : list of messages \\
    \>\> {\bf endstruct} initially $(\forall i: cut[i].color = red)$; \\
    \> \> $detect$: boolean initially $\false$;\\
    \>\\
    \>{\bf while} ($\exists i: (cut[i].color = red)$) {\bf do}\\
    \>\> {\bf if} $(q[i] = null)$ and $P_i$ terminated {\bf then return;} \\
    \>\>{\bf else} $cut[i].v$ := $receive(q[i])$;// advance the cut \\
    \>\>$paintState(i)$;\\
    \>\>update-channels(i);\\
    \>{\bf endwhile};\\
    \>\\
    \>$detect$ := $true$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{GCP detection algorithm---checker process}
  \label{fig:gchecker-algorithm}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
    ${update\_channels(i)}$\\
    \\
    \>{\bf for} all message $m \in incsend$ {\bf do}\\
    \>\>$P_j := destination(m)$;\\
    \>\>{\bf if} $(m \in R[i,j])$ {\bf then} $R[i,j] := R[i,j] - \{m\}$;\\
    \>\>{\bf else} $S[i,j] := S[i,j] \cup \{m\}$;\\
    \>\>$CP[i,j] := chanp_{ij}(S[i,j])$;\\
    \>\>{\bf if} $(CP[i,j] = F_s)$ {\bf then} $cut[j].color := red$;\\
    \>\>{\bf else if} $(CP[i,j] = F_r)$ {\bf then} $cut[i].color := red$;\\
    \>{\bf endfor}\\
    \\
    \>{\bf for} all message $m \in increcv$ {\bf do}\\
    \>\>$P_j := source(m)$;\\
    \>\>{\bf if} $(m \in S[j,i])$ {\bf then} $S[j,i] := S[j,i] - \{m\}$;\\
    \>\>{\bf else} $R[j,i] := R[j,i] \cup \{m\}$;\\
    \>\>$CP[j,i] = chanp_{ji}(S[j,i])$;\\
    \>\>{\bf if} $(CP[j,i] = F_s)$ {\bf then} $cut[i].color := red$;\\
    \>\>{\bf else if} $(CP[j,i] = F_r)$ {\bf then} $cut[j].color := red$;\\
    \>{\bf endfor}\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Procedure $update\_channels$}
  \label{fig:update-channels}
\end{figure}



\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \>   $state: \{passive, active\}$ initially $passive$ except for environment;\\
\> \>   $D$: integer initially $0$;\\
\> \>   $parent$: process id initially $null$;\\
\\
\> Upon receiving a message from $P_j$:\\
\> \>   {\bf if} $(parent=null)$ {\bf then} \\
\> \> \>        $parent := P_j;$\\
\> \> \>        $state := active;$\\
\> \>   {\bf else} send signal to $P_j$;\\
\\
\> Upon receiving a signal:\\
\> \>   $D := D - 1$;\\
\\
\> To send a message ({\bf enabled if} $(state = active)$):\\
\> \>   $D := D + 1$;\\
\\
\> on $(state = passive) \wedge (D=0) \wedge (parent \neq null)$:\\
\> \>   send signal to $parent$;\\
\> \>   $parent := null$;\\
\\
\> environment detects termination when $(D = 0)$.\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Termination detection algorithm \label{fig:DS}}
\end{figure}

\begin{figure}
\centerline{\ \epsfbox{figs/Figure2.eps}}
\caption{Transformation for NP-completeness proof of SGSD problem\label{fig:npc}}
\end{figure}


\begin{figure}[ht]
\centerline{\ \epsfbox{figs/Figure3.ps}}
\caption{Overlapping intervals \label{fig:overlap}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
  \begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var }\\
\> \>  $m$:array[$1$..$N$, $1$..$N$] of integer initially $\forall j,k:m[j,k] = 0$;\\
\> \\
\> $(s,send,t)$ to $P_j$:\\
\> \> $t.m := s.m;$\\
\> \> $t.m[i,j] := t.m[i,j]+1$;\\
\> \\
\> $(s, recv(u),t)$: {\bf enabled if} $\forall k: s.m[k,i] \geq u.m[k,i]$\\
\> \> $t.m := max(s.m, u.m)$;\\
\> \> $t.m[u.p,i] := t.m[u.p,i] + 1;$
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for causal ordering of messages\label{fig:causal} at $P_i$}
\end{figure}

\begin{figure}[htbp]
\vspace*{0.8in}
\begin{center}
\input{figs/issynch}
\end{center}
\vspace*{0.8in}
\caption{A computation that is synchronously ordered\label{fig:issynch}}
\end{figure}


\begin{figure}[htbp]
\begin{center}
\input{figs/nosynch}
\end{center}
\caption{A computation that is not synchronously ordered\label{fig:nosynch}}
\end{figure}



\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxxx\=xxxxx\=xxxxx\=xxxxxxxx \kill \\
$P_i::$ \\
\>{\bf var} \\
\>\> $state : \{active, passive\}$ initially $active$; \\
\\
\> To {send} $m$ to $P_j$, $(j < i)$\\
\> \> {\bf enabled if} $(state = active)$:\\
\>\> {send} $m$ to $P_j$  \\
\>\> $state := passive$; \\
\\
\>Upon {receive} $m$ from $P_j$, $(j > i)$\\
\> \> {\bf enabled if} $(state = active)$:\\
\>\>\> {send} $ack$ to $P_j$; \\
\\
\> Upon {receive} {$ack$}:\\
\>\> $state := active$; \\
\\
\> To {send} a message $(message\_id, m)$ to $P_j$, $(j > i)$\\
\>\> {send} {$request(message\_id)$} to $P_j$;  \\
\\
\>Upon {receive} {$request(message\_id)$} from $P_j$, $(j < i)$\\
\> \> {\bf enabled if} $(state = active)$:\\
\>\> {send} {$permission(message\_id)$} to $P_j$ \\
\>\> $state := passive$; \\
\\
\>Upon {receive} {$permission(message\_id)$} from $P_j$, $(j > i)$\\
\> \> {\bf enabled if} $(state = active)$:\\
\>\> {send} $m$ to $P_j$; \\
\\
\>Upon {receive} $m$ from $P_j$, $(j < i)$ \\
\>\> $state := active$; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{The algorithm at $P_i$ for synchronous ordering of messages}
\label{fig:synchalg}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \>   $parent$: process id;// initialized based on the \inx{spanning tree} \\
\> \>   $numchildren$: integer; // initialized based on the spanning tree \\
\> \>   $numreports$: integer initially $0$;\\
\\
\> on receiving a report from $P_j$\\
\> \> $numreports := numreports + 1;$\\
\> \>   {\bf if} $(numreports =numchildren)$ {\bf then} \\
\> \> \>   {\bf if} $(parent=null)$ {\bf then} // root node \\
\> \> \> \>   compute global function;\\
\> \> \>   {\bf else} send report to $parent$;\\
\> \>   {\bf endif};\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A convergecast algorithm \label{fig:converge}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_{root}::$\\
\>   send $m$ to all children; \\
\\
$P_{i}::i \neq root$\\
\> on receiving a message $m$ from $parent$\\
\> \>   send $m$ to all children; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A broadcast algorithm \label{fig:broadcast}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \>   $parent$: process id initially $null$;\\
\> \>   $numchildren$: integer initially $0$;\\
\> \>   $childrenlist$: list initially $null$;\\
\> \>   $numneighbors$: integer initially the number of neighbors;\\
\> \>   $numreports$: integer initially $0$;\\
\> \>   $notdone$: boolean initially $true$ except for the root;\\
\\
\> Upon receiving a message $m$ from $P_j$\\
\> \>        {\bf if}  $notdone$ {\bf then}\\
\> \> \>        $parent = P_j;$\\
\> \> \>        $notdone := \false;$\\
\> \> \>        send $m$ to all neighbors except $P_j$;\\
\> \> \>        send {\em (parent)} to $P_j$;\\
\> \>        {\bf else}\\
\> \> \>        send {\em (reject)} to $P_j$;\\
\\
\> Upon receiving a {\em (parent)} message\\
\> \>   $numchildren := numchildren + 1$;\\
\> \>   $append(childrenlist, P_j)$;\\
\> \>   $numreports := numreports + 1;$\\
\> \>  {\bf if}  $(numreports = numneighbors - 1)$ {\bf then} halt;\\
\\
\> Upon receiving a {\em (reject)} message\\
\> \>   $numreports := numreports + 1;$\\
\> \>  {\bf if}  $(numreports = numneighbors - 1)$ {\bf then} halt;
\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A spanning tree construction algorithm \label{fig:spanning}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxxx\=xxxxx\=xxxxx\=xxxxx\= \kill \\
\> {\bf var}\\
\> \> $d$: integer initially $0$; \\
\> \> $\inf$: set of information initially  \{ identity of the node \}; \\
\> \> $sent(c)$: information initially $\inf$ for all $c$\\
\\
\> {\bf while} $d < D$ {\bf do} \\
        \> \> $d := d + 1$; \\
        \> \> send$\langle \mbox{sent} (c) \rangle$ on all channels $c$; \\
        \> \> $new$ \la $\phi$; \\
        \> \> {\bf for} every channel $c$ {\bf do} \\
        \> \> \> receive $\langle \mbox{ received}(c) \rangle$ on $c$; \\
        \> \> \> {\bf for} $y \in  received(c) - \inf - new$ {\bf do}\\
         \> \> \> \>          $route(c) \la route(c) \cup \{y\}$; \\
        \> \> \> $new$ \la $new \cup (received(c) - \inf)$; \\
        \> \> {\bf endfor}\\
	\> \> $\inf$ \la $\inf \cup new$; \\
        \> \> $sent(c)$ \la $new - received(c)$;\\
\> {\bf endwhile};\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{An algorithm to compute the routing tables
  \label{fig:globcomp1}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxxx\=xxxxx\=xxxxx\=xxxxx\= \kill \\
\> {\bf var}\\
\> \> $d$: integer initially $0$; \\
\> \> $\inf, new$: set of information initially  \{ initial data \}; \\
\> \> $sent(c)$: information initially $\inf$ for all $c$\\
\> \> $open$: set of channels initially $all$;\\
\> \> $received(c)$: information initially $\forall c : received(c)  = \phi$\\
\\
\> {\bf while} $open$ $\not= \phi$ {\bf do} \\
        \> \> $d := d + 1$; \\
        \> \> {\bf for} $c \in $ $open$ {\bf do} \\
        \> \> \> $sent(c) \la new - received(c)$; \\
        \> \> \> send $\langle {sent} (c) \rangle$ on $c$; \\
        \> \> {\bf endfor}\\
	\> \> $new \la \phi$; \\
        \> \> {\bf for} $c \in $ $open$ {\bf do} \\
        \> \> \> receive $\langle \mbox{received}(c) \rangle$ on $c$; \\
        \> \> \> {\bf if} $(received(c) = sent(c))$ {\bf then} $open$ \la $open$ $- \{c\}$; \\
        \> \> \> $new \la new \cup (received(c) - \inf)$; \\
        \> \> \> compute problem specific information; \\
	\> \> {\bf endfor};\\
        \> \> $\inf \la \inf \cup new$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{An algorithm to compute a general global function
  \label{fig:globcomp2}}
\end{figure}


\begin{figure}
\begin{center}
\begin{tabular}{| l l l l |}
\hline
Time & Message 1 & Message 2 & Idle \\ \hline
0 & 1,3 $\rightarrow$ 2 & 5,7 $\rightarrow$ 6 & 4 \\
1 & 2,6 $\rightarrow$ 4 & 1,3 $\rightarrow$ 5 & 7 \\
2 & 4,5 $\rightarrow$ 7 & 2,6 $\rightarrow$ 1 & 3 \\
3 & 7,1 $\rightarrow$ 3 & 4,5 $\rightarrow$ 2 & 6 \\ \hline
\end{tabular}
\end{center}

\caption{A message sequence for repeated computation of a function\label{fig:mseq1}}
\end{figure}


\begin{figure}[htbp]
%\centerline{\psfig{figure=figs/ffig2.clean,bbllx=0.5in,bblly=7.75in,bburx=4.1in,bbury=10.75in}}
%\vspace*{3.5in}
%\input{figs/overlapFig.latex}
%\hspace*{0.5in}
\centerline{\epsfbox{figs/overlapFig.eps}}
\caption{Overlapping trees that determine message sequences\label{fig:rev}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
xx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf function} next($x$)::\\
\>\> // Type I move \\
\>\> {\bf if} $(even (x))$ {\bf then} \\
\>\> \> $x' := x/2$;\\
\>\> \\
\>\> // Type II move \\
\>\> {\bf if} $(odd(x) \wedge ( x < 2^{n-1}))$ {\bf then}\\
\>\> \>  $x' := x * 2^{lead0(x)}+1$;\\
\>\> \\
\>\> // Type III move \\
\>\> {\bf if} $(odd(x) \wedge ( x > 2^{n-1}))$ {\bf then}\\
\>\> \>  $x' := (x + 1)$ ;\\
\>\> \> {\bf if}~$(x' = N+1)$~ {\bf then}~  $x':= x'/2$;\\
\>\> {\bf endif};\\
\>\> \\
\>\> {\bf return}($x'$);
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{The function $next$ \label{fig:funcnext}}
\end{figure}



\begin{figure}[htbp]
\centerline{\epsfbox{figs/nodegroup.eps}}
%\centerline{\psfig{figure=figs/ffig3.clean,bbllx=0.5in,bblly=7.75in,bburx=4.1in,bbury=10.75in}}
%\vspace*{2.5in}
\caption{Node groups and transitions\label{fig:groups}}
\end{figure}



\begin{figure*}[t]
%\centerline{\epsfbox{figures/fig2.ps}}
%\centerline{\psfig{figure=figs/ffig4.clean,bbllx=0.5in,bblly=6.75in,bburx=7.1in,bbury=10.75in}}
%\vspace*{2.5in}
\begin{center}
\input{figs/implementation2Fig.latex}
\end{center}
\caption{Node labels generated by {\em next}.
Original in-order labels are shown inside the nodes.
\label{fig:next}}
\end{figure*}



\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\ 
\> \>  $knownbound, mymin, hismin$: real;\\
\> \>  $step, numsteps, dest$: integer;\\
\\
\>  Initialization;\\
\>  $knownbound := \infty$;\\
\>  {\bf for} $step:=0$ {\bf to} $numsteps$ {\bf do}\\
\>\>    $mymin := search(knownbound)$;\\
\>\>    $dest = tosend(i, step)$;\\
\>\>    {\bf if} ($dest \neq -1$) {\bf then}\\
\>\>\>       $send(dest, mymin)$;\\
\>\>    {\bf else} {\bf begin}\\
\>\>\>       $receive(torec(i, step), hismin)$;\\
\>\>\>       $knownbound := min(mymin, hismin)$;\\
\>\>    {\bf end}; \\
\>  {\bf endfor};\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Distributed branch-and-bound algorithm\label{fig:branch}}
\end{figure}



\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> \> $pulse$: integer initially $0$;\\
\\
\> round $i$ :\\
\> \>     $pulse := pulse + 1$;\\
\> \>   simulate the round $i$ of the synchronous algorithm;\\
\> \>   send messages to all neighbors with $pulse$;\\
\> \>   wait for exactly one message from each neighbors with $(pulse = i)$;\\

%\vspace{-8mm}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{The implementation of a simple synchronizer\label{fig:simple-synch} at $P_j$}
\end{figure}


\begin{figure}[htbp]
%\centerline{\includegraphics[width=5.5in]{figs/motivation1.eps}}
\centerline{\epsfbox{figs/motivation1.eps}}
\caption{\label{fig:motivation1} (a) A computation and (b) its slice with
respect to $(x_1 \geq 1) \wedge (x_3 \leq 3)$.}
\end{figure}


\begin{figure}[t]
%\centerline{\includegraphics[height=5.50cm]{join}}
\centerline{\epsfbox{figs/myjoin.eps}}
\caption{\label{joinIrreducible} (a) An example of a distributive lattice
(b) its partial order representation.}
\end{figure}


\begin{figure}[htbp]
%\centerline{\includegraphics[height=17.0cm]{sublattice}}
%\centerline{\epsfbox{figs/mysublattice.eps}}
\centerline{\epsfbox{figs/sublattice.eps}}
\caption{\label{slice} (a) A computation, (b) its lattice, (c) a
sublattice, and (d) the corresponding slice.}
\end{figure}


\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {0.98 \textwidth}\sf
\begin{center}\begin{minipage}{0.95 \textwidth}

~

~

\underline{Input}: A Computation $(E, \ra)$ and a regular predicate
$B$\\

\underline{Output}: A computation slice $(I_B, F, \ra_B)$ such that 
(1) Every consistent cut of $F$ is also a consistent cut of $E$
(2) All consistent cuts of $F$ satisfy $B$
(3) All consistent cuts of $E$ that satisfy $B$ are also consistent cuts of $F$.

\begin{itemize}
\item 
Step 1. Let $V$ be the least consistent cut in $E$ that satisfies $B$.
Since $B$ is a regular predicate it is linear and hence $V$ can
be determined, if it exists.
If no such cut exists, output ``B not possible''.
\item 
Step 2. Let $W$ be the greatest consistent cut in $E$ that satisfies $B$.
% \item
% Step 3. If $V=W$, then output ``B possible only in the cut $V$''
\item
Step 3. For each event $e \in W-V$, compute the least consistent cut
in $E$ that satisfies $B$ and includes $e$. Call that cut $J(e)$.
\item
Step 4. Let $R$ be an equivalence  relation defined on events in $W - V$ as follows:

\[ (e,f) \in R \: \equiv \: J(e) = J(f) \]

Let the equivalence classes induced by $R$ be $C_i$, $1 \leq i \leq
m$. For a class $C$, let $J(C)$ be $J(e)$ for some event $e$ in
$C$. Output $(V,F,\ra_B)$, where
 
\[ F := \{ C_i \: | \: 1 \leq i \leq m \} \] 
\[  \ra_B := \{ (C_i,C_j) \: | \:  J(C_i) \subseteq J(C_j) \wedge J(C_i) \neq J(C_j) \} \] 

~
\end{itemize} 
\end{minipage} \end{center} 
\end{minipage} 
} % end \fbox

\end{center}

\caption{An algorithm to construct the slice \label{fig:algo}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P$::\\
\> Upon $read(x)$:\\
\> \>     generate $Ok(v)$ where $v$ is the value of $P$'s copy of $x$;\\
\\
\> Upon $write(x,v)$:\\
\> \>      totally-ordered-broadcast $(x,v)$;\\
     \\
\> Upon receive of totally-ordered-broadcast$(x,v)$ from $Q$:\\
\> \>       set local copy of $x$ to $v$;\\
\> \>       {\bf if} $P=Q$ {\bf then} generate $Ok()$ for $write(x,v)$;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Sequential consistency: local read algorithm
  \label{fig:localread}}
\end{figure}


\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P$::\\
\> Upon $read(x)$:\\
\> \>     {\bf if} $(num=0)$ {\bf then}\\
\> \> \>     generate $Ok(v)$ where $v$ is the value of $P$'s copy of $x$;\\
\\
\> Upon $write(x,v)$:\\
\> \>      $num := num + 1$;\\
\> \>      totally-ordered-broadcast$(x,v)$;\\
\> \>      generate $Ok()$ for write;\\
     \\
\> Upon receive of totally-ordered-broadcast $(x,v)$ from $Q$:\\
\> \>       set local copy of $x$ to $v$;\\
\> \>       {\bf if} $(P=Q)$ {\bf then} \\
\>\>  \>           $num := num - 1$;\\
\>\>  \>           {\bf if} $(num = 0)$ {\bf then}\\
\>\>\>   \> 		generate $OK(v)$ where $v$ is the value of $P$'s copy of $x$;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Sequential consistency: local write algorithm
  \label{fig:localwrite}}
\end{figure}


\begin{figure}
\begin{tabular}{|l |l | l|}
\hline
{\bf Consistency} & {\bf Legal History}  & {\bf Order Preserved}\\
\hline
Linearizability & Global & Occurred before order \\
Normality (Problem \ref{exer:norm}) & Global & Process, object order\\
Sequential & Global & Process order \\
Causal & Per process & Process, object order \\
FIFO (Problem \ref{exer:FIFO}) & Per process & Process order \\
\hline
\end{tabular}
\caption{Summary of consistency conditions}
\label{tbl:consist}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> Bottom:\\
\> \> {\bf if} $(L=S)$ {\bf then} $S := S+1~ mod~ K$ ; \\
\\
\> For other machines:\\
\> \> {\bf if} $(L \neq S)$ {\bf then} $S := L$ ;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{$K$-state self-stabilizing algorithm \label{fig:kstate}}
\end{figure}

\begin{figure}[htb]\begin{center}
\input{figs/kstateFig.latex}
\kstate{2}{3}{4}{4}{2}{2}
\hspace*{1.3in}
\kstate{3}{3}{4}{4}{2}{2} 
\end{center}
\caption{A move by the bottom machine in the $K$-state algorithm \label{fig:kstateExample}}
\end{figure}


\begin{figure}[htb]\begin{center}
\input{figs/kstateFig.latex}
\kstate{3}{3}{4}{4}{4}{2} 
\hspace*{1.3in}
\kstate{3}{3}{4}{4}{4}{4} 
\end{center}
\caption{A move by a normal machine in the $K$-state algorithm \label{fig:kstateExampleB}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
Bottom:\\
\> {\bf if} $(B+1=R)$ {\bf then} $B:=B+2$;\\
\\
Normal:\\
 \> {\bf if} $(L=S+1)$ or $(R=S+1)$ {\bf then} $S:=S+1$;\\
\\
Top:\\
 \> {\bf if} $(L=B)$ and $(T \neq B+1)$ {\bf then} $T:=B+1$;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Three-state self-stabilizing algorithm \label{fig:3state}}
\end{figure}

\def\3state#1#2#3#4#5#6#7{
\setlength{\unitlength}{0.012500in}%
%
\begin{picture}(301,65)(115,590)
\thinlines
%\Large
\put(120,620){\line( 1, 0){300}}

\put(120,620){\circle*{12}}
\put(220,620){\circle*{12}}
\put(320,620){\circle*{12}}
\put(420,620){\circle*{12}}

\put(120,590){\makebox(0,0)[b]{B}}
\put(420,595){\makebox(0,0)[b]{T}}

\put(120,640){\makebox(0,0)[b]{#1}}
\put(220,640){\makebox(0,0)[b]{#2}}
\put(320,640){\makebox(0,0)[b]{#3}}
\put(420,640){\makebox(0,0)[b]{#4}}

\put(170,640){\makebox(0,0)[b]{#5}}
\put(270,640){\makebox(0,0)[b]{#6}}
\put(370,640){\makebox(0,0)[b]{#7}}

\end{picture}
}

\def\mla{$\leftarrow$}
\def\mra{$\rightarrow$}

\begin{figure}[htb]\begin{center}
\3state{1}{0}{2}{0}{\mra}{\mra}{\mla}

\vspace*{0.5in}

\3state{1}{1}{2}{0}{ }{\mla}{\mla}

\vspace*{0.5in}

\3state{1}{2}{2}{0}{\mla}{}{\mla}
\end{center}
\caption{A sample execution of the Three-state self-stabilizing algorithm \label{fig:3stateExample}}
\end{figure}


\begin{figure}[thbp]
\begin{center}
\begin{tabular}{|l | l|}
\hline
$p$ & A process\\
$G$ & A group of processes\\
$b$ & A predicate \\
$K_i(b)$ & Process $i$ in the group knows $b$\\
$S(b)$ & Someone in the group knows $b$\\
$E(b)$ & Everyone in the group knows $b$\\
$C(b)$ & $b$ is common knowledge in the group\\
$X$ & Set of all system computations\\
$[P]$ & Isomorphism relation on $X$\\
$x \models b$ & $b$ is true at computation $x$\\
\hline
\end{tabular}
\caption{ \label{tbl:knowledge} Notation}
\end{center}
\end{figure}

\begin{figure}[thbp]
\begin{center}
\begin{tabular}{|l | l|}
\hline
$G,H,J,K$& Global states of the system\\
$X,Y,Z$& Initial global states \\
$G[i]$& State of process $i$ in the global state $G$\\
$G \leq H$& H reachable from G\\
${\cal G},{\cal H}$& Set of global states \\
$s$& Sequence of events\\
$s(G)$& Global state resulting from application of $s$ to $G$.\\
$proc(s)$& Set of processes on which events in $s$ are defined.\\
% confusion about sequences of events vs sequences of states
\hline
\end{tabular}
\caption{ \label{tbl:flp} Notation}
\end{center}
\end{figure}

\begin{figure}[htbp]
\centerline{\epsfbox{figs/flp2.eps}}
\caption{(a) Commutativity of disjoint events (b) Asynchrony of messages\label{fig:flp-assumptions}}
\end{figure}

%TODO  figure needs to change
\begin{figure}[htbp]
\centerline{\epsfbox{figs/flp1.eps}}
\caption{(a) Case 1: $proc(e) \neq proc(f)$ (b) Case 2: $proc(e) = proc(f)$ \label{fig:flp-proof}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> \>   $V$: set of values initially $\{v_i\}$;\\
\\
\>   {\bf for} $k:=1$ to $f+1$ {\bf do}\\
\> \>     send \{$v \in V \: | \: P_i$ has not already sent $v$\} to all; \\
\> \>     receive $S_j$ from all processes $P_j, j \neq i$;\\
\> \>         $V := V \cup S_j;$ \\
\>   {\bf endfor}; \\
\\
\>     $y:=min(V)$; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Algorithm at $P_i$ for consensus under crash failures
  \label{fig:syn-crash}}
\end{figure}



\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
\> {\bf var}\\
\> \>   $V$: set of values initially $\{v_i\}$\\
\> \>   $decided$: boolean initially $false$;\\
\> \>   $\faulty$: set of indices initially $\{\}$;\\
\\
\> Phase I:\\
\>   {\bf for} $k:=1$ to  $f+1$ {\bf do}\\
\> \>     send \{$v \in V \: | \: P_i$ has not already sent $v$\} to all \\
\> \>     receive $S_j$ from all processes $P_j, j \neq i$\\
\> \>         $V := V \cup S_j;$ \\
\> \>     {\bf if} $(k=f+1)$ {\bf then} \\
\> \> \> $y:=min(V)$; \\
\> \> \>  halt; \\
\> \>     {\bf endif};\\
\> \>\\
\> \>    $\faulty$ := $\faulty \cup \{j \: | \: P_i$ did not receive any value from $P_j$ and\\
\> \> \>                         $P_j$ has not informed $P_i$ that it has decided\}\\
\> \>     {\bf if} ($|\faulty| < k$) {\bf then} \\
 \> \> \> $decided$ := $true$; \\
 \> \> \> {\bf goto} phase II; \\
\> \>     {\bf endif};\\
\>      {\bf endfor};\\
\\
\> Phase II:\\
\>   send \{$v \in V \: | \: P_i$ has not already sent $v$\} and ``I have decided'' to all\\
\>   $y:=min(V)$;\\
\>   halt;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{Early stopping algorithm for crash failures
  \label{fig:early-stopping}}
\end{figure}


\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
{\bf var}\\
\> $V$: array[1..$N$] of values\\
\> \> \>  initially $(V[i] = x) \wedge \forall j:j \neq i: V[j] = v_\bot$\\
\\
\> {\bf for} $k:=1$ {\bf to} $f+1$ {\bf do} \\
\\
\> \> first phase :\\
\> \> \>    send $V[i]$ to all other processors;\\
\> \> \>    set $V[j]$, ($j \neq i$) to the value received from $P_j$;\\
\> \> \>    $myvalue$ := majority value in the vector $V$ ($v_\bot$ if no majority);\\
\\
\> \> second phase:\\
\> \> \>  {\bf if} $(k = i)$ {\bf then} \\
\> \> \> \>   send $myvalue$ to all other processors;\\
\> \> \>   receive $kingvalue$ from $P_{k}$;\\
\> \> \>  {\bf if} $V$ vector has more than $N/2 + f$ copies of $myvalue$ {\bf then}\\
\> \> \> \> $V[i] := myvalue$; \\
\> \> \>  {\bf else} $V[i] := kingvalue$;\\
\\
\> {\bf endfor};\\
\\
\>  $y := V[i]$;\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
  \caption{An algorithm for Byzantine General Agreement at $P_i$
  \label{fig:king}}
\end{figure}


\begin{figure}[thbp]
\begin{center}
\begin{tabular}{|l | l| l|}
\hline

Name & Symbol & Accuracy Property \\
\hline
Perfect & {\cal P} & Strong \\
Strong & {\cal S} & Weak \\
Eventually perfect & $\diap$ & Eventually strong \\
Eventually strong & $\dias$ & Eventually weak \\
\hline
\end{tabular}
\caption{ \label{tbl:fd} Failure detectors with strong completeness property}
\end{center}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\>\>  $ES.suspects$: set  of processes initially $EW.suspects$;\\
\\
\> (I1) send $EW.suspects$ to all processes infinitely often;\\
\\
\> (I2) On receiving $m.suspects$ from $P_i$;\\
\>\>      $ES.suspects := ES.suspects \cup m.suspects - \{ i \}$;\\
%\vspace{-8mm}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Implementation of a $\dias$ detector using a $\diaw$ detector\label{fig:ew2es}}
\end{figure}

\begin{figure}[htbp]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
{$p$::}\\
\> {\bf var}\\
\> \> $v$ := input bit;\\
\> \> $r$ := 0; // round number \\
\> \> $t$ := 0;// timestamp\\
\\
\> {\bf while} undecided {\bf do}\\
\> \> $r := r+1$;\\
\> \> $c$ := ($r$ mod $n$) + $1$;// coordinator\\
\\
\> \> //{phase 1}:\\
\> \>    send ($p, r, v, t$) to $c$;\\
\\
\> \> // {phase 2}:\\
\> \>    $c$ waits for first $n/2+1$ estimates;\\
\> \>    $c$ chooses the estimate $w$ with the largest timestamp;\\
\> \>    $c$ proposes that value as $(c,r,w)$;\\
\\
\> \> // {phase 3}:\\
\> \>     $p$ waits for a message or failure suspicion of $c$;\\
\> \>     {\bf if} proposal $(c,r,w)$ is received {\bf then}\\
\> \> \>        $v := w$; $t := r$;\\
\> \> \>        send $(r,ACK)$ to $c$;\\
\> \>     {\bf else}\\
\> \> \>        send $(r,NACK)$ to $c$;\\
\\
\> \> // { phase 4}:\\
\> \>     $c$ waits for $n/2+1$ ACK/NACK messages;\\
\> \>     {\bf if} there are $n/2+1$ ACK messages {\bf then}\\
\> \> \>          $c$ sends $(decide,w)$ to all including itself;\\
\> {\bf endwhile};\\
\\
\\
\> { Upon receiving} $(decide,w)$\\
\> \>     $p$ sends $(decide,w)$ to all;\\
\> \>     $p$ decides on $w$ and halts.
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Consensus using $\dias$ detector}
%\caption{consensus using eventually strong failure detector}
\label{fig:consensus}
\end{figure}
\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\>\>  $IO.suspects$: set  of processes initially $EW.suspects$;\\
\\
\> (I1) send ``alive''  to all processes infinitely often;\\
\\
\> (I2) Upon receiving ``alive'' from $P_i$;\\
\> \>      $IO.suspects := EW.suspects - \{ i \}$;
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Implementation of an IO detector using a $\diaw$ detector\label{fig:es2io}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> \> $IO.suspects$ : set of processes initially $\emptyset$;\\
\> \> $timeout$: array[1..N] of integer initially t;\\
\> \> $watch$: timer initially set to $timeout$;\\
\\
\\
\> (A1) send ``alive''  to all processes after every $t$ units;\\
\\
\> (A2) Upon receiving ``alive'' from $P_i$;\\
\> \>       {\bf if} $i \in IO.suspects$ {\bf then}\\
\> \> \>        $IO.suspects := IO.suspects - \{ i \}$;\\
\> \> \>        $timeout[i] := timeout[i] + 1$;\\
\> \>       {\bf endif};\\
\> \>      Set $watch[i]$ timer for $timeout$;\\
\\
\> (A3) Upon expiry of watch[i]\\
\> \>      $IO.suspects := IO.suspects \cup \{ i \}$;\\
%\vspace{-8mm}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{Implementation of an IO detector\label{fig:io}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_j$::\\
\> {\bf var}\\
\> $RUP.suspects$: set of processes initially $\emptyset$;\\
\\
\> (B1) infinitely often broadcast a query message to all processes;\\
\\
\> (B2) Upon expiry of $timeout[i]$ time units \\
\> \>       {\bf if} ($P_i $ did not respond to the query) {\bf then}\\
\> \> \>       $RUP.suspects$ := $RUP.suspects \cup \{i\}$;\\
\> \>       {\bf else} $RUP.suspects$ := $RUP.suspects - \{i\}$;\\
\\
\> (B3) Upon receiving a query from $P_i$\\
\> \>        send ``I am alive'' to $P_i$\\
\\
%\vspace{-8mm}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{A detector that does not satisfy IO accuracy \label{fig:rup}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$:\\
\> {\bf var}\\
\> $token$: boolean; initially $\false$ for all $i \neq 1$ and $true$ for $i=1$.\\
\> // false represents absence of the token \\
\\
\> $suspected$: array[$1..N$] of boolean; // set by the failure detector \\
\\
\> Upon change from unsuspicion to suspicion of any process \\
\> \>      {\bf if} $\forall j < i: suspected[j]$ {\bf then}\\
\> \>      // is there any smaller process that is unsuspected \\
\> \> \>           $token := true ;$ // generate the token \\
\\
\> Upon change from suspicion to unsuspicion of $P_k$ \\
\>   {\bf if} $(k < i)$ {\bf then}\\
\> \>      $token := \false;$\\
\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for the alive token problem \label{fig:alive}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$:\\
\>{\bf var}\\
\>\> $ticket$: array[$1..N$] of (integer,integer) initially $\forall i: ticket[i] = (0,i)$\\
\>\> $suspected$: array[$1..N$] of boolean; // set by the failure detector \\
\\
\> (R1) Upon change from unsuspicion to suspicion of any process $P_k$\\
\>\> send ``suspected'' to $P_k$\\
\\
\> (R2) Upon receiving ``suspected''\\
\>\> {\bf if} $token(i)$ {\bf then} \\
\>\>\> $ticket[i] := Lamport's\_logical\_clock;$\\
\>\>\>   send ``slow'', $i$, $ticket[i]$ to all processes; \\
\\
\> (R3) Upon receiving ``slow'',$k,t$ \\
\>\> $ticket[k] := t;$\\
\\

$token(i) \equiv  (\forall j \neq i: suspected[j] \vee (ticket[j] > ticket[i])) \wedge \neg suspected[i]$

\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm that eventually guarantees a single token \label{fig:col}}
\end{figure}

\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_i$::\\
\> {\bf var}\\
\> $v$: initial value;\\
\\
\> Send $v$ to all processes;\\
\> Upon receiving $N-f$ proposals;\\
\> \>       $decision$ := $min$(proposals);
%\vspace{-8mm}
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for solving the $k$-set consensus problem \label{fig:k-set}}
\end{figure}


\begin{figure}[htb]\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_0$::\\
\> send message $m$ to all other processes;\\
\\
\\
$P_i (i \in \{1..N-1\})$::\\
\> {\bf var}\\
\> \> $notdone$: boolean initially $true$;\\
\\
\> On receiving a message $m$;\\
\> \> {\bf if} $notdone$ then send message $m$ to all processes;\\
\> \> $notdone := \false$;\\
\\
\end{tabbing}
\end{minipage}
} % end \fbox
\end{center}
\caption{An algorithm for reliable broadcast of message $m$ \label{fig:rbcast}}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/second-1.1.eps}}
\caption{An example of the domino effect}
\label{fig:domino}
\end{figure}



\begin{figure}[htbp]
\centerline{\epsfbox{figs/second-1.2.eps}}
\caption{Examples of zig-zag paths}
\label{fig:zig}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/second-1.3.eps}}
\caption{Example of an R-graph}
\label{fig:rgraph}
\end{figure}


\begin{figure}[htbp]
\centerline{\epsfbox{figs/second-2.1.eps}}
\caption{Example of a computation with local predicates}
\label{fig:compslice}
\end{figure}

\begin{figure}[htbp]
\centerline{\epsfbox{figs/second-2.2.eps}}
\caption{Slice of the computation}
\label{fig:conjslice}
\end{figure}


\begin{figure}
\begin{center}
\input{figs/f1.tex}
%\centerline{\epsfxsize=0.80\textwidth\epsfbox{figs/recovery.eps}}
\caption{A distributed computation\label{fig:comp}}
\end{center}
\end{figure}

 
\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_{i}$:: \\
\> {\bf type} $entry$ =  (integer $ver$, integer $ts$); // version, timestamp  \\
\> {\bf var} $clock$ : array [$1..N$] of entry initially\\
\> \> $\forall j : clock[j].ver = 0$ ; \\
\> \> $\forall j: j \neq i: clock[j].ts = 0 ; clock[i].ts = 1 $; \\
%/*--------------------------------------------------------------*/   \\
\\
\> { { To send message}} : \\
 \> \> send $(data, clock)$ ; \\
 \> \> $clock[i].ts := clock[i].ts + 1$; \\
%/*--------------------------------------------------------------*/ \\
\\
\> { { Upon receive of a message}} $(data, mclock)$  : \\ 
\> \> // $P_i$ receives vector clock `mclock' in incoming message  \\
\>\>  $\forall j: clock[j] = max(clock[j],mclock[j]) $; \\
 \> \> $clock[i].ts := clock[i].ts + 1$; \\
%/*----------------------------------------------------------------*/ \\
\\
\> { { Upon Restart }}(state $s$ restored) :  \\
       \> \> $clock = s.clock$;   \\ 
       \> \> $clock[i].ver := clock[i].ver + 1$;\\
       \> \> $clock[i].ts = 0$;  \\
%/*----------------------------------------------------------------*/ \\
\\
\> { { Upon Rollback}}(state $s$ restored) :  \\
        \>\> $clock = s.clock$;   \\ 
\> %       clock[i].ver := clock[i].ver + 1; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\caption{Formal description of the fault-tolerant vector clock\label{fig:ftvc}}
\end{center}
\end{figure}

\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_{i}$::\\
 \> {\bf var}\\
 \> \> $vtable$ :  array[$1..N$] of set of entry initially empty; \\
 \> \> $token$ :  entry;\\
% /*--------------------------------------------------------------*/ \\
\> { { Receive\_token}} $(v_1,t_1)$ from $P_j$ :  \\
\>   \>  $insert(vtable[j],  (v_1,t_1))$ ; \\
%  /*--------------------------------------------------------------*/ \\
\> { { Upon Restart}} \\
\>  \> $insert(vtable[i],  (v,clock[i].ts))$ ; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\caption{A formal description of the version end table mechanism\label{fig:version-end-table}}
\end{center}
\end{figure}


\begin{figure}[htbp]
\begin{center}
\fbox{\begin{minipage}  {\textwidth}\sf
\begin{tabbing}
x\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill
$P_{i}$:: \\
\> { { Receive\_message}} (data, mclock)  :  \\ 
%\> \> /* $P_i$ receives clock `mclock' in incoming message */\+ \\
\> \>    // Check whether message is obsolete  \\
\> \>    $\forall j$:{\bf if} $((mclock[j].ver,t) \in vtable[j]) $
 			 {\bf and}  $( t < mclock[j].ts )$ {\bf then} \\
\> \> \> discard message ; \\
%\> \> /* If not discarded then */ \\
\> \>    {\bf  if} $\exists j,l$ s.t. $l < mclock[j].ver \wedge  P_i$
	has  no token about $P_{j,l}$ {\bf then} \\
\> \>   \> postpone the delivery of the message until that token arrives;  \\
\\
%/*----------------------------------------------------------------*/ \\
\> { { Restart}} (after failure) :  \\
       \> \> restore last checkpoint; \\
       \> \> replay all the logged messages that follow the restored state; \\
       \> \> $insert(vtable[i],  (v,clock[i].ts))$;\\
       \> \> $broadcast\_token(clock[i])$;            \\
%/*-----------------------------------------------------------------*/ \\
\\
\> { { Receive\_token}} (v,t) from $P_j$ :   \\
  \> \> synchronously log the token to the stable storage; \\
  \>\>  {\bf if} $((mes,v,t') \in vtable[j])$ {\bf then}  \\
  \>\>  \>    {\bf if} $(t < t')$  {\bf then}  Rollback; \\ 
  \>\>  // Regardless of rollback, following actions are taken  \\
  \> \> update $vtable$; \\
  \> \> deliver  messages that were held for this token;  \\
%/*------------------------------------------------------------------*/ \\
\\
\> { { Rollback}} ( due to token  $(v,t)$ from $P_j$ ) :  \\
  \>\>  log all the unlogged messages to the stable storage; \\
  \>\>  restore the maximum checkpoint such that  \\
  \>\>  \>  either no record $(v,t') \in vtable[j]$ or  $(t' < t)$   ..(I) \\
  \>\>  discard the checkpoints that follow; \\
  \>\>  replay the messages logged after this checkpoint\\
   \> \> \> until condition (I) holds; \\
  \>\>  discard the logged messages that follow; \\
\end{tabbing}
\end{minipage}
} % end \fbox
\caption{An optimistic protocol for asynchronous recovery\label{fig:complete}}
\end{center}
\end{figure}

\begin{figure}\begin{center}
%\centerline{\epsfxsize=0.80\textwidth\epsfbox{figs/recovery2.eps}}
\input{figs/f2.tex}
\end{center}
\caption{An example of recovery\label{fig:recovery}}
\end{figure}
