Use of eCommons for rapid dissemination of COVID-19 research
In order to maximize the discoverability of COVID-19 research, and to conform with repository best practices and the requirements of publishers and research funders, we provide special guidance for COVID-19 submissions.
Effectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLP
|dc.contributor.author||Constable, Robert L.|
|dc.description.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 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.sponsorship||This 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.subject||One Step Lemma||en_US|
|dc.title||Effectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLP||en_US|