Computer Science – Logic in Computer Science
Scientific paper
2011-09-15
Computer Science
Logic in Computer Science
17 pages, 6 figures, uses pstricks; http://hdl.handle.net/1813/11512
Scientific paper
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.
No associations
LandOfFree
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-673531