% Wim H. Hesselink, September-October 2010 % Lamport's Bakery Mutual Exclusion Algorithm % Version June 2012 bakery0: THEORY BEGIN N: posnat Process: TYPE = below(N) allproc: finite_set[Process] = fullset[Process] % shavar num: Process -> int, act: Process -> bool % privar set1, set2, set3, qq, lev % 10: NCS ; predec[p] := {q | q in [16..19] % 11: act[p] := (flickering) true ; lev := 0 ; % 12: set1 := fullset ; % 13: while nonempty?(set1) do % extract some r from set1 ; % lev := max(lev, num[r]) ; % od ; % 14: num[p] := (flickering) lev + 1; % 15: act[p] := (flickering) false ; % 16: set2 := set3 := fullset ; % 17: while nonempty?(set2) do % choose some qq in set2 ; % 18: if qq in set3 then % await not act[qq] ; remove qq from set3 % else % await num[qq] <= 0 OR (num[p],p) <= (num[qq],qq) ; % remove qq from set2 % fi % od ; % 19: CS ; % for all q do predec[q] := predec[q] - {p} ; % 20: num[p] := (flickering) 0 ; cnt := cnt + 1 ; % goto 10 . % Fault tolerance: from any location: % num[p] := arbitrary ; act[p] := arbitrary ; % for all q do predec[q] := predec[q] - {p} ; predec/[p] := empty ; % goto 21 . % 21: act[p] := (flickering) false ; goto 20. state: TYPE = [# % shared variables num: [Process -> nat], act: pred[Process], predec: [Process -> set[Process]], % private variables qq: [Process -> Process], set1, set2, set3: [Process -> finite_set[Process]], pc, lev, cnt: [Process -> nat] #] p, q, r: VAR Process x, y: VAR state n: VAR nat b: VAR bool init(x): bool = FORALL q: x`pc(q) = 10 AND NOT x`act(q) AND x`num(q) = 0 AND empty?(x`predec(q)) goto(p, n, x): state = x WITH [ `pc(p) := n ] flickact(p, x): state = x WITH [`act(p) := NOT x`act(p)] stepFact(p, x, y): bool = (x`pc(p) = 11 OR x`pc(p) = 15 OR x`pc(p) = 21) AND y = flickact(p, x) flicknum(p, n, x): state = x WITH [`num(p) := n] stepFnum(p, x, y): bool = x`pc(p) = 14 AND EXISTS n: y = flicknum(p, n, x) stepFnumR(p, x, y): bool = x`pc(p) = 20 AND EXISTS n: y = flicknum(p, n, x) next10(p, x): state = x WITH [ `predec(p) := {q | 16 <= x`pc(q) AND x`pc(q) <= 19}, `pc(p) := 11 ] step10(p, x, y): bool = % NCS x`pc(p) = 10 AND y = next10(p, x) next11(p, x): state = x WITH [ `lev(p) := 0, `act(p) := true, `pc(p) := 12 ] step11(p, x, y): bool = x`pc(p) = 11 AND y = next11(p, x) next12(p, x): state = x WITH [ `set1(p) := allproc, `pc(p) := 13 ] step12(p, x, y): bool = x`pc(p) = 12 AND y = next12(p, x) next13(p, q, x): state = x WITH [ `set1(p) := remove(q, x`set1(p)) , `lev(p) := max(x`lev(p), x`num(q)) ] step13B(p, x, y): bool = x`pc(p) = 13 AND EXISTS q: x`set1(p)(q) AND y = next13(p, q, x) step13E(p, x, y): bool = x`pc(p) = 13 AND empty?(x`set1(p)) AND y = goto(p, 14, x) next14(p, x):state = x WITH [ `num(p) := 1+x`lev(p), `pc(p) := 15 ] step14(p, x, y): bool = x`pc(p) = 14 AND y = next14(p, x) next15(p, x): state = x WITH [ `act(p) := false, `pc(p) := 16 ] step15(p, x, y): bool = x`pc(p) = 15 AND y = next15(p, x) next16(p, x): state = x WITH [ `set3(p) := allproc, `set2(p) := allproc, `pc(p) := 17 ] step16(p, x, y): bool = x`pc(p) = 16 AND y = next16(p, x) next17(p, q, x): state = x WITH [ `qq(p) := q, `pc(p) := 18 ] step17B(p, x, y): bool = x`pc(p) = 17 AND EXISTS q: x`set2(p)(q) AND y = next17(p, q, x) step17E(p, x, y): bool = x`pc(p) = 17 AND empty?(x`set2(p)) AND y = goto(p, 19, x) next18(p, x): state = x WITH [ `set3(p) := IF x`set3(p)(x`qq(p)) THEN remove(x`qq(p), x`set3(p)) ELSE x`set3(p) ENDIF, `set2(p) := IF x`set3(p)(x`qq(p)) THEN x`set2(p) ELSE remove(x`qq(p), x`set2(p)) ENDIF, `pc(p) := 17 ] step18(p, x, y): bool = x`pc(p) = 18 AND IF x`set3(p)(x`qq(p)) THEN NOT x`act(x`qq(p)) ELSE x`num(x`qq(p)) = 0 OR x`num(p) < x`num(x`qq(p)) OR x`num(p) = x`num(x`qq(p)) AND p <= x`qq(p) ENDIF AND y = next18(p, x) next19(p, x): state = x WITH [ `predec := (LAMBDA q: remove(p, x`predec(q))), `pc(p) := 20 ] step19(p, x, y): bool = % CS x`pc(p) = 19 AND y = next19(p, x) next21(p, x): state = x WITH [ `act(p) := false, `pc(p) := 20 ] step21(p, x, y): bool = x`pc(p) = 21 AND y = next21(p, x) next20(p, x): state = x WITH [ `num(p) := 0, `cnt(p) := x`cnt(p) + 1, `pc(p) := 10 ] step20(p, x, y): bool = x`pc(p) = 20 AND y = next20(p, x) nextFault(p, n, b, x): state = x WITH [ `predec := (LAMBDA q: IF q = p THEN emptyset ELSE remove(p, x`predec(q)) ENDIF), `set1(p) := emptyset, `set3(p) := emptyset, `set2(p) := emptyset, `num(p) := n, `act(p) := b, `pc(p) := 21 ] stepFault(p, x, y): bool = % Fault EXISTS n, b: y = nextFault(p, n, b, x) step(p, x, y): bool = stepFact(p, x, y) OR stepFnum(p, x, y) OR stepFnumR(p, x, y) OR step10(p, x, y) OR step11(p, x, y) OR step12(p, x, y) OR step13B(p, x, y) OR step13E(p, x, y) OR step14(p, x, y) OR step15(p, x, y) OR step16(p, x, y) OR step17B(p, x, y) OR step17E(p, x, y) OR step18(p, x, y) OR step19(p, x, y) OR step21(p, x, y) OR step20(p, x, y) OR stepFault(p, x, y) forwardstep(p, x, y): bool = step11(p, x, y) OR step12(p, x, y) OR step13B(p, x, y) OR step13E(p, x, y) OR step14(p, x, y) OR step15(p, x, y) OR step16(p, x, y) OR step17B(p, x, y) OR step17E(p, x, y) OR step18(p, x, y) OR step19(p, x, y) OR step21(p, x, y) OR step20(p, x, y) otherstep(p, x, y): bool = stepFact(p, x, y) OR stepFnum(p, x, y) OR stepFnumR(p, x, y) OR step10(p, x, y) OR stepFault(p, x, y) step_dichotomy: LEMMA step(p, x, y) IFF (forwardstep(p, x, y) OR otherstep(p, x, y)) mx(q, r, x): bool = x`pc(q) = 19 AND x`pc(r) = 19 IMPLIES q = r iq0(q, r, x): bool = 17 <= x`pc(q) AND x`pc(q) <= 19 AND 15 <= x`pc(r) AND x`pc(r) <= 19 IMPLIES x`set2(q)(r) OR x`num(q) < x`num(r) OR x`num(q) = x`num(r) AND q <= r iq1(q, x): bool = x`pc(q) = 19 IMPLIES empty?(x`set2(q)) mx_implied: LEMMA iq0(q, r, x) AND iq1(q, x) AND iq0(r, q, x) AND iq1(r, x) IMPLIES mx(q, r, x) iq2(q, r, x): bool = 17 <= x`pc(q) AND x`pc(q) <= 19 AND 13 <= x`pc(r) AND x`pc(r) <= 14 IMPLIES x`set2(q)(r) OR x`set1(r)(q) OR x`num(q) <= x`lev(r) iq3(q, x): bool = empty?(x`set1(q)) OR x`pc(q) <= 13 iq4(q, x): bool = 15 <= x`pc(q) AND x`pc(q) <= 19 IMPLIES x`num(q) > 0 iq5(q, x): bool = x`pc(q) <= 13 IMPLIES x`num(q) = 0 iq0_step_rest: LEMMA iq0(q, r, x) AND step(p, x, y) IMPLIES iq0(q, r, y) OR step14(p, x, y) OR step18(p, x, y) iq0_step_14: LEMMA iq0(q, r, x) AND step14(p, x, y) AND iq2(q, r, x) AND iq3(r, x) IMPLIES iq0(q, r, y) iq0_step_18: LEMMA iq0(q, r, x) AND step18(p, x, y) AND iq4(r, x) AND iq5(r, x) IMPLIES iq0(q, r, y) iq0_step: LEMMA iq0(q, r, x) AND step(p, x, y) AND iq2(q, r, x) AND iq3(r, x) AND iq4(r, x) AND iq5(r, x) IMPLIES iq0(q, r, y) iq1_step: LEMMA iq1(q, x) AND step(p, x, y) IMPLIES iq1(q, y) iq6(q, r, x): bool = 17 <= x`pc(q) AND x`pc(q) <= 18 AND 13 <= x`pc(r) AND x`pc(r) <= 14 IMPLIES x`set3(q)(r) OR x`set1(r)(q) OR x`num(q) <= x`lev(r) iq2_step_rest: LEMMA iq2(q, r, x) AND step(p, x, y) IMPLIES iq2(q, r, y) OR step18(p, x, y) iq2_step_18: LEMMA iq2(q, r, x) AND step18(p, x, y) AND iq6(q, r, x) IMPLIES iq2(q, r, y) iq2_step: LEMMA iq2(q, r, x) AND step(p, x, y) AND iq6(q, r, x) IMPLIES iq2(q, r, y) iq3_step: LEMMA iq3(q, x) AND step(p, x, y) IMPLIES iq3(q, y) iq4_step: LEMMA iq4(q, x) AND step(p, x, y) IMPLIES iq4(q, y) iq5_step: LEMMA iq5(q, x) AND step(p, x, y) IMPLIES iq5(q, y) iq7(q, x): bool = 12 <= x`pc(q) AND x`pc(q) <= 14 IMPLIES x`act(q) iq6_step_rest: LEMMA iq6(q, r, x) AND step(p, x, y) IMPLIES iq6(q, r, y) OR step18(p, x, y) iq6_step_18: LEMMA iq6(q, r, x) AND step18(p, x, y) AND iq7(r, x) IMPLIES iq6(q, r, y) iq6_step: LEMMA iq6(q, r, x) AND step(p, x, y) AND iq7(r, x) IMPLIES iq6(q, r, y) iq7_step: LEMMA iq7(q, x) AND step(p, x, y) IMPLIES iq7(q, y) iq8(q, x): bool = 10 <= x`pc(q) AND x`pc(q) <= 21 iq8_step: LEMMA iq8(q, x) AND step(p, x, y) IMPLIES iq8(q, y) iq9(q, x): bool = x`act(q) IMPLIES 11 <= x`pc(q) AND x`pc(q) <= 15 OR x`pc(q) = 21 iq9_step: LEMMA iq9(q, x) AND step(p, x, y) IMPLIES iq9(q, y) iqall(x): bool = (FORALL q: iq1(q, x) AND iq4(q, x) AND iq3(q, x) AND iq8(q, x) AND iq5(q, x) AND iq7(q, x) AND iq9(q, x)) AND (FORALL q, r: iq0(q, r, x) AND iq2(q, r, x) AND iq6(q, r, x)) iqall_implies_mx: LEMMA iqall(x) IMPLIES mx(q, r, x) iqall_step: LEMMA iqall(x) AND step(p, x, y) IMPLIES iqall(y) iqall_start: LEMMA init(x) IMPLIES iqall(x) idle(x): bool = FORALL p: x`pc(p) = 10 fwdenabled(p, x): bool = 11 <= x`pc(p) AND x`pc(p) <= 21 AND (x`pc(p) = 18 IMPLIES IF x`set3(p)(x`qq(p)) THEN NOT x`act(x`qq(p)) ELSE x`num(x`qq(p)) = 0 OR x`num(p) < x`num(x`qq(p)) OR x`num(p) = x`num(x`qq(p)) AND p <= x`qq(p) ENDIF ) fwdenabled_equiv: LEMMA fwdenabled(p, x) IFF (EXISTS y: forwardstep(p, x, y)) no_deadlock: LEMMA iqall(x) IMPLIES idle(x) OR EXISTS p: fwdenabled(p, x) fcfs(q, x): bool = x`pc(q) = 19 IMPLIES empty?(x`predec(q)) kq0(q, r, x): bool = 17 <= x`pc(q) AND x`predec(q)(r) IMPLIES x`set2(q)(r) fcfs_implied: LEMMA (FORALL r: kq0(q, r, x)) AND iq1(q, x) IMPLIES fcfs(q, x) kq1(q, r, x): bool = x`predec(q)(r) IMPLIES 16 <= x`pc(r) AND x`pc(r) <= 19 kq2(q, r, x): bool = 15 <= x`pc(q) AND x`pc(q) <= 18 AND x`predec(q)(r) IMPLIES x`num(r)+1 <= x`num(q) kq0_rest: LEMMA kq0(q, r, x) AND step(p, x, y) IMPLIES kq0(q, r, y) OR step18(p, x, y) kq0_18: LEMMA kq0(q, r, x) AND step18(p, x, y) AND kq1(q, r, x) AND kq2(q, r, x) AND iq4(r, x) IMPLIES kq0(q, r, y) kq0_step: LEMMA kq0(q, r, x) AND step(p, x, y) AND kq1(q, r, x) AND kq2(q, r, x) AND iq4(r, x) IMPLIES kq0(q, r, y) kq1_step: LEMMA kq1(q, r, x) AND step(p, x, y) IMPLIES kq1(q, r, y) kq3(q, r, x): bool = 13 <= x`pc(q) AND x`pc(q) <= 14 AND x`predec(q)(r) IMPLIES x`set1(q)(r) OR x`num(r) <= x`lev(q) kq2_rest: LEMMA kq2(q, r, x) AND step(p, x, y) IMPLIES kq2(q, r, y) OR stepFnum(p, x, y) OR step14(p, x, y) OR stepFnumR(p, x, y) OR step20(p, x, y) kq2_Fnum: LEMMA kq2(q, r, x) AND stepFnum(p, x, y) AND kq1(q, r, x) IMPLIES kq2(q, r, y) kq2_FnumR: LEMMA kq2(q, r, x) AND stepFnumR(p, x, y) AND kq1(q, r, x) IMPLIES kq2(q, r, y) kq2_14: LEMMA kq2(q, r, x) AND step14(p, x, y) AND kq1(q, r, x) AND kq3(q, r, x) AND iq3(q, x) IMPLIES kq2(q, r, y) kq2_20: LEMMA kq2(q, r, x) AND step20(p, x, y) AND kq1(q, r, x) IMPLIES kq2(q, r, y) kq2_step: LEMMA kq2(q, r, x) AND step(p, x, y) AND kq1(q, r, x) AND kq3(q, r, x) AND iq3(q, x) IMPLIES kq2(q, r, y) kq3_rest: LEMMA kq3(q, r, x) AND step(p, x, y) IMPLIES kq3(q, r, y) OR stepFnum(p, x, y) OR stepFnumR(p, x, y) OR step14(p, x, y) kq3_Fnum: LEMMA kq3(q, r, x) AND stepFnum(p, x, y) AND kq1(q, r, x) IMPLIES kq3(q, r, y) kq3_FnumR: LEMMA kq3(q, r, x) AND stepFnumR(p, x, y) AND kq1(q, r, x) IMPLIES kq3(q, r, y) kq3_14: LEMMA kq3(q, r, x) AND step14(p, x, y) AND kq1(q, r, x) IMPLIES kq3(q, r, y) kq3_step: LEMMA kq3(q, r, x) AND step(p, x, y) AND kq1(q, r, x) IMPLIES kq3(q, r, y) kq4(q, x): bool = x`pc(q) = 18 IMPLIES x`set2(q)(x`qq(q)) kq4_step: LEMMA kq4(q, x) AND step(p, x, y) IMPLIES kq4(q, y) kqall(x): bool = (FORALL q: kq4(q, x)) AND (FORALL q, r: kq0(q, r, x) AND kq1(q, r, x) AND kq2(q, r, x) AND kq3(q, r, x) ) globinv(x): bool = iqall(x) AND kqall(x) fcfs_again: LEMMA globinv(x) IMPLIES fcfs(q, x) kqall_step: LEMMA globinv(x) AND step(p, x, y) IMPLIES kqall(y) kqall_start: LEMMA init(x) IMPLIES kqall(x) globinv_step: LEMMA globinv(x) AND step(p, x, y) IMPLIES globinv(y) globinv_start: LEMMA init(x) IMPLIES globinv(x) vf(p, x): nat = card(x`set1(p)) + card(x`set2(p)) + card(x`set3(p)) vf_equal_dif: LEMMA step(p, x, y) IMPLIES vf(q, x) = vf(q, y) OR q = p vf_descends_eq: LEMMA step(p, x, y) IMPLIES vf(p, y) <= vf(p, x) OR x`pc(p) = 12 OR x`pc(p) = 16 vf_decreases_18: LEMMA step18(p, x, y) AND kq4(p, x) IMPLIES vf(p, y) < vf(p, x) END bakery0