Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Effectively Nonblocking Consensus Procedures Can Execute Forever ? a Constructive Version of FLP

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

File(s)
Effectively.pdf (193.67 KB)
Permanent Link(s)
https://hdl.handle.net/1813/11512
Collections
Computing and Information Science Technical Reports
Author
Constable, Robert L.
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.

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.
Date Issued
2008-10-15T19:50:59Z
Keywords
Initialization Lemma
•
Constructive FLP
•
One Step Lemma
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance