|
%
% Purpose : There are two common scenarios for synchronization
% protocols to apply instantaneous adjustments. The
% first is to compute a correction term for the current
% interval,and apply the correction when the Clocktime
% reaches a specific value. The second is to set the
% local counter to a specific value in response to some event.
% This file presents a virtual clock based upon the first
% scenario and shows that is satisfies the Precision
% requirement of clock synchronization
%
virtual_clock_1
[(IMPORTING synch_protocol_invariants)
P: posnat, % Nominal duration of a synchronization interval
T0: int, % Clocktime at start of protocol
rho: nnreal, % Bound on drift for a good oscillator
alpha_l, alpha_u: nnreal, % negative and positive read error bounds
pi_0: {pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}
] : THEORY
BEGIN
IMPORTING
synch_protocol_invariants[P, T0, rho, alpha_l, alpha_u, pi_0],
virtual_clocks[P, T0, rho]
hst: VAR [nat -> non_empty_finite_set[good_clock]]
ic, ic1, ic2: VAR interval_clock
t1: VAR real
ac, ac1, ac2: VAR weakly_accurate_clock
k : VAR nat
j: VAR posint
% Definition and required properties of turns(ac) event_sequence
turns(ac)(k): real = IF k = 0 THEN ac(0)(T(0)) ELSE ac(k-1)(T(k)) ENDIF
turns_increasing: LEMMA increasing?(turns(ac))
turns_unbounded: LEMMA unbounded?(turns(ac))
turns_event_sequence: JUDGEMENT turns(ac) HAS_TYPE event_sequence
turns_nonoverlap: LEMMA
compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u)) AND
compatible?(ac2, ac1, pi_0 + max(alpha_l, alpha_u))
IMPLIES
nonoverlap?(turns(ac1), turns(ac2))
turns_early: LEMMA earliest_adjustment?(ac, ADJ + 1)(turns(ac))
turns_self: LEMMA self_adjustment?(ac, ADJ + 1)(turns(ac))
turns_cross: LEMMA
compatible?(ac1, ac2, pi_0 + max(alpha_l, alpha_u)) AND
compatible?(ac2, ac1, pi_0 + max(alpha_l, alpha_u))
IMPLIES
cross_adjustment?(ac1, ADJ + 1)(turns(ac2))
% main results
VC1(ac)(t1): int = VC(turns(ac))(ac)(t1)
VC1_j: LEMMA VC1(ac)(turns(ac)(j)) = C(ac(j))(ac(j - 1)(T(j)))
VC1_precision: THEOREM
trace?(ic1, hst) AND
trace?(ic2, hst) AND
initial_precision?(hst, pi_0) AND
synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
max(t(ic1)(0),t(ic2)(0)) <= t1
IMPLIES
abs(VC1(ic1)(t1) - VC1(ic2)(t1)) <= Pi
VC1_accuracy_lower: THEOREM
trace?(ic, hst) AND
initial_precision?(hst, pi_0) AND
synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
t(ic)(0) <= t1
IMPLIES
((t1 - t(ic)(0)) * (1 - (alpha_u / p_lower))
- pi_0 * (1 + alpha_u / p_lower)
- (drift + rate * (alpha_u / p_lower)) * (1 + ADJ)) / rate
< 1 + VC1(ic)(t1) - T(0)
VC1_optimal_accuracy_lower: COROLLARY
alpha_u = 0 AND
trace?(ic, hst) AND
initial_precision?(hst, pi_0) AND
synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
t(ic)(0) <= t1
IMPLIES
((t1 - t(ic)(0)) - pi_0) / rate
- drift * (1 + ADJ) / rate
< 1 + VC1(ic)(t1) - T(0)
VC1_accuracy_upper: THEOREM
trace?(ic, hst) AND
initial_precision?(hst, pi_0) AND
synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
t(ic)(0) <= t1
IMPLIES
VC1(ic)(t1) - T(0)
<= ((t1 - t(ic)(0)) * (1 + alpha_l / p_lower)
+ pi_0 * (1 + alpha_l / p_lower)) * rate
+ (1 + ADJ) * (drift + rate * alpha_l / p_lower) * rate
VC1_optimal_accuracy_upper: COROLLARY
alpha_l = 0 AND
trace?(ic, hst) AND
initial_precision?(hst, pi_0) AND
synch_protocol_invariants?(hst, pi_0, p_lower, p_upper) AND
t(ic)(0) <= t1
IMPLIES
VC1(ic)(t1) - T(0)
<= ((t1 - t(ic)(0)) + pi_0) * rate
+ (1 + ADJ) * drift * rate
END virtual_clock_1
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
