% W.H. Hesselink, March-June 2010, version May 2012 % Mutual exclusion, according to E.A. Lycklama and V. Hadzilacos % ACM TOPLAS 13, 1991, pages 558-576 % A simplification with four nonatomic shared bits per thread % 21 {idle} ; threadset := allThreads ; turnset := allPairs ; % predec[p] := { q | central[q] } ; % 22 cc := (flickering) true ; % 23 for all k: turnset do copy[k] := turn[k] end ; % cnt := shacnt; shacnt ++ ; % 24 turn[p*R+nx] := (flickering) true ; central[p] := true ; % 25 cc[p] := (flickering) false ; % 26 while exists kk with copy[kk] do % 27 await NOT turn[kk] then copy[kk] := false ; % endwhile ; % 28 cc[p] := (flickering) true ; thr := 0 ; % 29 while thr < p do % if NOT cc[thr] then thr ++ % else % 30 cc[p] := (flickering) false ; % 31 await NOT cc[thr] then % endif % endwhile ; % 32 while thr < N do % await thr = p OR NOT cc[thr] then thr ++ % endwhile ; % 33 CS ; % 34 cc[p] := (flickering) false ; central[p] := false ; % 35 turn[p*R+nx] := (flickering) false ; incar++ ; % nx := (nx+1)%N ; goto 21. mx4bitSafe[N: posnat, R: posnat]: THEORY BEGIN Thread: TYPE = below(N) Version: TYPE = below(R) Pair: TYPE = [Thread, Version] kk: VAR Pair boundingpairs: LEMMA % used to prove the TCC of allpairs R*kk`1+kk`2 < R*N allpairs: finite_set[Pair] = fullset[Pair] allThreads: finite_set[Thread] = fullset[Thread] state: TYPE = [# % shared state cc: pred[Thread], turn: finite_set[Pair], shacnt: nat, central: pred[Thread], predec: [Thread -> setof[Thread]], % private state turnset, copy: [Thread -> finite_set[Pair]], pc, cnt, incar: [Thread -> nat], thr: [Thread -> upto(N)], kk: [Thread -> Pair], nx: [Thread -> Version] #] p, q, r: VAR Thread x, y: VAR state % Flickering steps cflickering(p, x): state = x WITH [ `cc(p) := NOT x`cc(p) ] stepCF(p, x, y): bool = (x`pc(p) = 22 OR x`pc(p) = 25 OR x`pc(p) = 28 OR x`pc(p) = 30 OR x`pc(p) = 34) AND y = cflickering(p, x) tuflickering(p, x): state = x WITH [ `turn(p, x`nx(p)) := NOT x`turn(p, x`nx(p)) ] stepTuF(p, x, y): bool = (x`pc(p) = 24 OR x`pc(p) = 35) AND y = tuflickering(p, x) % Program steps % The function next... serve in the proof of absence of deadlock. % They need care to avoid unprovable TCCs. next21(p, x): state = x WITH [ `predec(p) := x`central, `turnset(p) := allpairs, `pc(p) := 22 ] step21(p, x, y): bool = x`pc(p) = 21 AND y = next21(p, x) next22(p, x): state = x WITH [ `cc(p) := true, `pc(p) := 23 ] step22(p, x, y): bool = x`pc(p) = 22 AND y = next22(p, x) next23B(p, kk, x): state = x WITH [ `turnset(p) := remove(kk, x`turnset(p)), `copy(p)(kk) := x`turn(kk) ] step23B(p, x, y): bool = x`pc(p) = 23 AND EXISTS kk: x`turnset(p)(kk) AND y = next23B(p, kk, x) next23E(p, x): state = x WITH [ `cnt(p) := x`shacnt, `shacnt := x`shacnt + 1, `pc(p) := 24 ] step23E(p, x, y): bool = x`pc(p) = 23 AND empty?(x`turnset(p)) AND y = next23E(p, x) next24(p, x): state = x WITH [ `turn(p, x`nx(p)) := true, `central(p) := true, `pc(p) := 25 ] step24(p, x, y): bool = x`pc(p) = 24 AND y = next24(p, x) next25(p, x): state = x WITH [ `cc(p) := false, `pc(p) := 26 ] step25(p, x, y): bool = x`pc(p) = 25 AND y = next25(p, x) next26B(p, kk, x): state = x WITH [ `kk(p) := kk, `pc(p) := 27 ] step26B(p, x, y): bool = x`pc(p) = 26 AND EXISTS kk: x`copy(p)(kk) AND y = next26B(p, kk, x) next26E(p, x): state = x WITH [ `pc(p) := 28 ] step26E(p, x, y): bool = x`pc(p) = 26 AND empty?(x`copy(p)) AND y = next26E(p, x) next27(p, x): state = x WITH [ `copy(p) := remove(x`kk(p), x`copy(p)), `pc(p) := 26 ] step27(p, x, y): bool = x`pc(p) = 27 AND NOT x`turn(x`kk(p)) AND y = next27(p, x) next28(p, x): state = x WITH [ `cc(p) := true, `thr(p) := 0, `pc(p) := 29 ] step28(p, x, y): bool = x`pc(p) = 28 AND y = next28(p, x) next29B(p, x): state = x WITH [ `thr(p) := IF p <= x`thr(p) OR x`cc(x`thr(p)) THEN x`thr(p) ELSE x`thr(p)+1 ENDIF, `pc(p) := IF x`thr(p) < p AND x`cc(x`thr(p)) THEN 30 ELSE 29 ENDIF ] step29B(p, x, y): bool = x`pc(p) = 29 AND x`thr(p) < p AND y = next29B(p, x) next29E(p, x): state = x WITH [ `thr(p) := p+1, `pc(p) := 32 ] step29E(p, x, y): bool = x`pc(p) = 29 AND p <= x`thr(p) AND y = next29E(p, x) next30(p, x): state = x WITH [ `cc(p) := false, `pc(p) := 31 ] step30(p, x, y): bool = x`pc(p) = 30 AND y = next30(p, x) at(p, x): bool = x`thr(p) < N AND x`cc(x`thr(p)) next31(p, x): state = x WITH [ `pc(p) := 28 ] step31(p, x, y): bool = x`pc(p) = 31 AND NOT at(p, x) AND y = next31(p, x) next32B(p, x): state = x WITH [ `thr(p) := IF x`thr(p) < N THEN x`thr(p) + 1 ELSE 0 ENDIF ] step32B(p, x, y): bool = x`pc(p) = 32 AND x`thr(p) < N AND NOT x`cc(x`thr(p)) AND y = next32B(p, x) next32E(p, x): state = x WITH [ `pc(p) := 33 ] step32E(p, x, y): bool = x`pc(p) = 32 AND x`thr(p) = N AND y = next32E(p, x) next33(p, x): state = x WITH [ `pc(p) := 34 ] step33(p, x, y): bool = x`pc(p) = 33 AND y = next33(p, x) next34(p, x): state = x WITH [ `cc(p) := false, `central(p) := false, `predec := LAMBDA q: remove(p, x`predec(q)), `pc(p) := 35 ] step34(p, x, y): bool = x`pc(p) = 34 AND y = next34(p, x) m: VAR Version rotate(m): Version = IF m < R-1 THEN m+1 ELSE 0 ENDIF rotate_dif: LEMMA R > 1 IMPLIES rotate(m) /= m rotate_dif2: LEMMA R > 2 IMPLIES rotate(rotate(m)) /= m next35(p, x): state = x WITH [ `turn(p, x`nx(p)) := false, `nx(p) := rotate(x`nx(p)), `incar(p) := x`incar(p) + 1, `pc(p) := 21 ] step35(p, x, y): bool = x`pc(p) = 35 AND y = next35(p, x) step(p, x, y): bool = stepCF(p, x, y) OR stepTuF(p, x, y) OR step21(p, x, y) OR step22(p, x, y) OR step23B(p, x, y) OR step23E(p, x, y) OR step24(p, x, y) OR step25(p, x, y) OR step26B(p, x, y) OR step26E(p, x, y) OR step27(p, x, y) OR step28(p, x, y) OR step29B(p, x, y) OR step29E(p, x, y) OR step30(p, x, y) OR step31(p, x, y) OR step32B(p, x, y) OR step32E(p, x, y) OR step33(p, x, y) OR step34(p, x, y) OR step35(p, x, y) % Invariants acta(q, x): bool = x`pc(q) = 29 OR x`pc(q) = 32 OR x`pc(q) = 33 iq0(q, x): bool = acta(q, x) IMPLIES x`cc(q) iq0_step: LEMMA iq0(q, x) AND step(p, x, y) IMPLIES iq0(q, y) iq1(q, x): bool = 33 <= x`pc(q) IMPLIES N <= x`thr(q) iq1_step: LEMMA iq1(q, x) AND step(p, x, y) IMPLIES iq1(q, y) iq2(q, r, x): bool = acta(q, x) AND acta(r, x) AND q < x`thr(r) AND r < x`thr(q) IMPLIES q = r iq2_step_dif: LEMMA iq2(q, r, x) AND step(p, x, y) IMPLIES iq2(q, r, y) OR q = p OR r = p iq2_step_eq_rest: LEMMA iq2(p, r, x) AND step(p, x, y) IMPLIES iq2(p, r, y) OR step29B(p, x, y) OR step32B(p, x, y) iq2_step_eq29: LEMMA iq2(p, r, x) AND step29B(p, x, y) AND iq0(p, x) AND iq0(r, x) IMPLIES iq2(p, r, y) iq2_step_eq32: LEMMA iq2(p, r, x) AND step32B(p, x, y) AND iq0(p, x) AND iq0(r, x) IMPLIES iq2(p, r, y) iq2_step_eq: LEMMA iq2(p, r, x) AND step(p, x, y) AND iq0(p, x) AND iq0(r, x) IMPLIES iq2(p, r, y) iq2_step: LEMMA iq2(q, r, x) AND step(p, x, y) AND iq0(q, x) AND iq0(r, x) IMPLIES iq2(q, r, y) mx(q, r, x): bool = x`pc(q) = 33 AND x`pc(r) = 33 IMPLIES q = r mx_implied: LEMMA iq2(q, r, x) AND iq1(q, x) AND iq1(r, x) IMPLIES mx(q, r, x) iq3(q, x): bool = x`pc(q) = 32 IMPLIES q < x`thr(q) iq3_step: LEMMA iq3(q, x) AND step(p, x, y) IMPLIES iq3(q, y) ijqall(x): bool = (FORALL q: iq0(q, x) AND iq1(q, x) AND iq3(q, x)) AND (FORALL q, r: iq2(q, r, x)) ijqall_step: LEMMA ijqall(x) AND step(p, x, y) IMPLIES ijqall(y) kq0(q, x): bool = x`central(q) IFF 25 <= x`pc(q) AND x`pc(q) <= 34 kq0_step: LEMMA kq0(q, x) AND step(p, x, y) IMPLIES kq0(q, y) kq1(q, r, x): bool = x`predec(q)(r) IMPLIES x`turnset(q)(r, x`nx(r)) OR x`copy(q)(r, x`nx(r)) kq4(q, r, x): bool = x`predec(q)(r) IMPLIES x`central(r) kq5(q, x): bool = x`central(q) IMPLIES x`turn(q, x`nx(q)) kq1_step_rest: LEMMA kq1(q, r, x) AND step(p, x, y) IMPLIES kq1(q, r, y) OR step23B(p, x, y) OR step27(p, x, y) OR step35(p, x, y) kq1_step_23: LEMMA kq1(q, r, x) AND step23B(p, x, y) AND kq4(q, r, x) AND kq5(r, x) IMPLIES kq1(q, r, y) kq1_step_27: LEMMA kq1(q, r, x) AND step27(p, x, y) AND kq4(q, r, x) AND kq5(r, x) IMPLIES kq1(q, r, y) kq1_step_35: LEMMA kq1(q, r, x) AND step35(p, x, y) AND kq4(q, r, x) AND kq0(r, x) IMPLIES kq1(q, r, y) kq1_step: LEMMA kq1(q, r, x) AND step(p, x, y) AND kq4(q, r, x) AND kq5(r, x) AND kq0(r, x) IMPLIES kq1(q, r, y) kq2(q, x): bool = 22 <= x`pc(q) AND x`pc(q) <= 23 OR empty?(x`turnset(q)) kq2_step: LEMMA kq2(q, x) AND step(p, x, y) IMPLIES kq2(q, y) kq3(q, x): bool = 23 <= x`pc(q) AND x`pc(q) <= 27 OR empty?(x`copy(q)) kq3_step: LEMMA kq3(q, x) AND step(p, x, y) IMPLIES kq3(q, y) kq4_step: LEMMA kq4(q, r, x) AND step(p, x, y) IMPLIES kq4(q, r, y) kq5_step_rest: LEMMA kq5(q, x) AND step(p, x, y) IMPLIES kq5(q, y) OR step24(p, x, y) OR step35(p, x, y) OR stepTuF(p, x, y) kq5_step_list: LEMMA kq5(q, x) AND (step24(p, x, y) OR step35(p, x, y) OR stepTuF(p, x, y)) AND kq0(q, x) IMPLIES kq5(q, y) kq5_step: LEMMA kq5(q, x) AND step(p, x, y) AND kq0(q, x) IMPLIES kq5(q, y) kqall(x): bool = (FORALL q: kq2(q, x) AND kq3(q, x) AND kq5(q, x) AND kq0(q, x)) AND (FORALL q, r: kq1(q, r, x) AND kq4(q, r, x)) kqall_step: LEMMA kqall(x) AND step(p, x, y) IMPLIES kqall(y) fcfs(q, x): bool = % FCFS empty?(x`predec(q)) OR 22 <= x`pc(q) AND x`pc(q) <= 27 fcfs_implied_by_kqall: LEMMA kqall(x) IMPLIES fcfs(q, x) lq0(q, x): bool = x`cc(q) IMPLIES 22 <= x`pc(q) AND x`pc(q) <= 25 OR 28 <= x`pc(q) AND x`pc(q) <= 30 OR 32 <= x`pc(q) AND x`pc(q) <= 34 lq0_step: LEMMA lq0(q, x) AND step(p, x, y) IMPLIES lq0(q, y) lq1(q, x): bool = x`pc(q) = 27 IMPLIES x`copy(q)(x`kk(q)) lq1_step: LEMMA lq1(q, x) AND step(p, x, y) IMPLIES lq1(q, y) lq2(kk, x): bool = x`turn(kk) IMPLIES 24 <= x`pc(kk`1) AND x`nx(kk`1) = kk`2 lq2_step: LEMMA lq2(kk, x) AND step(p, x, y) IMPLIES lq2(kk, y) lq3(q, kk, x): bool = x`copy(q)(kk) AND 24 <= x`pc(q) AND x`nx(kk`1) = kk`2 IMPLIES x`cnt(kk`1) < x`cnt(q) mq0(q, x): bool = x`cnt(q) < x`shacnt mq4(q, kk, x): bool = x`copy(q)(kk) AND x`nx(kk`1) = kk`2 IMPLIES 24 <= x`pc(kk`1) aq1(q, kk, x): bool = %% should become mq3A x`copy(q)(kk) AND rotate(x`nx(kk`1)) = kk`2 IMPLIES 21 <= x`pc(kk`1) AND x`pc(kk`1) <= 27 lq3_step_rest: LEMMA lq3(q, kk, x) AND step(p, x, y) IMPLIES lq3(q, kk, y) OR step23E(p, x, y) OR step35(p, x, y) lq3_step_23: LEMMA lq3(q, kk, x) AND step23E(p, x, y) AND mq4(q, kk, x) AND mq0(kk`1, x) IMPLIES lq3(q, kk, y) lq3_step_35: LEMMA lq3(q, kk, x) AND step35(p, x, y) AND aq1(q, kk, x) IMPLIES lq3(q, kk, y) lq3_step: LEMMA lq3(q, kk, x) AND step(p, x, y) AND mq4(q, kk, x) AND mq0(kk`1, x) AND aq1(q, kk, x) IMPLIES lq3(q, kk, y) lq4(q, x): bool = 21 <= x`pc(q) AND x`pc(q) <= 35 lq4_step: LEMMA lq4(q, x) AND step(p, x, y) IMPLIES lq4(q, y) % At this point, we begin a bottom-up approach. mq0_step: LEMMA mq0(q, x) AND step(p, x, y) IMPLIES mq0(q, y) mq1(q, x): bool = 23 <= x`pc(q) AND x`pc(q) <= 24 IMPLIES x`cc(q) mq1_step: LEMMA mq1(q, x) AND step(p, x, y) IMPLIES mq1(q, y) lqall(x): bool = (FORALL q: lq4(q, x) AND lq0(q, x) AND lq1(q, x) AND mq0(q, x) AND mq1(q, x)) AND (FORALL kk: lq2(kk, x)) lqall_step: LEMMA lqall(x) AND step(p, x, y) IMPLIES lqall(y) mq2(q, kk, x): bool = 23 <= x`pc(q) AND x`pc(q) <= 24 AND x`copy(q)(kk) AND x`nx(kk`1) /= kk`2 IMPLIES x`nx(kk`1) = rotate(kk`2) AND x`pc(kk`1) <= 32 AND (x`pc(kk`1) <= 28 OR x`thr(kk`1) <= q) mq2A(q, kk, x): bool = 23 <= x`pc(q) AND x`pc(q) <= 24 AND x`copy(q)(kk) IMPLIES rotate(x`nx(kk`1)) /= kk`2 mq2A_implied: LEMMA mq2(q, kk, x) AND R >= 3 IMPLIES mq2A(q, kk, x) mq2_step_rest: LEMMA mq2(q, kk, x) AND step(p, x, y) IMPLIES mq2(q, kk, y) OR step22(p, x, y) OR step23B(p, x, y) OR step29B(p, x, y) OR step32B(p, x, y) mq2_step_22: LEMMA mq2(q, kk, x) AND step22(p, x, y) AND kq3(q, x) IMPLIES mq2(q, kk, y) mq2_step_23: LEMMA mq2(q, kk, x) AND step23B(p, x, y) AND lq2(kk, x) IMPLIES mq2(q, kk, y) mq2_step_29: LEMMA mq2(q, kk, x) AND step29B(p, x, y) AND mq1(q, x) IMPLIES mq2(q, kk, y) mq2_step_32: LEMMA mq2(q, kk, x) AND step32B(p, x, y) AND mq1(q, x) IMPLIES mq2(q, kk, y) mq2_step: LEMMA mq2(q, kk, x) AND step(p, x, y) AND kq3(q, x) AND lq2(kk, x) AND mq1(q, x) IMPLIES mq2(q, kk, y) mq3(q, kk, x): bool = x`copy(q)(kk) AND rotate(x`nx(kk`1)) = kk`2 IMPLIES x`pc(kk`1) = 21 OR x`predec(kk`1)(q) mq3_step_rest: LEMMA mq3(q, kk, x) AND step(p, x, y) IMPLIES mq3(q, kk, y) OR step21(p, x, y) OR step23B(p, x, y) OR step34(p, x, y) mq3_step_21: LEMMA mq3(q, kk, x) AND step21(p, x, y) AND mq2(q, kk, x) AND R > 2 AND kq3(q, x) AND kq0(q, x) IMPLIES mq3(q, kk, y) mq3_step_23B: LEMMA mq3(q, kk, x) AND step23B(p, x, y) AND lq2(kk, x) AND R > 1 IMPLIES mq3(q, kk, y) mq3_step_34: LEMMA mq3(q, kk, x) AND step34(p, x, y) AND kq3(q, x) IMPLIES mq3(q, kk, y) mq3_step: LEMMA mq3(q, kk, x) AND step(p, x, y) AND mq2(q, kk, x) AND lq2(kk, x) AND R > 2 AND kq3(q, x) AND kq0(q, x) IMPLIES mq3(q, kk, y) aq1_implied: LEMMA fcfs(kk`1, x) AND mq3(q, kk, x) IMPLIES aq1(q, kk, x) mq4_step_rest: LEMMA mq4(q, kk, x) AND step(p, x, y) IMPLIES mq4(q, kk, y) OR step23B(p, x, y) OR step35(p, x, y) mq4_step_23: LEMMA mq4(q, kk, x) AND step23B(p, x, y) AND lq2(kk, x) IMPLIES mq4(q, kk, y) mq4_step_35: LEMMA mq4(q, kk, x) AND step35(p, x, y) AND aq1(q, kk, x) IMPLIES mq4(q, kk, y) mq4_step: LEMMA mq4(q, kk, x) AND step(p, x, y) AND lq2(kk, x) AND aq1(q, kk, x) IMPLIES mq4(q, kk, y) mqall(x): bool = R > 2 AND (FORALL q, kk: lq3(q, kk, x) AND mq4(q, kk, x) AND mq3(q, kk, x) AND mq2(q, kk, x) ) mqall_step: LEMMA mqall(x) AND step(p, x, y) AND kqall(x) AND lqall(x) IMPLIES mqall(y) globinv(x): bool = ijqall(x) AND kqall(x) AND lqall(x) AND mqall(x) globinv_step: THEOREM globinv(x) AND step(p, x, y) IMPLIES globinv(y) fcfs_implied: LEMMA globinv(x) IMPLIES fcfs(q, x) mx_implied_again: LEMMA globinv(x) IMPLIES mx(q, r, x) % Initialization initstate: state = (# % shared state cc:= emptyset[Thread], turn:= emptyset[Pair], shacnt:= 1, central := emptyset[Thread], predec:= (LAMBDA q: emptyset[Thread]), % private state turnset:= (LAMBDA q: emptyset[Pair]), copy:= (LAMBDA q: emptyset[Pair]), pc:= (LAMBDA q: 21), cnt:= (LAMBDA q: 0), incar:= (LAMBDA q: 0), thr:= (LAMBDA q: 0), kk:= (LAMBDA q: (0,0)), nx:= (LAMBDA q: 0) #) init(x): bool = R > 2 AND x`cc = emptyset[Thread] AND x`turn = emptyset[Pair] AND x`central = emptyset[Thread] AND FORALL q: x`predec(q) = emptyset[Thread] AND x`turnset(q) = emptyset[Pair] AND x`copy(q) = emptyset[Pair] AND x`pc(q) = 21 AND x`cnt(q) < x`shacnt % AND x`thr(q) <= N init_initstate: LEMMA R > 2 IMPLIES init(initstate) globinv_init: LEMMA init(x) IMPLIES globinv(x) % Absence of deadlock otherstep(p, x, y): bool = step21(p, x, y) OR stepCF(p, x, y) OR stepTuF(p, x, y) forwardstep(p)(x, y): bool = % step22(p, x, y) OR step23B(p, x, y) OR step23E(p, x, y) OR step24(p, x, y) OR step25(p, x, y) OR step26B(p, x, y) OR step26E(p, x, y) OR step27(p, x, y) OR step28(p, x, y) OR step29B(p, x, y) OR step29E(p, x, y) OR step30(p, x, y) OR step31(p, x, y) OR step32B(p, x, y) OR step32E(p, x, y) OR step33(p, x, y) OR step34(p, x, y) OR step35(p, x, y) step_dichotomy: LEMMA forwardstep(p)(x, y) OR otherstep(p, x, y) IFF step(p, x, y) disabled(p)(x): bool = x`pc(p) = 21 OR (x`pc(p) = 27 AND x`turn(x`kk(p))) OR (31 <= x`pc(p) AND x`pc(p) <= 32 AND at(p,x)) disabled_not_forward: LEMMA disabled(p)(x) AND iq3(p, x) IMPLIES NOT EXISTS y: forwardstep(p)(x, y) disabled_or_enabled: LEMMA lq4(p, x) IMPLIES disabled(p)(x) OR EXISTS y: forwardstep(p)(x, y) disabled_eq_fwd_disabled: LEMMA globinv(x) IMPLIES disabled(p)(x) = NOT EXISTS y: forwardstep(p)(x, y) stopped(x): bool = FORALL p: disabled(p)(x) stopped_implies_not_cc: LEMMA stopped(x) AND globinv(x) IMPLIES FORALL q: NOT x`cc(q) stopped_implies21or27: LEMMA stopped(x) AND globinv(x) IMPLIES FORALL q: x`pc(q) = 21 OR x`pc(q) = 27 stopped_implies_idle: THEOREM stopped(x) AND globinv(x) IMPLIES FORALL q: x`pc(q) = 21 END mx4bitSafe