PDF Publication Title:
Text from PDF Page: 040
40 2.6. SAFETY of Classic Paxos, but first we begin by proving some simple properties of the algorithm, which will be of use to us later on. Lemma 6 (Monotonicity of promises). The last promised epoch stored by each acceptor is monotonically increasing. Proof of lemma 6. The last promised epoch is initially nil and can only be updated by acceptors in response to receiving prepare or propose from proposers (Property 10). The last promised epoch is only updated to the epoch received if the epoch received is greater than or equal to last promised epoch (Properties 6 & 7). Therefore the last promised epoch is strictly increasing. Lemma 7 (Relation between acceptor epochs). The last promised epoch is always greater than (or equivalent to) the last accepted epoch on each acceptor. Proof of lemma 7. Whenever the last accepted proposal is updated, the last promised epoch has always been updated to the same value (Properties 9 & 10). As a result, the last accepted proposal is never updated to a value strictly greater than the last promised epoch. Lemma 6 shows that the last promised epoch is monotonically increasing thus the last promised epoch is never updated to a value less than the last accepted epoch. Therefore, it is always the case that the last promised epoch ≥ last accepted epoch. The proof of lemma 7 highlights the importance of ensuring the steps in the Classic Paxos algorithm are executed in-order. If the last accepted proposal was written prior to writing the last promised epoch then an acceptor failure between these two writes could violate lemma 7. Lemma 8 (General promise format). For all promises sent by acceptors of the form promise(e,f,v), where f ̸= nil then it is the case that e ≥ f. Proof of lemma 8. An acceptor would send promise(e,f,v) in response to receiving pre- pare(e) from a proposer (Property 8). Therefore e ≥ the last promised epoch when the prepare message was received. From lemma 7 the last promised epoch ≥ the last accepted epoch f. By transitivity on the ≥ relation, e ≥ f One implication of lemma 8 is that acceptors may send promises of the form promise(e,e,v). This might occur if an acceptor was to receive a proposer’s propose(e,v) before prepare(e) due to out-of-order delivery. However, a promise of this form will never be used by a proposer to complete phase one. This is because the proposer of e will have already completed phase one since (e, v) had already been proposed. Corollary 8.1 (Useful promise format). All promises that are used by proposers towards a decision are either of the forms promise(e,nil,nil) (without a proposal) or promise(e,f,v) where e > f (with a previous proposal).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 | RSS | AMP |