\begin{itemize}
\item
$\alpha = \delta \cdot a_n \cdot \varepsilon$
\item
$\gamma$ is the sequence returned by $wt(s_{n-1},Q_i)$ and $b$ is
its final state
\item
$a_n$ is an action of process $P_i$
\item
none of the sequences $\beta$, $\gamma$, or $\varepsilon$ contains
an action from process $P_i$
\item
$d_1$ decides 1 and $d_0$ decides 0
\end{itemize}

<pre>{latex}
\begin{itemize}
\item
$\alpha = \delta \cdot a_n \cdot \varepsilon$
\item
$\gamma$ is the sequence returned by $wt(s_{n-1},Q_i)$ and $b$ is
its final state
\item
$a_n$ is an action of process $P_i$
\item
none of the sequences $\beta$, $\gamma$, or $\varepsilon$ contains
an action from process $P_i$
\item
$d_1$ decides 1 and $d_0$ decides 0
\end{itemize}
{latex}
</pre>

{latex}
\enlargethispage{36in}    % keeps everything on one page so it is returned by latex macro.


\Large\begin{center} \textbf{Effectively Nonblocking Consensus
Procedures Can Execute Forever -- a Constructive Version of FLP
}\\
\vspace{.25in}
 \large{Robert L. Constable}\\
 \normalsize\em{Cornell University} \\
 \normalsize\em{Print date: \today}\\
 \normalsize\em{July 17, 2008}\footnote{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{center}

\begin{flushleft}
\normalsize

\begin{abstract}
\noindent The Fischer-Lynch-Paterson theorem (FLP) says that it is
impossible for processes in an \emph{asynchronous distributed
system} 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{block}, i.e. reach a global state
in which no process can decide.
\flushleft
A deterministic fault-tolerant consensus protocol is
\emph{effectively nonblocking} if from any reachable \emph{global
state} 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{P} and a natural
number $n$, we show how to compute the $n$-th step of an infinitely
\emph{indecisive computation} of \textbf{P}. From this fully constructive
result, the \emph{classical FLP} follows as a corollary as well as a
stronger classical result, called here \emph{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{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{abstract}

{latex}