6.852: Distributed Algorithms Spring, 2008Today’s planAsynch Shared Memory ModelASM ModelThe Mutual Exclusion ProblemSlide 6Slide 7Slide 8One more assumption…Mutual Exclusion algorithm [Dijkstra 65]Dijkstra’s algorithmDijkstra’s algorithm, pre/eff codeNote on code styleCorrectnessProgressProgress, cont’dSlide 17Mutual exclusion, Proof 2Running TimeAdding fairness guarantees [Peterson]Peterson 2-process algorithmCorrectness: Mutual exclusionCorrectness: ProgressCorrectness: Lockout-freedomTime complexityPeterson n-process algorithmsSequence of competitionsSlide 28Slide 29Slide 30Progress, Lockout-freedomPeterson Tournament AlgorithmSlide 33Slide 34Bounded Bypass?Lamport’s Bakery AlgorithmBakery AlgorithmSlide 38Slide 39Slide 40Liveness ConditionsFIFO ConditionImpact of Bakery AlgorithmNext time…6.852: Distributed AlgorithmsSpring, 2008Class 13Today’s plan•The mutual exclusion problem•Dijkstra’s algorithm•Peterson’s algorithms•Lamport’s Bakery algorithm•Reading: Sections 10.1-10.5, 10.7•Next: Sections 10.6-10.8Asynch Shared Memory Model•One big shared memory system automaton A.•External actions at process “ports”.•Each process i has:–A set statesi of states.–A subset starti,of start states. •Each variable x has:–A set valuesx of values it can take on.–A subset initialx of initial values.p1p2pnx1x2A•Automaton A:–States: State for each process, a value for each variable.–Start: Start states, initial values.–Actions: Each action associated with one process, and some also with a single shared variable.–Input/output actions: At the external boundary.–Transitions: Correspond to local process steps and variable accesses.–Tasks: One or more per process (threads).ASM Model•Execution of A:–By IOA fairness definition, each task gets infinitely many chances to take steps.–Model environment as a separate automaton, to express restrictions on environment behavior.p1p2pnx1x2A•Commonly-used variable types:–Read/write registers: Most basic primitive.•Allows access using separate read and write operations.–Read-modify-write: More powerful primitive.•Atomically, read variable, do local computation, write to variable.–Compare-and-swap, fetch-and-add, queues, stacks,…The Mutual Exclusion Problem•Share one resource among n user processes, U1, U2,…,Un.•Ui has four “regions”.–Subsets of its states, described by portions of its code.–C critical; R remainder; T trying; E exit•Cycle: •Architecture:–Uis and A are IOAs, compose.R T C Ep1p2pnx1x2AU1U2UnProtocols for obtaining and relinquishing the resourceThe Mutual Exclusion Problem•Actions at user interface:–tryi, criti, exiti, remi–Ui interacts with pi•Correctness conditions:–Well-formedness (Safety property):•System obeys cyclic discipline.•E.g., doesn’t grant resource when it wasn’t requested.–Mutual exclusion (Safety):•System never grants to > 1 user simultaneously.•Trace safety property.•Or, there’s no reachable system state in which >1 user is in C at once.–Progress (Liveness):•From any point in a fair execution:–If some user is in T and no user is in C then at some later point, some user enters C.–If some user is in E then at some later point, some user enters R.p1p2pnx1x2AU1U2UnpiUitryicritiexitiremiThe Mutual Exclusion Problem•Well-formedness (Safety):–System obeys cyclic discipline.•Mutual exclusion (Safety):–System never grants to > 1 user.•Progress (Liveness):–From any point in a fair execution:•If some user is in T and no user is in C then at some later point, some user enters C.•If some user is in E then at some later point, some user enters R.p1p2pnx1x2AU1U2Un•Conditions on the system automaton A, not the users.–System determines if/when users enter C and R.–Users determine if/when users enter T and E.–We don’t state any requirements on the users, except for assuming that they respect well-formedness.The Mutual Exclusion Problem•Well-formedness (Safety):•Mutual exclusion (Safety):•Progress (Liveness):–From any point in a fair execution:•If some user is in T and no user is in C then at some later point, some user enters C.•If some user is in E then at some later point, some user enters R.p1p2pnx1x2AU1U2Un•Fairness assumption:–Progress condition requires fairness assumption (all process tasks continue to get turns to take steps).–Needed to guarantee that some process enters C or R.–In general, in the asynchronous model, liveness properties require fairness assumptions.–Contrast: Well-formedness and mutual exclusion are safety properties, don’t depend on fairness.One more assumption…•No permanently active processes.–Locally-controlled actions enabled only when user is in T or E.–No always-awake, dedicated processes.–Motivation:•Multiprocessor settings, where users can run processes at any time, but are otherwise not involved in the protocol.•Avoid “wasting a processor”.Mutual Exclusion algorithm [Dijkstra 65]•Based on Dekker’s 2-process solution.•Pseudocode, p. 265-266–Written in traditional sequential style, must somehow translate into more detailed state/transition description.•Shared variables: Read/write registers.–turn, in {1,2,…,n}, multi-writer multi-reader (MWMR), init anything.–for each process i:•flag(i), in {0,1,2}, single-writer multi-reader (1WMR), init 0•Written by i, read by everyone.•Process i’s Stage 1:–Set flag := 1, repeatedly check to see if turn = i.–If not, and turn’s current owner is seen to be inactive, then set turn := i.–Otherwise keep checking.–When you see turn = i, move to Stage 2.Dijkstra’s algorithm•Stage 2:–Set flag(i) := 2.–Check (any order) that no other process has flag = 2.–If check completes successfully, go to C.–If not, go back to beginning of Stage 1.•Exit protocol:–Set flag(i) := 0.•Problem with the code style:–Unclear what constitutes an atomic step.•E.g., need three separate steps to test turn, test flag(turn), and set turn.–Must rewrite to make this clear:•E.g., precondition/effect code (p. 268-269)•E.g., sequential-style code with explicit reads and writes, one per line.Dijkstra’s algorithm, pre/eff code•One transition definition for each kind of atomic step.•Explicit program counter.•E.g.:–set-flag-1i: Sets flag to 1 and prepares to test turn.–test-turni: Tests turn, and either moves to Stage 2 or
View Full Document