theory HOModel imports Main begin declare if_split_asm [split] ― ‹perform default perform case splitting on conditionals› 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 - { ― ‹Show the Integrity property, the other conjuncts are the same.› 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 ― ‹In this case both possible values occur in @{text "vals"}, and the result is trivial.› 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 ― ‹theory HOModel›