  The Fischer-Lynch-Paterson theorem (FLP) says that it is impossible for
processes in an 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.
  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 block, i.e. reach a global state in which no process can decide.
  A deterministic fault-tolerant consensus protocol is effectively nonblocking
if from any reachable 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 P and a natural
number n, we show how to compute the n-th step of an infinitely indecisive
computation of P. From this fully constructive result, the classical FLP
follows as a corollary as well as a stronger classical result, called here
Strong FLP. Moreover, the construction focuses attention on the important role
of nonblocking in protocol design.
  An interesting consequence of the constructive proof is that we can, in
principle, build an 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.
