Unknown macro: {latex}
\enlargethispage
Unknown macro: {1000mm}
% keeps everything on one page so it is returned by latex macro.
\usepackage
Unknown macro: {amssymb}
\usepackage
Unknown macro: {amstext}
\newcommand\ignore[2]{}
%------------------Jim Aug 11 --------------------------
\newcommand
Unknown macro: {ThirdNodeType}
Unknown macro: {rput}
\usepackage
Unknown macro: {pstricks,pst-node,pst-tree}
\usepackage
Unknown macro: {wrapfig}
\psset
Unknown macro: {nodesep=3pt}
\psset
Unknown macro: {xunit=.9cm}
\psset
Unknown macro: {yunit=.9cm}
%\usepackage
Unknown macro: {times}
%\usepackage
Unknown macro: {simplemargins}
%\newcommand\modabstract[1]{\center\textbf
Unknown macro: {Abstract}
\flushleft \begin
Unknown macro: {minipage}
[h]
Unknown macro: {5.5in}
#1\end{minipage}}
\Large\begin
Unknown macro: {center}
\textbf{Effectively Nonblocking Consensus
Procedures Can Execute Forever – a Constructive Version of FLP
}
\vspace
Unknown macro: {.25in}
\large
Unknown macro: {Robert L. Constable}
\normalsize\em
Unknown macro: {Cornell University}
\normalsize\em
Unknown macro: {Print date}
\normalsize\em
Unknown macro: {July 17, 2008}
\footnote
Unknown macro: {The current draft includes improvements up to August 30,2008 and small non technical edits to the July 17, 2008 version made in August 2011. See Acknowledgements at the end of the article for grants supporting this work.}
\end
\begin
Unknown macro: {flushleft}
\normalsize
\begin
Unknown macro: {abstract}
\noindent The Fischer-Lynch-Paterson theorem (FLP) says that it is
impossible for processes in an \emph
Unknown macro: {asynchronous distributedsystem}
to achieve consensus on a binary value when a single process
can fail; it is a widely cited theoretical result about network
computing. All proofs that I know depend essentially on classical
(nonconstructive) logic, although they use the hypothetical
construction of a nonterminating execution as a main lemma.
\flushleft
FLP is also a guide for protocol designers, and in that role there
is a connection to an important property of consensus procedures,
namely that they should not \emph
Unknown macro: {block}
, i.e. reach a global state
in which no process can decide.
\flushleft
A deterministic fault-tolerant consensus protocol is
\emph
Unknown macro: {effectively nonblocking}
if from any reachable \emph
Unknown macro: {globalstate}
we can find an execution path that decides. In this article
we effectively construct a nonterminating execution of any such
protocol. That is, given any effectively nonblocking protocol \textbf
Unknown macro: {P}
and a natural
number $n$, we show how to compute the $n$-th step of an infinitely
\emph
Unknown macro: {indecisive computation}
of \textbf
. From this fully constructive
result, the \emph
Unknown macro: {classical FLP}
follows as a corollary as well as a
stronger classical result, called here \emph
Unknown macro: {Strong FLP}
. Moreover,
the construction focuses attention on the important role of
nonblocking in protocol design.
\flushleft
An interesting consequence of the constructive proof is that we can, in principle, build an \emph
Unknown macro: {undefeatable attacker}
for a consensus protocol that is provably correct, indeed because it is provably correct. We can do this in practice on certain kinds of networks.
\end
\section
Unknown macro: {Introduction}
\subsection
Unknown macro: {Background}
The standard version of the Fisher-Lynch-Paterson theorem is that
there is no asynchronous distributed algorithm that is responsive to
its inputs, solves the agreement problem, and guarantees 1-failure
termination. This is a negative statement, producing a
contradiction, yet implicit in all proofs is an imagined
construction of a nonterminating execution in which no process
decides, they "waffle" endlessly. That imagined execution is an
interesting object, displaying what can go wrong in trying to reach
consensus and characterizing a class of protocols. The hypothetical
execution is used to guide thinking about consensus protocol design
(illustrated below). In light of that use, a natural question about
the classical proofs of FLP is whether the hypothetical infinite
waffling execution could actually be constructed from any purported
consensus protocol \textbf
Unknown macro: {P}
, that is, given \textbf
, can we
exhibit an algorithm $\alpha$ such that for any natural number $n$,
$\alpha
$ is the $n$-th step of the indecisive computation.
It appears that no such explicit construction could be carried out
following the method of the classical proof because there isn't
enough information given with the protocol, and the key concept in
the standard proofs, the notion of \emph
Unknown macro: {valence}
(\emph
Unknown macro: {univalence}
and \emph
Unknown macro: {bivalence}
), is not defined effectively, i.e. they require
knowing the results of all possible executions. This means that the
case analysis used to imagine the infinite execution can not
actually be decided. Of course, it is not possible to find this
infinite execution by simply running a purported protocol. Only a
\emph
Unknown macro: {proof}
can show that it will run forever.
Other authors \cite
Unknown macro: {Vol04,BW87}
have reformulated the proof of the
FLP in a way that singles out the infinite computation as the result
of a separate lemma, but they do not provide an effective means of
building the infinite computation and do not use constructive
reasoning. I refer to Volzer's classical result as \emph
Unknown macro: {StrongFLP}
; it is a corollary of the effective construction given here.
The key to being able to build the nonterminating execution is to
provide more information, which we do by introducing the notion of
\emph
Unknown macro: {effective nonblocking}
, defining bivalence effectively, and
introducing the idea of a \emph
Unknown macro: {v-possible execution}
. We use the
term \emph
in most of this article to make comparison
with the classical ideas clear, but when contrasting this work to
others, we will use the term \emph
Unknown macro: {effective bivalence}
.
\footnote
Unknown macro: {In the original FLP article the authors say}
Effective nonblocking is a natural concept in the setting in which
we verify protocols using constructive logic, say the rules of the
Nuprl formal programming environment or of the Coq prover
\cite
Unknown macro: {BYC04}
. The logic of Nuprl is Computational Type Theory (CTT)
\cite
Unknown macro: {ABCEKLM05}
, which is constructive, and the logic of Coq is the
Calculus of Inductive Constructions (CIC), closely related to CTT
and also constructive. So when we prove that a protocol is
nonblocking, we obtain the effective witness function used in the
definition below. Mark Bickford in his Nuprl formalization
of consensus protocols has done formal
proofs of nonblocking from which Nuprl can extract the deciding
state and could extract an execution as well.
The importance of nonblocking can be seen from this "blocking
theorem" by Robbert van Renesse in \cite
Unknown macro: {Rvr08}
: \emph
Unknown macro: {A consensusprotocol that guarantees a decision in the absence of failures mayblock in the presence of even a single failure.}
This is justified
by citing FLP, and it follows cleanly from CFLP as I show below. Robbert van Renesse says: ``Blocked states occur when one or more
processes fail at a time at which other processes cannot determine
if the protocol has decided. A protocol that tolerates failures must
avoid such blocked states''. Protocol designers actually carry out
an analysis of blocking in debugging designs. A constructive proof
of the \emph
Unknown macro: {blocking theorem}
could find the blocking scenario
after designating a process that fails. Knowing precisely the number
of blocking scenarios and their properties would be useful in
evaluating protocol designs.
It is fascinating that once we use the concept of effective
bivalence, it is possible to automatically translate some
nonconstructive proofs of FLP into fully constructive ones from
which it is possible to build the nonterminating execution. Here we look
at the simpler result that we can effectively build nonterminating
executions. These are executions that endlessly waffle about the
decisions that are possible, decisions actually taken by
\emph
Unknown macro: {decisive executions}
.
Since it is not possible to provide an \emph
Unknown macro: {algorithm}
, i.e. a
\emph
Unknown macro: {terminating}
consensus procedure, we start with the kind of
protocol that can be built, and stress the possibility of
nontermination by calling it a \emph
Unknown macro: {procedure}
not an algorithm.
\subsection
Unknown macro: {Computing Model}
The results here depend on the computing model behind the Logic of
Events, \cite
Unknown macro: {BC08}
which is essentially embedding the standard model of asynchronous
message-passing network computing into
Computational Type Theory. The standard model is presented in the book
\emph
Unknown macro: {Distributed Computing}
of Attyia \& Welch \cite
Unknown macro: {AW04}
and is
similar to the one in \cite
Unknown macro: {FLP85}
. We assume reliable FIFO communication
channels.
A \emph
Unknown macro: {global state}
of the system consists of the state of the
processes and the condition of the message queues. An
\emph
Unknown macro: {execution}
is an alternating sequence of global states and
actions taken by processes. Thus an execution $\alpha$ of
distributed system \textbf
Unknown macro: {S}
determines sequence of \emph
Unknown macro: {globalstates}
, $s_1, s_2, s_3, ...$. These are also called
\emph
Unknown macro: {configurations}
of the execution. Execution is fair \emph
Unknown macro: {in}
that all messages sent to nonfailing processes
will eventually be read and all enabled actions will eventually be
taken by processes that do not fail.
A \emph
Unknown macro: {step of computation}
can involve any finite number of processes
reading a message from an input channel, changing the internal
state, and sending messages on output channels. In the proofs here,
we pick an order on these steps so that there is always a single
action separating the global states. We say that a \emph
Unknown macro: {schedule}
determines the order of the actions.
\subsection
Unknown macro: {Definitions}
\textbf
Unknown macro: {Definition}
: A Boolean \emph
Unknown macro: {consensus procedure}
on
processes $P_
Unknown macro: {i}
~i=1,...,n$ tolerating $t$ failures is a possibly
nonterminating distributed procedure \textbf
Unknown macro: {P}
which is deterministic
(no randomness), responsive on uniform initializations, consistent
(all deciding processes agree on the same value).
\textbf
is called \emph
Unknown macro: {effectively nonblocking}
if from any
reachable global state $s$ of an execution of \textbf
Unknown macro: {P}
and any
subset $Q$ of $n-t$ nonfailed processes, \emph
Unknown macro: {we can find}
an
execution $\alpha$ from $s$ using $Q$ and a process $P_
Unknown macro: {alpha}
$ in
$Q$ which decides a value $v~\epsilon~\mathbb
Unknown macro: {B}
$.
Constructively this means that we have a computable function,
$wt(s,Q)$ which produces an execution $\alpha$ and a state
$s_\alpha$ in which a process, say $P_\alpha$ decides a value $v$.
In this setting, a consensus procedure is \emph
Unknown macro: {responsive}
if when
\emph
Unknown macro: {all}
processes are initialized to $v$, they terminate with
decision $v$ unless they fail. This means that all nonblocking
witnesses will return $v$ as well.
The nonblocking property requires that consensus procedures
tolerating $t$ failures can use any subset of $n-t$ processes to
pick out from any partial execution a process that makes a decision.
This is enough information for an \emph
Unknown macro: {algorithmic adversary}
to
prevent a deterministic consensus procedure, one that does not rely
on randomness, from terminating on every execution. The adversary
can keep adjusting the schedule of executions to prevent processes
from deciding.
It is important to have good notations for the class of all
processes of \textbf
except for $P_i$. We denote that class by $Q_i$, because we
want to factor executions into steps of a specified process and
those of the remaining processes. These are disjoint sets, and we
can combine executions from them by appending one to another and
infer joint properties from the separate properties of each.
\textbf
For a $v~\epsilon~\mathbb
Unknown macro: {B}
$, a global state
$s$ is \emph
Unknown macro: {v-possible}
\emph
Unknown macro: {iff}
for some subset $Q$ of $n-t$
processes we can find using the nonblocking witness a state
$s^
Unknown macro: {prime}
_
Unknown macro: {Q}
$ and a process $P_Q$ in $s^
_
Unknown macro: {Q}
$ that
decides $v$. That is, $wt(s,Q)$ produces a computation ending in
$s^
Unknown macro: {prime}
_
$.
\textbf
Unknown macro: {Definition}
A global state $b$ is \emph
Unknown macro: {bivalent}
iff we
can find executions $\alpha_0$ and $\alpha_1$ from $b$ that decide
$0$ and $1$ respectively. We can pick out the deciding process from
the execution. A state is \emph
Unknown macro: {bivalent via $Q_i$}
if neither
execution involves a step of process $P_i$. Note, if $b$ is
bivalent, we can effectively exhibit the executions $\alpha_0$ and
$\alpha_1$.
\textbf
Unknown macro: {Fact}
It is \emph
Unknown macro: {decidable}
whether the global states of a
consensus procedure are $v-possible$.
Note, we can't decide bivalence.