6.852: Distributed Algorithms Spring, 2008Today’s planLegal execution fragmentsSelf-stabilization: DefinitionSS Algorithm 1: Breadth-first spanning treeBreadth-first spanning treeAlgorithm strategySelf-stabilizing mutual exclusionMutual exclusionLemma 1Lemma 2Lemma 3Lemma 4Putting the pieces togetherReducing the atomicityComposing self-stabilizing algorithmsComposing SS algorithmsWeaker definition of SSSlide 19Applying the composition theoremMutual exclusion in a rooted treeSelf-stabilizing emulations [Dolev, Chapter 4]Self-stabilizing emulationsMaking non-self-stabilizing algorithms self-stabilizingExample: ConsensusSlide 26ExtensionsMaking non-SS algorithms SS: Monitoring and resettingOther stuff in the book6.852: Distributed AlgorithmsSpring, 2008Class 25-1Today’s plan•Self-stabilizing algorithms:–Breadth-first spanning tree (review)–Mutual exclusion•Composing self-stabilizing algorithms•Making non-self-stabilizing algorithms self-stabilizing•Reading: –[ Dolev, Chapter 2 ]Legal execution fragments•Given a distributed algorithm A, define a set L of “legal” execution fragments of A.•L can include both safety and liveness conditions.•Example: Mutual exclusion–L might be the set of all fragments  such that:•(Mutual exclusion)–No two processes are in the critical region, in any state in .•(Progress) –If in some state of , someone is in T and no one is in C, then sometime thereafter, someone  C.–If in some state of , someone is in E, then sometime thereafter, someone  R.Self-stabilization: Definition•A global state of algorithm A is safe with respect to legal set L, provided that every fair execution fragment of A that starts with s is in L.•Algorithm A is self-stabilizing for legal set L if every fair execution fragment  of A contains a state s that is safe with respect to L.–Implies that the suffix of  starting with s is in L.–Also, any other fair execution fragment starting with s is in L.•Weaker definition: Algorithm A is self-stabilizing for legal set L if every fair execution fragment  has a suffix in L.SS Algorithm 1:Breadth-first spanning tree•Shared-memory model•Connected, undirected graph G = (V,E).•Processes P1,…,Pn, P1 a designated root.•Permanent knowledge:–P1 always knows it’s the root.–Everyone always knows who their neighbors are.P1P4P3P2r12r21r13r42r24r31•Neighboring processes in G share registers in both directions: –rij written by Pi, read by Pj.•Output: A breadth-first spanning tree, recorded in the rij:–rij.parent = 1 if j is i’s parent, 0 otherwise.–rij.dist = distance from root to i in the BFS tree = smallest number of hops on any path from 1 to i in G.–Values in registers should remain constant from some point onward.Breadth-first spanning tree •In terms of legal sets:–Define execution fragment  to be legal if:•The registers have correct BFS output values, in all states in .•Registers never change.–L = set of legal execution fragments.•Safe state s:–Global state from which all extensions have registers with correct, unchanging BFS output values.•SS definition says:–Any fair execution fragment , starting from any state, contains some “safe” state s.–That is, one from which all extensions have registers with correct, unchanging BFS output values.–Implies that any fair execution fragment  has a suffix in which the register contents represent a fixed BFS tree.Algorithm strategy•The system can start in any state, with–Any values (of the allowed types) in registers,–Any values in local process variables,•Processes can’t assume that their own states and output registers are initially correct.•Repeatedly recalculate states and outputs based on inputs from neighbors.•In case of tie, use default rule for selecting parent.•We proved correctness, stabilization time, using induction on distance from root.Self-stabilizing mutual exclusion•[Dijkstra 73]•Ring of processes, each with output variable xi.•High granularity: In one atomic step, process Pi can read both neighbors’ variables, compute its next value, and write it to variable xi. P1: do forever: if x1 = xn then x1 := x1 + 1 mod (n+1) Pi, i  1: do forever: if xi  xi-1 then xi := xi-1P1PnP3P2x1x2x3xn•That is:–P1 tries to make its variable unequal to its predecessor’s.–Each other tries to make its variable equal to its predecessor’sThat’s (n+1), not n.Mutual exclusion•In what sense does this “solve mutual exclusion”?•Definition: “Pi is enabled” (or “Pi can change its state”) in a configuration, if the variables are set so Pi can take a step and change the value of its variable xi.•Legal execution fragment :–In any state in , exactly one process is enabled.–For each i,  contains infinitely many states in which Pi is enabled.•Use this to solve mutual exclusion:–Say Pi interacts with requesting user Ui.–Pi grants Ui the critical section when:•Ui has requested it, and •Pi is enabled.–When Ui returns the resource, Pi actually does its step, changing xi.–Guarantees mutual exclusion, progress.–Also lockout-freedom.Lemma 1•Legal :–In any state in , exactly one process is enabled.–For each i,  contains infinitely many states in which Pi is enabled.•Lemma 1: A configuration in which all the x variables have the same value is safe.–Meaning from such a config, any fair execution fragment is legal.•Proof: Only P1 can change its state, then P2,…and so on around the ring (forever).•Remains to show: Starting from any state, we actually reach a configuration in which all the x values are the same.Lemma 2•Lemma 2: In every configuration, at least one of the potential x values, {0,…,n}, does not appear in any xi.•Proof: Obviously. There are are only n variables and n+1 values.Lemma 3•Lemma 3: In any fair execution fragment (from any configuration c), P1 changes x1 at least once every nl time.•Proof:–Assume not---P1 goes longer than nl without changing x1 from some value v.–Then by time l, P2 sets x2 to v,–By time 2l, P3 sets x3 to v,–…–By (n-1)l, Pn sets xn to v.–All these values remain = v, as long as x1 doesn’t change.–But then by time nl, P1 sees xn = x1, and changes x1.Lemma 4•Lemma 4: In any fair execution fragment , a configuration in which all the x values are the same (and so, a