Show simple item record

dc.contributor.authorConstable, Robert L.
dc.description.abstractThe 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 such a protocol. That is, given the 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.en_US
dc.description.sponsorshipThis work was funded by NSF grant CNS 872612445 and by the Information Directorate of the Air Force Research Lab (AFRL) at Rome, grant FA 8750-08-2-0153.en_US
dc.subjectInitialization Lemmaen_US
dc.subjectConstructive FLPen_US
dc.subjectOne Step Lemmaen_US
dc.titleEffectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLPen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record