% Model of the digital circuitry described in % % A fault-tolerant digital clocking system % William M. Daly % Albert L. Hopkins, jr., % John F. McKena % MIT Draper Lab % Results: % ------- % We can prove eventually clocks do synchronize, but ASSUMING % that the faulty clock does not CHANGE more than once at a % given time instant; i.e. it is not allowed to change too fast. % In particular, we should ADD a test -- each clock element % makes sure that other clock elements do not send it different % values too soon. % Model with symmetric fault is v6 % Model with byzantine fault is v7 % In v7, properties are proved assuming G(timeAdvance>0 OR X(timeAdvance>0)) % which is a strong way to say that the faulty clock does not change its % value too often % In v8, we improve this model of faulty clock. % It is still not fully exact. % % Details: % -------- % Idea: asynchronous events that are epsilon time units % apart will be treated as synchronized. (time abstraction). % each digital element has 2 flip-flops and 2-timers. % state: z12a, z12b: BOOLEAN state in the flip flop % for timers: each timer has a deadline variable % z10, z11: { notset, t860, t200 } let us have a integer number % qnmf = is defined from the values of the n clocks... % dynamics: state updated at every event % each digital element sees if it has one of these events. % event: leadingEdgeQnmf, fallingEdgeQfp1, % event: leadingEdgeQfp1, fallingEdgeQnmf, % event: z10 % draperClockv8: CONTEXT = BEGIN % The system has two parameters: % f is the number of faulty clocks % N is the number of non-faulty clocks. % We verify the system for different values of N and f. % We assume N+f >= 3*f+1 N: NATURAL = 3 ; % number of NON-FAULTY nodes f: NATURAL = 1 ; % number of faulty nodes Node: TYPE = [1 .. N] ; tMax: NATURAL = 11 ; % one-shot multivibrator z10 time period tMin: NATURAL = 3 ; % one-shot multivibrator z11 time period Time: TYPE = [-1 .. tMax] ; min(x: ARRAY [1..N] OF Time, y: ARRAY [1..N] OF Time, i:[0..N], a:Time): Time = IF i = N AND a = tMax THEN 0 ELSIF i = N THEN a ELSIF (x[i+1] < y[i+1] OR y[i+1] = -1) AND x[i+1] < a AND x[i+1] > 0 THEN min(x, y, i+1, x[i+1]) ELSIF (x[i+1] >= y[i+1] OR x[i+1] = -1) AND y[i+1] < a AND y[i+1] > 0 THEN min(x, y, i+1, y[i+1]) ELSE min(x, y, i+1, a) ENDIF; sum(x: ARRAY [1..N] OF BOOLEAN, i: [0..N], a: [0..N] ): [0..N] = IF i = N THEN a ELSIF x[i+1] THEN sum(x, i+1, a+1) ELSE sum(x, i+1, a) ENDIF; % Q_b^r where s is the sum of all 1's in x q(b: [1..N], s: [0..N]): [BOOLEAN -> BOOLEAN] = IF (s >= b) THEN { TRUE } ELSIF (s + f < b) THEN { FALSE } ELSE { TRUE, FALSE } ENDIF ; % The state of the system consists of % c: ARRAY [1..N] OF BOOLEAN % qrmf,qfp1: ARRAY [1..N] OF BOOLEAN % qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r % % c is the array that stores the clock value for each of % the N non-faulty clocks. The value is either TRUE (1) % or FALSE (0). Note that we do not keep the state of the % faulty clocks since it is irrelevant. This leads to a % smaller (and easily model checkable) model. % % The quorum function % Q(b,a) is defined so that it has value 1 if a or more its % b inputs are 1, and is 0 otherwise. % % qfp1 is the quorum function Q(N+f, f+1). % qnmf is the quorum function Q(N+f, N). calculator: MODULE = BEGIN INPUT c: ARRAY [1 .. N] OF BOOLEAN INPUT z10, z11: ARRAY [1 .. N] OF Time OUTPUT qnmf, qfp1: ARRAY [1 .. N] of BOOLEAN OUTPUT timeAdvance: Time LOCAL smin: [1 .. N] LOCAL faultc: ARRAY Node OF [0 .. 1] INITIALIZATION faultc = [ [i:Node] 0]; qnmf = [ [i:[1..N]] FALSE ]; qfp1 = [ [i:[1..N]] FALSE ]; timeAdvance = 0 DEFINITION smin = sum(c, 0, 0) ; TRANSITION [ % The following model forces the faulty clock to make ATMOST ONE change % at ONE time instant timeAdvance <= 0 --> qnmf' = [ [i:[1..N]] smin+faultc[i] >= N ] ; qfp1' = [ [i:[1..N]] smin+faultc[i] >= f+1 ] ; timeAdvance' = IF FORALL (i:[1..N]): (qnmf[i] = qnmf'[i] AND qfp1[i] = qfp1'[i]) THEN min(z10, z11, 0, tMax) ELSE 0 ENDIF [] timeAdvance > 0 --> faultc' IN {a: ARRAY Node OF [0..1] | TRUE }; qnmf' = [ [i:[1..N]] smin+faultc'[i] >= N ] ; qfp1' = [ [i:[1..N]] smin+faultc'[i] >= f+1 ] ; timeAdvance' = IF FORALL (i:[1..N]): (qnmf[i] = qnmf'[i] AND qfp1[i] = qfp1'[i]) THEN min(z10, z11, 0, tMax) ELSE 0 ENDIF ] END; element[i: Node]: MODULE = BEGIN OUTPUT z10i, z11i: Time % -1 if stable (0); else unstate and z10 is the time when returns to 0 LOCAL z12b: BOOLEAN % latched values OUTPUT c0: BOOLEAN % clock output (latched inside FF z12a) INPUT qni, qfi: BOOLEAN INPUT timeAdvance: Time INITIALIZATION z10i = tMax - i; z11i = -1; z12b = TRUE % since qnmf is initialized to FALSE; this is NOT(it) % c0 is left uninitialized TRANSITION [ % Both z10 and z11 are triggered (NOT(qni) AND qni' AND NOT(qfi) AND qfi') OR (qfi AND NOT(qfi') AND qni AND NOT(qni')) --> z10i' = tMax-1 ; z11i' = IF z11i = -1 THEN tMin ELSE z11i ENDIF ; c0' = IF z11i = -1 THEN z12b ELSE c0 ENDIF [] % Only z10 is triggered, z11 is not ((NOT(qni) AND qni') OR (qfi AND NOT(qfi'))) AND NOT( (qni AND NOT(qni')) OR (NOT(qfi) AND qfi')) --> z10i' = tMax-1 [] % Only z11 is triggered, z10 is not NOT((NOT(qni) AND qni') OR (qfi AND NOT(qfi'))) AND ( (qni AND NOT(qni')) OR (NOT(qfi) AND qfi')) --> z11i' = IF z11i = -1 THEN tMin ELSE z11i ENDIF; c0' = IF z11i = -1 THEN z12b ELSE c0 ENDIF [] qni = qni' AND qfi = qfi' AND timeAdvance' > 0 AND z10i = timeAdvance' AND NOT(z11i = timeAdvance') --> z10i' = tMax-1; z11i' = IF z11i = -1 THEN tMin ELSE z11i - timeAdvance' ENDIF; c0' = IF z11i = -1 THEN z12b ELSE c0 ENDIF [] % Critical case - probability zero event? qni = qni' AND qfi = qfi' AND timeAdvance' > 0 AND z10i = timeAdvance' AND z11i = timeAdvance' --> z10i' = tMax-1 ; % z11i' = tMin ; z11i' = -1 ; z12b' = NOT(qni) ; % c0' = z12b [] % FIRE z11i qni = qni' AND qfi = qfi' AND timeAdvance' > 0 AND z11i = timeAdvance' AND NOT(z10i = timeAdvance') --> z10i' = IF z10i = -1 THEN -1 ELSE z10i - timeAdvance' ENDIF; z11i' = -1 ; % fire z12a z12b' = NOT(qni) ; [] qni = qni' AND qfi = qfi' AND timeAdvance' > 0 AND NOT(z11i = timeAdvance') AND NOT(z10i = timeAdvance') --> z10i' = IF z10i > 0 THEN z10i - timeAdvance' ELSE -1 ENDIF; z11i' = IF z11i > 0 THEN z11i - timeAdvance' ELSE -1 ENDIF; [] qni = qni' AND qfi = qfi' AND timeAdvance' = 0 --> %[] %timeAdvance' = 0 --> ] END; system: MODULE = calculator || ( WITH OUTPUT c: ARRAY Node OF BOOLEAN WITH INPUT qnmf: ARRAY Node OF BOOLEAN WITH INPUT qfp1: ARRAY Node OF BOOLEAN WITH OUTPUT z10: ARRAY Node OF Time WITH OUTPUT z11: ARRAY Node OF Time (|| (i: Node): RENAME c0 TO c[i], qni TO qnmf[i], qfi TO qfp1[i], z10i TO z10[i], z11i TO z11[i] IN element[i] ) ) ; monitor: MODULE = BEGIN INPUT c: ARRAY Node OF BOOLEAN INPUT timeAdvance: Time OUTPUT flag: BOOLEAN INITIALIZATION flag = FALSE TRANSITION [ timeAdvance' > 0 AND FORALL (i:Node): (c[i] = c[1]) --> flag' = TRUE [] timeAdvance' > 0 AND EXISTS (i:Node): NOT(c[i] = c[1]) --> flag' = FALSE [] ELSE --> ] END; systemmonitor: MODULE = system || monitor ; p0: LEMMA system |- G ( timeAdvance < 100 OR (FORALL (i:[1..N]): c[i] = c[1])) ; % PROVED! p1: LEMMA system |- F( G ( (FORALL (i:[1..N]): c[i] = c[1])) ) ; % PROVED ! p2: LEMMA system |- F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ; % INVALID p3: LEMMA system |- G ( timeAdvance = 0 ) ; % INVALID p4: LEMMA system |- G( EXISTS (i:[1..N]): z11[i] < tMin ) ; % PROVED ! p5: LEMMA system |- G( EXISTS (i:[1..N]): z10[i] > tMin ) ; % PROVED! p6: LEMMA system |- G( EXISTS (i:[1..N]): NOT(z10[i] = -1) OR NOT(z11[i] = -1)) ; % PROVED p7: LEMMA %system |- G(F( timeAdvance > 0)) => F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ; % PROVED ! system |- F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ; p8: LEMMA % PROVED %systemmonitor |- G(F( timeAdvance > 0)) => F ( flag ) ; % INVALID %systemmonitor |- G(F( timeAdvance > 0)) => G(F ( flag )) ; % PROVED %systemmonitor |- G( timeAdvance > 0 OR X(timeAdvance > 0)) => G(F ( flag )) ; % PROVED! % systemmonitor |- G(F ( flag )) ; % PROVED! systemmonitor |- F(G ( flag )) ; p9: LEMMA % PROVED!!! % system |- G(timeAdvance > 0 OR X(timeAdvance > 0)) => G ( F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ); % PROVED! % system |- G ( F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ); % PROVED! system |- F ( G ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ); % INVALID % system |- G(timeAdvance > 0 OR X(timeAdvance > 0) OR X(X(timeAdvance > 0))) => G ( F ( ((FORALL (i:[1..N]): c[i] = c[1])) ) ); % PROVED! p10: LEMMA system |- G(F(timeAdvance > 0)) ; % INVALID % system |- F(G(timeAdvance > 0)) ; % PROVED! p11: LEMMA system |- G(F(EXISTS (i:[1..N]): (NOT(z10[i] = -1) OR NOT(z11[i] = -1)))); p12: LEMMA system |- G ( (FORALL (i:[1..N]): c[i] = c[1]) => G ( (FORALL (i:[1..N]): c[i] = c[1])) ) ; END