Theory AteDefs
theory AteDefs
imports "../HOModel"
begin
section ‹Verification of the \ate{} Consensus algorithm›
text ‹
Algorithm \ate{} is presented in~\<^cite>‹"biely:tolerating"›. Like \ute{},
it is an uncoordinated algorithm that tolerates value faults, and it
is parameterized by values $T$, $E$, and $\alpha$ that serve a similar
function as in \ute{}, allowing the algorithm to be adapted to the
characteristics of different systems. \ate{} can be understood as a
variant of \emph{OneThirdRule} tolerating Byzantine faults.
We formalize in Isabelle the correctness proof of the algorithm that
appears in~\<^cite>‹"biely:tolerating"›, using the framework of theory
‹HOModel›.
›
subsection ‹Model of the Algorithm›
text ‹
We begin by introducing an anonymous type of processes of finite
cardinality that will instantiate the type variable ‹'proc›
of the generic HO model.
›
typedecl Proc
axiomatization where Proc_finite: "OFCLASS(Proc, finite_class)"
instance Proc :: finite by (rule Proc_finite)
abbreviation
"N ≡ card (UNIV::Proc set)"
text ‹The following record models the local state of a process.›
record 'val pstate =
x :: "'val"
decide :: "'val option"
text ‹
The ‹x› field of the initial state is unconstrained, but no
decision has yet been taken.
›
definition Ate_initState where
"Ate_initState p st ≡ (decide st = None)"
text ‹
The following locale introduces the parameters used for the \ate{}
algorithm and their constraints~\<^cite>‹"biely:tolerating"›.
›
locale ate_parameters =
fixes α::nat and T::nat and E::nat
assumes TNaE:"T ≥ 2*(N + 2*α - E)"
and TltN:"T < N"
and EltN:"E < N"
begin
text ‹The following are consequences of the assumptions on the parameters.›
lemma majE: "2 * (E - α) ≥ N"
using TNaE TltN by auto
lemma Egta: "E > α"
using majE EltN by auto
lemma Tge2a: "T ≥ 2 * α"
using TNaE EltN by auto
text ‹
At every round, each process sends its current ‹x›.
If it received more than ‹T› messages, it selects the smallest value
and store it in ‹x›. As in algorithm \emph{OneThirdRule}, we
therefore require values to be linearly ordered.
If more than ‹E› messages holding the same value are received,
the process decides that value.
›
definition mostOftenRcvd where
"mostOftenRcvd (msgs::Proc ⇒ 'val option) ≡
{v. ∀w. card {qq. msgs qq = Some w} ≤ card {qq. msgs qq = Some v}}"
definition
Ate_sendMsg :: "nat ⇒ Proc ⇒ Proc ⇒ 'val pstate ⇒ 'val"
where
"Ate_sendMsg r p q st ≡ x st"
definition
Ate_nextState :: "nat ⇒ Proc ⇒ ('val::linorder) pstate ⇒ (Proc ⇒ 'val option)
⇒ 'val pstate ⇒ bool"
where
"Ate_nextState r p st msgs st' ≡
(if card {q. msgs q ≠ None} > T
then x st' = Min (mostOftenRcvd msgs)
else x st' = x st)
∧ ( (∃v. card {q. msgs q = Some v} > E ∧ decide st' = Some v)
∨ ¬ (∃v. card {q. msgs q = Some v} > E)
∧ decide st' = decide st)"
subsection ‹Communication Predicate for \ate{}›
text ‹
Following~\<^cite>‹"biely:tolerating"›, we now define the communication
predicate for the \ate{} algorithm. The round-by-round predicate
requires that no process may receive more than ‹α› corrupted
messages at any round.
›
definition Ate_commPerRd where
"Ate_commPerRd HOrs SHOrs ≡
∀p. card (HOrs p - SHOrs p) ≤ α"
text ‹
The global communication predicate stipulates the three following
conditions:
\begin{itemize}
\item for every process ‹p› there are infinitely many rounds
where ‹p› receives more than ‹T› messages,
\item for every process ‹p› there are infinitely many rounds
where ‹p› receives more than ‹E› uncorrupted messages,
\item and there are infinitely many rounds in which more than
‹E - α› processes receive uncorrupted messages from the
same set of processes, which contains more than ‹T› processes.
\end{itemize}
›
definition
Ate_commGlobal where
"Ate_commGlobal HOs SHOs ≡
(∀r p. ∃r' > r. card (HOs r' p) > T)
∧ (∀r p. ∃r' > r. card (SHOs r' p ∩ HOs r' p) > E)
∧ (∀r. ∃r' > r. ∃π1 π2.
card π1 > E - α
∧ card π2 > T
∧ (∀p ∈ π1. HOs r' p = π2 ∧ SHOs r' p ∩ HOs r' p = π2))"
subsection ‹The \ate{} Heard-Of Machine›
text ‹
We now define the non-coordinated SHO machine for the \ate{} algorithm
by assembling the algorithm definition and its communication-predicate.
›
definition Ate_SHOMachine where
"Ate_SHOMachine = ⦇
CinitState = (λ p st crd. Ate_initState p (st::('val::linorder) pstate)),
sendMsg = Ate_sendMsg,
CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st'),
SHOcommPerRd = (Ate_commPerRd:: Proc HO ⇒ Proc HO ⇒ bool),
SHOcommGlobal = Ate_commGlobal
⦈"
abbreviation
"Ate_M ≡ (Ate_SHOMachine::(Proc, 'val::linorder pstate, 'val) SHOMachine)"
end
end