Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP

TL;DR

This paper provides a constructive proof that effectively nonblocking consensus protocols can run forever, offering new insights into the FLP impossibility theorem and implications for protocol design and attack strategies.

Contribution

It introduces a constructive method to simulate infinite indecisive executions of nonblocking protocols, strengthening FLP with a practical approach.

Findings

Constructs infinite indecisive executions for nonblocking protocols.

Derives FLP as a corollary from the constructive proof.

Shows potential for building undefeatable attackers against correct protocols.

Abstract

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.