% Short report on results on SAL model and formal verification of:
%
% A fault-tolerant digital clocking system
% William M. Daly
% Albert L. Hopkins, jr.,
% John F. McKena
% MIT Draper Lab
%
%% Summary of the result:
% ----------------------
% The proposed clock synchronization algorithm
% is buggy and can not synchronize clocks from
% arbitrary initial configurations if faults are
% assumed byzantine.
%
% Details:
% --------
% We modeled the proposed algorithm in SAL, as a
% finite state machine.
%
% Time was abstracted into 4 regions, named
% l, lf, fa, fl.
% Intuitively,
% "l" represents a small region around the leading edge,
% "fa" represents a small region around the falling edge,
% "lf" represents the region after l but before fa, and
% "fl" represents the region after fa but before l.
%
% The system has two parameters:
% f is the number of faulty clocks
% r is the number of non-faulty clocks.
% We verify the system for different values of f and r.
% We assume r+f >= 3*f+1
%
% The state of the system consists of
% c: ARRAY [1..r] OF BOOLEAN
% ftime, ltime: ARRAY [1..r] OF TIME
% qrmf,qfp1: ARRAY [1..r] OF BOOLEAN % qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
% currtime: TIME
%
% c is the array that stores the clock value for each of
% the r 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.
%
% currtime holds the value of the current time (l, lf, fa, fl).
%
% 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(r+f, f+1).
% qrmf is the quorum function Q(r+f, r).
%
% If clock c[i] sees a falling edge on qfp1 signal, then it
% sets ftime[i] to (current_time + 2 abstract time units).
% If clock c[i] sees a leading edge on qrmf signal, then it
% sets ltime[i] to (current_time + 2 abstract time units).
% There is also an abstract time value called "notset" for the
% case when these arrays have unset values.
%
% The SAL model then follows the description in the 1973 paper.
% When a clock output changes, it is not allowed to change again
% for an interval t_min, which in our case is 1 abstract time unit.
%
% We can run the sal symbolic model checker to verify
% eventuality properties, which state that the system eventually
% reaches some 'clock synchronized' state.
% We use f = 1 and r = 3.
%
% For the case when the initial state has 2 clocks at 1
% and 1 clock at 0, then the byzantine faulty 4th clock can
% make the system loop in states that have either
% (2 clocks at 1 and 1 clock at 0)
% or
% (1 clock at 1 and 2 clocks at 0)
% at all times.
% Thus, the good clocks never synchronize.
%
% Most minor changes to the protocol continue to yield counter-examples
% to the desired clock-sync property.
% It appears to be difficult to fix.
%
phaseLocking7: CONTEXT =
BEGIN
% Time is abstracted into 4 regions
% l = leading edge ; f = following edge (of desired clock signal)
TIME: TYPE = { l, lf, fa, fl, notset };
r: NATURAL = 3 ; % number of NON-FAULTY nodes
f: NATURAL = 1 ; % number of faults tolerated
sum(x: ARRAY [1..r] OF BOOLEAN, n: [0..r], a: [0..r] ): [0..r] =
IF n = r THEN a ELSIF x[n+1] THEN sum(x, n+1, a+1) ELSE sum(x, n+1, a) ENDIF;
% Q_b^r where s is the sum of all 1's in x
q(b: [1..r], s: [0..r]): [BOOLEAN -> BOOLEAN] =
IF (s >= b) THEN { TRUE }
ELSIF (s + f < b) THEN { FALSE }
ELSE { TRUE, FALSE } ENDIF ; % STUCK AT 1 FAULT - not byzantine
prev(t: TIME): TIME =
IF t = l THEN fl
ELSIF t = lf THEN l
ELSIF t = fa THEN lf
ELSE fa ENDIF ;
next(t: TIME): TIME =
IF t = l THEN lf
ELSIF t = lf THEN fa
ELSIF t = fa THEN fl
ELSE l ENDIF ;
next2(t: TIME): TIME = next(next(t)) ;
calculator: MODULE =
BEGIN
OUTPUT ftime, ltime: ARRAY [1..r] OF TIME
OUTPUT qrmf,qfp1: ARRAY [1..r] OF BOOLEAN % qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
INPUT c: ARRAY [1..r] OF BOOLEAN
INPUT currtime: TIME
LOCAL smin: [0..r]
INITIALIZATION
ftime = [ [i:[1..r]] IF c[i] THEN notset ELSE next(currtime) ENDIF ] ;
ltime = [ [i:[1..r]] IF c[i] THEN next(currtime) ELSE notset ENDIF ] ;
qrmf = [ [i:[1..r]] FALSE ];
qfp1 = [ [i:[1..r]] FALSE ];
DEFINITION
smin = sum(c, 0, 0) ;
TRANSITION
[
% currtime = currtime' -->
TRUE -->
qrmf' IN { a: ARRAY [1..r] OF BOOLEAN | FORALL (i:[1..r]):
q(r,smin)(a[i]) } ;
qfp1' IN { a: ARRAY [1..r] OF BOOLEAN | FORALL (i:[1..r]):
q(f+1,smin)(a[i]) } ;
ftime' = [ [i:[1..r]]
IF c[i] THEN notset
ELSIF (qfp1[i] AND qfp1'[i] = FALSE) THEN next2(currtime)
ELSE ftime[i] ENDIF ] ;
ltime' = [ [i:[1..r]]
IF NOT(c[i]) THEN notset
ELSIF (qrmf[i] = FALSE AND qrmf'[i]) THEN next2(currtime)
ELSE ltime[i] ENDIF ]
% []
% ELSE -->
]
END;
updater: MODULE =
BEGIN
INPUT ftime, ltime: ARRAY [1..r] OF TIME
INPUT qrmf,qfp1: ARRAY [1..r] OF BOOLEAN % qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
OUTPUT currtime: TIME
LOCAL frozen: ARRAY [1..r] OF TIME
LOCAL lastChange: ARRAY [1..r] OF TIME
OUTPUT c: ARRAY [1..r] OF BOOLEAN % r phase locked clock's
INITIALIZATION
currtime = l ;
frozen = [ [i:[1..r]] currtime ] ;
lastChange = [ [i:[1..r]] notset ] ;
%c = [ [i:[1..r]] FALSE ];
%c = [ [i:[1..r]] IF i=1 THEN TRUE ELSE FALSE ENDIF ];
c IN { a: ARRAY [1..r] OF BOOLEAN | 2*sum(a,0,0) = 2 } ;
TRANSITION
[
FORALL (i:[1..r]): (NOT(frozen[i] = currtime) OR
( NOT(qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i]) ) AND
NOT(qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]) AND
NOT(ftime[i] = currtime AND NOT(c[i])) AND
NOT(ltime[i] = currtime AND c[i]) )) AND NOT(lastChange[i] = next(currtime)) -->
currtime' = next(currtime) ;
frozen' = [ [i:[1..r]] IF frozen[i] = currtime THEN next(currtime)
ELSE frozen[i] ENDIF ]
[]
ELSE -->
c' = [ [i:[1..r]]
IF frozen[i] = currtime AND qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i])
THEN TRUE
ELSIF frozen[i] = currtime AND qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]
THEN FALSE
ELSIF frozen[i] = currtime AND ftime[i] = currtime AND NOT(c[i])
THEN TRUE
ELSIF frozen[i] = currtime AND ltime[i] = currtime AND c[i]
THEN FALSE
ELSIF lastChange[i] = next(currtime) THEN NOT(c[i])
ELSE c[i] ENDIF ] ;
lastChange' = [ [i:[1..r]]
IF NOT(c[i] = c'[i]) THEN currtime ELSE lastChange[i] ENDIF ] ;
frozen' = [ [i:[1..r]]
IF frozen[i] = currtime AND qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i])
THEN next(currtime)
ELSIF frozen[i] = currtime AND qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]
THEN next(currtime)
ELSIF frozen[i] = currtime AND ftime[i] = currtime AND NOT(c[i])
THEN next(currtime)
ELSIF frozen[i] = currtime AND ltime[i] = currtime AND c[i]
THEN next(currtime)
ELSE frozen[i] ENDIF ]
]
END ;
startup: MODULE = calculator || updater ;
p1: LEMMA
startup |- F ( currtime = fl );
p2: LEMMA
% startup |- F( G ( currtime = fl => (FORALL (i:[1..r]): c[i] = c[1])) ) ;
startup |- F( G ( (FORALL (i:[1..r]): c[i] = c[1])) ) ;
% THIS PROPERTY IS INVALID.
p22: LEMMA
startup |- F ( ((FORALL (i:[1..r]): c[i] = c[1])) ) ;
p3: LEMMA
startup |- ( G ( (currtime = fl) => (sum(c,0,0) <= f OR sum(c,0,0) >= 2*f+1) ) ) ;
p4: LEMMA
startup |- G ( (currtime = fl) => (FORALL (j:[1..r]): FORALL (k:[1..r]):
c[j] = c[k] ) );
p5: LEMMA
startup |- G( FORALL (i:[1..r]): c[i] = FALSE => X(NOT(ftime[i] = prev(currtime)) )) ;
END