6.852: Distributed Algorithms Spring, 2008Today’s planLamport’s Bakery AlgorithmBakery AlgorithmCorrectness: Mutual exclusionSlide 6Slide 7Liveness ConditionsFIFO ConditionImpact of Bakery Algorithm6.852: Distributed AlgorithmsSpring, 2008Class 14Today’s plan•More mutual exclusion algorithms:–Lamport’s Bakery algorithm, cont’d–Burns’ algorithm•Lower bound on shared memory for mutual exclusion•Reading: Sections 10.6-10.8•Next: Chapters 10 and 11.Lamport’s Bakery Algorithm•Features:–Uses only single-writer, multi-reader registers.–Extends to even weaker registers called “safe registers”, in which operations have durations, and a read that overlaps a write receives an arbitrary response. –Guarantees lockout-freedom, in fact, almost-FIFO behavior.•But:–Registers are unbounded size.–Algorithm can be simulated using bounded registers, not easily.•Shared variables:–For each process i:•choosing(i), a Boolean, written by i, read by all, initially 0•number(i), a natural number, written by i, read by all, initially 0Bakery Algorithm•First part (the “Doorway”, D):–Process i sets choosing(i) to 1.–Reads other processes’ numbers, chooses a number greater than all the numbers it reads, writes it in number(i).–Then sets choosing(i) to 0.•Second part:–Wait to see that no others are choosing, and no one else has a smaller (number, id) pair.–Wait for each process j in turn:•First for choosing(j) = 0, •Then for number(j) = 0 or (number(i), i) < (number(j), j).Correctness: Mutual exclusion•Key invariant: If process i is in C, and process j i is in (T D) C, then (number(i),i) < (number(j),j).•Proof: –Could prove by induction.–Instead, give argument based on events in executions.–This argument extends to weaker registers, with concurrent accesses.Trying region after doorway, or critical regionCorrectness: Mutual exclusion•Invariant: If i is in C, and j i is in (T D) C, then (number(i),i) < (number(j),j).•Proof: –Consider a point where i is in C and j i is in (T D) C.–Then before i enters C, it must read choosing(j) = 0, event .–Case 1: j sets choosing(j) := 1 (starts choosing) after .•Then number(i) is set before j starts choosing.•So j sees the “correct” number(i) and chooses something bigger. •That suffices.–Case 2: j sets choosing(j) := 0 (finishes choosing) before .•Then when i reads number(j) in its second waitfor loop, it gets the “correct” number(j). •Since i decides to enter C, it must see (number(i),i) < (number(j),j). : i reads choosing(j) = 0 i in C, j in (T D) CCorrectness: Mutual exclusion•Invariant: If i is in C, and j i is in (T D) C, then (number(i),i) < (number(j),j).•Proof of mutual exclusion:–Apply invariant both ways.–Contradictory requirements.Liveness Conditions•Progress:–By contradiction.–If not, eventually region changes stop, leaving everyone in T or R, and at least one process in T.–Everyone in T eventually finishes choosing.–Then nothing blocks the smallest (number, index) process from entering C.•Lockout-freedom:–Consider any i that enters T–Eventually it finishes the doorway.–Thereafter, any newly-entering process picks a bigger number.–Progress implies that processes continue to enter C, as long as i is still in T.–In fact, this must happen infinitely many times!–But those with bigger numbers can’t get past i, contradiction.FIFO Condition•Not really FIFO (T vs. C), but close:–“FIFO after the doorway”: if j leaves D before i T, then j C before i C.•But the “doorway” is an artifact of this algorithm, so this isn’t a meaningful way to evaluate it.•Maybe say “there exists a doorway such that”…–But then we could take D to be the entire trying region, making the property trivial.•To make the property nontrivial:–Require D to be “wait-free”: a process must complete D if it keeps taking steps, regardless of what any other processes do.–D in the Bakery Algorithm is wait-free.•“FIFO after a wait-free doorway”Impact of Bakery Algorithm•Originated important ideas:–Wait-freedom•Fundamental notion for theory of fault-tolerant asynchronous distributed algorithms.–Weakly coherent memories•Beginning of formal study: definitions, and some algorithmic strategies for coping with
View Full Document
Unlocking...