|
virtual_clocks
[
P: posnat, % Nominal duration of a synchronization interval
T0: int, % Clocktime at start of protocol
rho: nnreal % Bound on drift for a good oscillator
] : THEORY
BEGIN
IMPORTING
interval_clocks[P, T0, rho],
inverse_clocks[rho],
event_sequences
ic, ic1, ic2: VAR interval_clock
es, es1, es2: VAR event_sequence
k, A: VAR nat
t1: VAR real
p: VAR posreal
adj, pi: VAR nnreal
au, al: VAR nnreal
%
VC(es)(ic)(t1): int = C(ic(index_of(es)(t1)))(t1)
VC_j: LEMMA VC(es)(ic)(es(k)) = C(ic(k))(es(k))
% an event sequence, es, of adjustments to an interval clock, ic
% has to satisfy these conditions:
earliest_adjustment?(ic, A)(es): bool =
FORALL k: ic(k)(T(k) - A) <= es(k)
latest_adjustment?(ic, A)(es): bool =
FORALL k: es(k + 1) <= ic(k)(T(k + 1) + A)
earliest_cross_adjustment?(ic, A)(es): bool =
FORALL k: ic(k)(T(k + 1) - A) <= es(k + 1)
latest_cross_adjustment?(ic, A)(es): bool =
FORALL k: es(k) <= ic(k)(T(k) + A)
self_adjustment?(ic, A)(es): bool =
earliest_adjustment?(ic, A)(es) AND
latest_adjustment?(ic, A)(es)
cross_adjustment?(ic, A)(es): bool =
earliest_cross_adjustment?(ic, A)(es) AND
latest_cross_adjustment?(ic, A)(es)
% observability properties for virtual clock update windows
observable_peers: LEMMA
self_adjustment?(ic, A)(es) AND
es(0) <= t1
IMPLIES
obs?(P + A, T(index_of(es)(t1)), ic(index_of(es)(t1)), t1)
observable_master: LEMMA
self_adjustment?(ic1, A)(es1) AND
cross_adjustment?(ic1, A)(es2) AND
max(es1(0),es2(0)) <= t1 AND
index_of(es2)(t1) = index_of(es1)(t1) + 1
IMPLIES
obs?(A, T(index_of(es1)(t1) + 1), ic1(index_of(es1)(t1)), t1)
observable_slave: LEMMA
self_adjustment?(ic2, A)(es2) AND
cross_adjustment?(ic2, A)(es1) AND
max(es1(0), es2(0)) <= t1 AND
index_of(es2)(t1) = index_of(es1)(t1) + 1
IMPLIES
obs?(A, T(index_of(es1)(t1) + 1), ic2(index_of(es1)(t1) + 1), t1)
% nonoverlap properties for virtual clocks
adjustment_nonoverlap: LEMMA %%% NOT USED, but curious
latest_cross_adjustment?(ic, A)(es1) AND
earliest_cross_adjustment?(ic, A)(es2) AND
2 * A <= P
IMPLIES
nonoverlap?(es1, es2)
% precision results for virtual clocks
Pi(adj, A): int = ceiling(rate * (adj + drift * (P + A)))
VC_precision_0: LEMMA
peer_precision?(ic1, ic2, adj) AND
peer_precision?(ic2, ic1, adj) AND
self_adjustment?(ic1, A)(es1) AND
self_adjustment?(ic2, A)(es2) AND
max(es1(0), es2(0)) <= t1 AND
index_of(es2)(t1) = index_of(es1)(t1)
IMPLIES
abs(VC(es1)(ic1)(t1) - VC(es2)(ic2)(t1)) <= Pi(adj, A)
VC_precision_1: LEMMA
compatible?(ic1, ic2, adj) AND
self_adjustment?(ic1, A)(es1) AND
self_adjustment?(ic2, A)(es2) AND
cross_adjustment?(ic1, A)(es2) AND
cross_adjustment?(ic2, A)(es1) AND
max(es1(0), es2(0)) <= t1 AND
index_of(es2)(t1) = index_of(es1)(t1) + 1
IMPLIES
abs(VC(es1)(ic1)(t1) - VC(es2)(ic2)(t1)) <= Pi(adj, A)
VC_precision_sym: LEMMA
compatible?(ic1, ic2, adj) AND
compatible?(ic2, ic1, adj) AND
nonoverlap?(es1, es2) AND
self_adjustment?(ic1, A)(es1) AND
self_adjustment?(ic2, A)(es2) AND
cross_adjustment?(ic1, A)(es2) AND
cross_adjustment?(ic2, A)(es1) AND
max(es1(0), es2(0)) <= t1 AND
index_of(es2)(t1) >= index_of(es1)(t1)
IMPLIES
abs(VC(es1)(ic1)(t1) - VC(es2)(ic2)(t1)) <= Pi(adj, A)
VC_precision: THEOREM
compatible?(ic1, ic2, adj) AND
compatible?(ic2, ic1, adj) AND
nonoverlap?(es1, es2) AND
nonoverlap?(es2, es1) AND
self_adjustment?(ic1, A)(es1) AND
self_adjustment?(ic2, A)(es2) AND
cross_adjustment?(ic1, A)(es2) AND
cross_adjustment?(ic2, A)(es1) AND
max(es1(0), es2(0)) <= t1
IMPLIES
abs(VC(es1)(ic1)(t1) - VC(es2)(ic2)(t1)) <= Pi(adj, A)
% accuracy results for virtual clocks
index_upper_bound: LEMMA
lower_accuracy_bound?(ic, al, pi) AND
earliest_adjustment?(ic, A)(es) AND
p = P / rate - al AND
es(0) <= t1
IMPLIES
index_of(es)(t1) <= (t1 - t(ic)(0) + A * rate + pi) / p
VC_lower_accuracy: THEOREM
upper_accuracy_bound?(ic, au, pi) AND
lower_accuracy_bound?(ic, al, pi) AND
earliest_adjustment?(ic, A)(es) AND
p = P / rate - al AND
es(0) <= t1
IMPLIES
((t1 - t(ic)(0)) * (1 - au / p)
- pi * (1 + au / p)
- A * (drift + rate * au / p)) / rate
< 1 + VC(es)(ic)(t1) - T(0)
VC_upper_accuracy: THEOREM
lower_accuracy_bound?(ic, al, pi) AND
earliest_adjustment?(ic, A)(es) AND
p = P / rate - al AND
es(0) <= t1
IMPLIES
VC(es)(ic)(t1) - T(0) <=
((t1 - t(ic)(0)) * (1 + al / p)
+ pi * (1 + al / p)
+ A * (drift + rate * al / p)) * rate
END virtual_clocks
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
