PDF Publication Title:
Text from PDF Page: 045
CHAPTER 2. CONSENSUS & CLASSIC PAXOS 45 Table 2.3 outlines how we divided up our proof of Safety for Classic Paxos (Theorem 14). Our approach of using multiple layers of intermediate results will allow us to revise this proof throughout this thesis, without reproducing the complete proof. It is worthwhile noting that lemmas 6, 7, 8 and 10 are properties of the acceptor algorithm for Classic Paxos. Their proofs do not rely upon any properties of the proposer algorithm and thus these lemmas still hold if the proposers behave arbitrarily. Likewise lemmas 11 and 9 are properties of the proposer algorithm for Classic Paxos and do not reply upon the acceptor algorithm. 2.7 Progress The proof of safety for Classic Paxos does not depend on any liveness conditions such as bounded message delay or execution time. In contrast, the proof of progress, the sub- ject of this section, must depend upon some liveness conditions, as proved by the FLP result [FLP85]. We will formulate progress as follows: from time 0 to Global Stabilisation Time (GST), a system of participants have been executing Classic Paxos. No assumptions regarding liveness are made during this time. The system may be in any reachable state at GST. From GST, the following liveness conditions must apply for a sufficient period: • At least a majority of acceptors are live and reply to messages from proposers, if specified by the algorithm, within the known upper bound δa16. • Exactly one (fixed) proposer is live and its relative clock is no faster than δd ahead of global time. We assume that no messages from other proposers are delivered17. • Messages between the proposer and majority of acceptors are delivered within the known bound δm. This model of initial asynchrony, eventually followed by synchrony is sometimes known as partial synchrony [DLS88]. As expected, we require that a majority of acceptors are up and able to communicate as the proposer will need to get majority agreement to complete the two phases of Classic Paxos. We also need to require that exactly one proposer is executing the algorithm to prevent proposers duelling indefinitely, as illustrated in Figure 2.6 (§2.3). The requirements for bounded execution time, message delay and clock drift are to ensure that the acceptors will have a chance to respond to messages from the proposer prior to the proposer restarting the proposal. 16This need not be a fixed group, but we will assume it is to simplify our proof. 17This assumption is not necessary for guaranteeing progress but it does simplify our proof.PDF Image | Distributed consensus
PDF Search Title:
Distributed consensusOriginal File Name Searched:
UCAM-CL-TR-935.pdfDIY PDF Search: Google It | Yahoo | Bing
Cruise Ship Reviews | Luxury Resort | Jet | Yacht | and Travel Tech More Info
Cruising Review Topics and Articles More Info
Software based on Filemaker for the travel industry More Info
The Burgenstock Resort: Reviews on CruisingReview website... More Info
Resort Reviews: World Class resorts... More Info
The Riffelalp Resort: Reviews on CruisingReview website... More Info
CONTACT TEL: 608-238-6001 Email: greg@cruisingreview.com (Standard Web Page)