Unknown macro: {latex}
%\enlargethispage
Unknown macro: {12in}
% keeps everything on one page so it is returned by latex macro.
\usepackage
Unknown macro: {amssymb}
\usepackage
Unknown macro: {amstext}
\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
\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.