Theory Heard_Of.HOModel
theory HOModel
imports Main
begin
declare if_split_asm [split]
section ‹Heard-Of Algorithms›
subsection ‹The Consensus Problem›
text ‹
We are interested in the verification of fault-tolerant distributed algorithms.
The Consensus problem is paradigmatic in this area. Stated
informally, it assumes that all processes participating in the algorithm
initially propose some value, and that they may at some point decide some value.
It is required that every process eventually decides, and that all processes
must decide the same value.
More formally, we represent runs of algorithms as ‹ω›-sequences of
configurations (vectors of process states). Hence, a run is modeled as
a function of type ‹nat ⇒ 'proc ⇒ 'pst› where type variables
‹'proc› and ‹'pst› represent types of processes and process
states, respectively. The Consensus property is expressed with respect
to a collection ‹vals› of initially proposed values (one per process)
and an observer function ‹dec::'pst ⇒ val option› that retrieves the decision
(if any) from a process state. The Consensus problem is stated as the conjunction
of the following properties:
\begin{description}
\item[Integrity.] Processes can only decide initially proposed values.
\item[Agreement.] Whenever processes ‹p› and ‹q› decide,
their decision values must be the same. (In particular, process ‹p›
may never change the value it decides, which is referred to as Irrevocability.)
\item[Termination.] Every process decides eventually.
\end{description}
The above properties are sometimes only required of non-faulty processes, since
nothing can be required of a faulty process.
The Heard-Of model does not attribute faults to processes, and therefore the
above formulation is appropriate in this framework.
›
type_synonym
('proc,'pst) run = "nat ⇒ 'proc ⇒ 'pst"
definition
consensus :: "('proc ⇒ 'val) ⇒ ('pst ⇒ 'val option) ⇒ ('proc,'pst) run ⇒ bool"
where
"consensus vals dec rho ≡
(∀n p v. dec (rho n p) = Some v ⟶ v ∈ range vals)
∧ (∀m n p q v w. dec (rho m p) = Some v ∧ dec (rho n q) = Some w
⟶ v = w)
∧ (∀p. ∃n. dec (rho n p) ≠ None)"
text ‹
A variant of the Consensus problem replaces the Integrity requirement by
\begin{description}
\item[Validity.] If all processes initially propose the same value ‹v›
then every process may only decide ‹v›.
\end{description}
›
definition weak_consensus where
"weak_consensus vals dec rho ≡
(∀v. (∀p. vals p = v) ⟶ (∀n p w. dec (rho n p) = Some w ⟶ w = v))
∧ (∀m n p q v w. dec (rho m p) = Some v ∧ dec (rho n q) = Some w
⟶ v = w)
∧ (∀p. ∃n. dec (rho n p) ≠ None)"
text ‹
Clearly, ‹consensus› implies ‹weak_consensus›.
›
lemma consensus_then_weak_consensus:
assumes "consensus vals dec rho"
shows "weak_consensus vals dec rho"
using assms by (auto simp: consensus_def weak_consensus_def image_def)
text ‹
Over Boolean values (``binary Consensus''), ‹weak_consensus›
implies ‹consensus›, hence the two problems are equivalent.
In fact, this theorem holds more generally whenever at most two
different values are proposed initially (i.e., ‹card (range vals) ≤ 2›).
›
lemma binary_weak_consensus_then_consensus:
assumes bc: "weak_consensus (vals::'proc ⇒ bool) dec rho"
shows "consensus vals dec rho"
proof -
{
fix n p v
assume dec: "dec (rho n p) = Some v"
have "v ∈ range vals"
proof (cases "∃w. ∀p. vals p = w")
case True
then obtain w where w: "∀p. vals p = w" ..
with bc have "dec (rho n p) ∈ {Some w, None}" by (auto simp: weak_consensus_def)
with dec w show ?thesis by (auto simp: image_def)
next
case False
thus ?thesis by (auto simp: image_def)
qed
} note integrity = this
from bc show ?thesis
unfolding consensus_def weak_consensus_def by (auto elim!: integrity)
qed
text ‹
The algorithms that we are going to verify solve the Consensus or weak Consensus
problem, under different hypotheses about the kinds and number of faults.
›
subsection ‹A Generic Representation of Heard-Of Algorithms›
text ‹
Charron-Bost and Schiper~\<^cite>‹"charron:heardof"› introduce
the Heard-Of (HO) model for representing fault-tolerant
distributed algorithms. In this model, algorithms execute in communication-closed
rounds: at any round~$r$, processes only receive messages that were sent for
that round. For every process~$p$ and round~$r$, the ``heard-of set'' $HO(p,r)$
denotes the set of processes from which~$p$ receives a message in round~$r$.
Since every process is assumed to send a message to all processes in each round,
the complement of $HO(p,r)$ represents the set of faults that may affect~$p$ in
round~$r$ (messages that were not received, e.g. because the sender crashed,
because of a network problem etc.).
The HO model expresses hypotheses on the faults tolerated by an algorithm
through ``communication predicates'' that constrain the sets $HO(p,r)$
that may occur during an execution. Charron-Bost and Schiper show that
standard fault models can be represented in this form.
The original HO model is sufficient for representing algorithms
tolerating benign failures such as process crashes or message loss. A later
extension for algorithms tolerating Byzantine (or value) failures~\<^cite>‹"biely:tolerating"›
adds a second collection of sets $SHO(p,r) \subseteq HO(p,r)$ that contain those
processes $q$ from which process $p$ receives the message that $q$ was indeed
supposed to send for round $r$ according to the algorithm. In other words,
messages from processes in $HO(p,r) \setminus SHO(p,r)$ were corrupted, be it
due to errors during message transmission or because of the sender was faulty or
lied deliberately. For both benign and Byzantine errors, the HO model registers
the fault but does not try to identify the faulty component (i.e., designate the
sending or receiving process, or the communication channel as the ``culprit'').
Executions of HO algorithms are defined with respect to collections
$HO(p,r)$ and $SHO(p,r)$. However, the code of a process does not have
access to these sets. In particular, process $p$ has no way of determining
if a message it received from another process $q$ corresponds to what $q$
should have sent or if it has been corrupted.
Certain algorithms rely on the assignment of ``coordinator'' processes for
each round. Just as the collections $HO(p,r)$, the definitions assume an
external coordinator assignment such that $coord(p,r)$ denotes the coordinator
of process $p$ and round $r$. Again, the correctness of algorithms may depend
on hypotheses about coordinator assignments -- e.g., it may be assumed that
processes agree sufficiently often on who the current coordinator is.
The following definitions provide a generic representation of HO and SHO algorithms
in Isabelle/HOL. A (coordinated) HO algorithm is described by the following parameters:
\begin{itemize}
\item a finite type ‹'proc› of processes,
\item a type ‹'pst› of local process states,
\item a type ‹'msg› of messages sent in the course of the algorithm,
\item a predicate ‹CinitState› such that ‹CinitState p st crd› is
true precisely of the initial states ‹st› of process ‹p›, assuming
that ‹crd› is the initial coordinator of ‹p›,
\item a function ‹sendMsg› where ‹sendMsg r p q st› yields
the message that process ‹p› sends to process ‹q› at round
‹r›, given its local state ‹st›, and
\item a predicate ‹CnextState› where ‹CnextState r p st msgs crd st'›
characterizes the successor states ‹st'› of process ‹p› at round
‹r›, given current state ‹st›, the vector
‹msgs :: 'proc ⇒ 'msg option› of messages that ‹p› received at
round ‹r› (‹msgs q = None› indicates that no message has been
received from process ‹q›),
and process ‹crd› as the coordinator for the following round.
\end{itemize}
Note that every process can store the coordinator for the current round in its
local state, and it is therefore not necessary to make the coordinator a parameter
of the message sending function ‹sendMsg›.
We represent an algorithm by a record as follows.
›
record ('proc, 'pst, 'msg) CHOAlgorithm =
CinitState :: "'proc ⇒ 'pst ⇒ 'proc ⇒ bool"
sendMsg :: "nat ⇒ 'proc ⇒ 'proc ⇒ 'pst ⇒ 'msg"
CnextState :: "nat ⇒ 'proc ⇒ 'pst ⇒ ('proc ⇒ 'msg option) ⇒ 'proc ⇒ 'pst ⇒ bool"
text ‹
For non-coordinated HO algorithms, the coordinator argument of functions
‹CinitState› and ‹CnextState› is irrelevant, and we
define utility functions that omit that argument.
›
definition isNCAlgorithm where
"isNCAlgorithm alg ≡
(∀p st crd crd'. CinitState alg p st crd = CinitState alg p st crd')
∧ (∀r p st msgs crd crd' st'. CnextState alg r p st msgs crd st'
= CnextState alg r p st msgs crd' st')"
definition initState where
"initState alg p st ≡ CinitState alg p st undefined"
definition nextState where
"nextState alg r p st msgs st' ≡ CnextState alg r p st msgs undefined st'"
text ‹
A \emph{heard-of assignment} associates a set of processes with each
process. The following type is used to represent the collections $HO(p,r)$
and $SHO(p,r)$ for fixed round $r$.
%
Similarly, a \emph{coordinator assignment} associates a process (its coordinator)
to each process.
›
type_synonym
'proc HO = "'proc ⇒ 'proc set"
type_synonym
'proc coord = "'proc ⇒ 'proc"
text ‹
An execution of an HO algorithm is defined with respect to HO and SHO
assignments that indicate, for every round ‹r› and every process ‹p›,
from which sender processes ‹p› receives messages (resp., uncorrupted
messages) at round ‹r›.
%% That's the intention, but we don't enforce this in the definitions.
% Obviously, SHO sets are always included in HO sets, for the same process and round.
The following definitions formalize this idea. We define ``coarse-grained''
executions whose unit of atomicity is the round of execution. At each round,
the entire collection of processes performs a transition according to the
‹CnextState› function of the algorithm. Consequently, a system state is
simply described by a configuration, i.e. a function assigning a process state
to every process. This definition of executions may appear surprising for an
asynchronous distributed system, but it simplifies system verification,
compared to a ``fine-grained'' execution model that records individual events
such as message sending and reception or local transitions. We will justify
later why the ``coarse-grained'' model is sufficient for verifying interesting
correctness properties of HO algorithms.
The predicate ‹CSHOinitConfig› describes the possible initial configurations
for algorithm ‹A› (remember that a configuration is a function that assigns
local states to every process).
›
definition CHOinitConfig where
"CHOinitConfig A cfg (coord::'proc coord) ≡ ∀p. CinitState A p (cfg p) (coord p)"
text ‹
Given the current configuration ‹cfg› and the HO and SHO sets ‹HOp›
and ‹SHOp› for process ‹p› at round ‹r›, the function
‹SHOmsgVectors› computes the set of possible vectors of messages that
process ‹p› may receive. For processes ‹q ∉ HOp›, ‹p›
receives no message (represented as value ‹None›). For processes
‹q ∈ SHOp›, ‹p› receives the message that ‹q› computed
according to the ‹sendMsg› function of the algorithm. For the remaining
processes ‹q ∈ HOp - SHOp›, ‹p› may receive some arbitrary value.
›
definition SHOmsgVectors where
"SHOmsgVectors A r p cfg HOp SHOp ≡
{μ. (∀q. q ∈ HOp ⟷ μ q ≠ None)
∧ (∀q. q ∈ SHOp ∩ HOp ⟶ μ q = Some (sendMsg A r q p (cfg q)))}"
text ‹
Predicate ‹CSHOnextConfig› uses the preceding function and the algorithm's
‹CnextState› function to characterize the possible successor configurations
in a coarse-grained step, and predicate ‹CSHORun› defines (coarse-grained)
executions ‹rho› of an HO algorithm.
›
definition CSHOnextConfig where
"CSHOnextConfig A r cfg HO SHO coord cfg' ≡
∀p. ∃μ ∈ SHOmsgVectors A r p cfg (HO p) (SHO p).
CnextState A r p (cfg p) μ (coord p) (cfg' p)"
definition CSHORun where
"CSHORun A rho HOs SHOs coords ≡
CHOinitConfig A (rho 0) (coords 0)
∧ (∀r. CSHOnextConfig A r (rho r) (HOs r) (SHOs r) (coords (Suc r))
(rho (Suc r)))"
text ‹
For non-coordinated algorithms. the ‹coord› arguments of the above functions
are irrelevant. We define similar functions that omit that argument, and relate
them to the above utility functions for these algorithms.
›
definition HOinitConfig where
"HOinitConfig A cfg ≡ CHOinitConfig A cfg (λq. undefined)"
lemma HOinitConfig_eq:
"HOinitConfig A cfg = (∀p. initState A p (cfg p))"
by (auto simp: HOinitConfig_def CHOinitConfig_def initState_def)
definition SHOnextConfig where
"SHOnextConfig A r cfg HO SHO cfg' ≡
CSHOnextConfig A r cfg HO SHO (λq. undefined) cfg'"
lemma SHOnextConfig_eq:
"SHOnextConfig A r cfg HO SHO cfg' =
(∀p. ∃μ ∈ SHOmsgVectors A r p cfg (HO p) (SHO p).
nextState A r p (cfg p) μ (cfg' p))"
by (auto simp: SHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_def nextState_def)
definition SHORun where
"SHORun A rho HOs SHOs ≡
CSHORun A rho HOs SHOs (λr q. undefined)"
lemma SHORun_eq:
"SHORun A rho HOs SHOs =
(HOinitConfig A (rho 0)
∧ (∀r. SHOnextConfig A r (rho r) (HOs r) (SHOs r) (rho (Suc r))))"
by (auto simp: SHORun_def CSHORun_def HOinitConfig_def SHOnextConfig_def)
text ‹
Algorithms designed to tolerate benign failures are not subject to
message corruption, and therefore the SHO sets are irrelevant (more formally,
each SHO set equals the corresponding HO set). We define corresponding
special cases of the definitions of successor configurations and of runs,
and prove that these are equivalent to simpler definitions that will be more
useful in proofs. In particular, the vector of messages received by a process
in a benign execution is uniquely determined from the current configuration
and the HO sets.
›
definition HOrcvdMsgs where
"HOrcvdMsgs A r p HO cfg ≡
λq. if q ∈ HO then Some (sendMsg A r q p (cfg q)) else None"
lemma SHOmsgVectors_HO:
"SHOmsgVectors A r p cfg HO HO = {HOrcvdMsgs A r p HO cfg}"
unfolding SHOmsgVectors_def HOrcvdMsgs_def by auto
text ‹With coordinators›
definition CHOnextConfig where
"CHOnextConfig A r cfg HO coord cfg' ≡
CSHOnextConfig A r cfg HO HO coord cfg'"
lemma CHOnextConfig_eq:
"CHOnextConfig A r cfg HO coord cfg' =
(∀p. CnextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg)
(coord p) (cfg' p))"
by (auto simp: CHOnextConfig_def CSHOnextConfig_def SHOmsgVectors_HO)
definition CHORun where
"CHORun A rho HOs coords ≡ CSHORun A rho HOs HOs coords"
lemma CHORun_eq:
"CHORun A rho HOs coords =
(CHOinitConfig A (rho 0) (coords 0)
∧ (∀r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))))"
by (auto simp: CHORun_def CSHORun_def CHOinitConfig_def CHOnextConfig_def)
text ‹Without coordinators›
definition HOnextConfig where
"HOnextConfig A r cfg HO cfg' ≡ SHOnextConfig A r cfg HO HO cfg'"
lemma HOnextConfig_eq:
"HOnextConfig A r cfg HO cfg' =
(∀p. nextState A r p (cfg p) (HOrcvdMsgs A r p (HO p) cfg) (cfg' p))"
by (auto simp: HOnextConfig_def SHOnextConfig_eq SHOmsgVectors_HO)
definition HORun where
"HORun A rho HOs ≡ SHORun A rho HOs HOs"
lemma HORun_eq:
"HORun A rho HOs =
( HOinitConfig A (rho 0)
∧ (∀r. HOnextConfig A r (rho r) (HOs r) (rho (Suc r))))"
by (auto simp: HORun_def SHORun_eq HOnextConfig_def)
text ‹
The following derived proof rules are immediate consequences of
the definition of ‹CHORun›; they simplify automatic reasoning.
›
lemma CHORun_0:
assumes "CHORun A rho HOs coords"
and "⋀cfg. CHOinitConfig A cfg (coords 0) ⟹ P cfg"
shows "P (rho 0)"
using assms unfolding CHORun_eq by blast
lemma CHORun_Suc:
assumes "CHORun A rho HOs coords"
and "⋀r. CHOnextConfig A r (rho r) (HOs r) (coords (Suc r)) (rho (Suc r))
⟹ P r"
shows "P n"
using assms unfolding CHORun_eq by blast
lemma CHORun_induct:
assumes run: "CHORun A rho HOs coords"
and init: "CHOinitConfig A (rho 0) (coords 0) ⟹ P 0"
and step: "⋀r. ⟦ P r; CHOnextConfig A r (rho r) (HOs r) (coords (Suc r))
(rho (Suc r)) ⟧ ⟹ P (Suc r)"
shows "P n"
using run unfolding CHORun_eq by (induct n, auto elim: init step)
text ‹
Because algorithms will not operate for arbitrary HO, SHO, and coordinator
assignments, these are constrained by a \emph{communication predicate}.
For convenience, we split this predicate into a \emph{per Round} part that
is expected to hold at every round and a \emph{global} part that must hold
of the sequence of (S)HO assignments and may thus express liveness assumptions.
In the parlance of~\<^cite>‹"charron:heardof"›, a \emph{HO machine} is an HO algorithm
augmented with a communication predicate. We therefore define (C)(S)HO machines as
the corresponding extensions of the record defining an HO algorithm.
›
record ('proc, 'pst, 'msg) HOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
HOcommPerRd::"'proc HO ⇒ bool"
HOcommGlobal::"(nat ⇒ 'proc HO) ⇒ bool"
record ('proc, 'pst, 'msg) CHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
CHOcommPerRd::"nat ⇒ 'proc HO ⇒ 'proc coord ⇒ bool"
CHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc coord) ⇒ bool"
record ('proc, 'pst, 'msg) SHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
SHOcommPerRd::"('proc HO) ⇒ ('proc HO) ⇒ bool"
SHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc HO) ⇒ bool"
record ('proc, 'pst, 'msg) CSHOMachine = "('proc, 'pst, 'msg) CHOAlgorithm" +
CSHOcommPerRd::"('proc HO) ⇒ ('proc HO) ⇒ 'proc coord ⇒ bool"
CSHOcommGlobal::"(nat ⇒ 'proc HO) ⇒ (nat ⇒ 'proc HO)
⇒ (nat ⇒ 'proc coord) ⇒ bool"
end