Unformatted text preview:

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

MIT 6 852 - Lecture Notes

Download Lecture Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?