section ‹The OneThirdRule Algorithm› theory OneThirdRule_Defs imports Heard_Of.HOModel "../Consensus_Types" begin text ‹The contents of this file have been taken almost verbatim from the Heard Of Model AFP entry. The only difference is that the types have been changed.› subsection ‹Model of the algorithm› text ‹ The state of each process consists of two fields: ‹last_vote› holds the current value proposed by the process and ‹decision› the value (if any, hence the option type) it has decided. › record 'val pstate = last_vote :: "'val" decision :: "'val option" text ‹ The initial value of field ‹last_vote› is unconstrained, but no decision has been taken initially. › definition OTR_initState where "OTR_initState p st ≡ decision st = None" text ‹ Given a vector ‹msgs› of values (possibly null) received from each process, @{term "HOV msgs v"} denotes the set of processes from which value ‹v› was received. › definition HOV :: "(process ⇒ 'val option) ⇒ 'val ⇒ process set" where "HOV msgs v ≡ { q . msgs q = Some v }" text ‹ @{term "MFR msgs v"} (``most frequently received'') holds for vector ‹msgs› if no value has been received more frequently than ‹v›. Some such value always exists, since there is only a finite set of processes and thus a finite set of possible cardinalities of the sets @{term "HOV msgs v"}. › definition MFR :: "(process ⇒ 'val option) ⇒ 'val ⇒ bool" where "MFR msgs v ≡ ∀w. card (HOV msgs w) ≤ card (HOV msgs v)" lemma MFR_exists: "∃v. MFR msgs v" proof - let ?cards = "{ card (HOV msgs v) | v . True }" let ?mfr = "Max ?cards" have "∀v. card (HOV msgs v) ≤ N" by (auto intro: card_mono) hence "?cards ⊆ { 0 .. N }" by auto hence fin: "finite ?cards" by (metis atLeast0AtMost finite_atMost finite_subset) hence "?mfr ∈ ?cards" by (rule Max_in) auto then obtain v where v: "?mfr = card (HOV msgs v)" by auto have "MFR msgs v" proof (auto simp: MFR_def) fix w from fin have "card (HOV msgs w) ≤ ?mfr" by (rule Max_ge) auto thus "card (HOV msgs w) ≤ card (HOV msgs v)" by (unfold v) qed thus ?thesis .. qed text ‹ Also, if a process has heard from at least one other process, the most frequently received values are among the received messages. › lemma MFR_in_msgs: assumes HO:"HOs m p ≠ {}" and v: "MFR (HOrcvdMsgs OTR_M m p (HOs m p) (rho m)) v" (is "MFR ?msgs v") shows "∃q ∈ HOs m p. v = the (?msgs q)" proof - from HO obtain q where q: "q ∈ HOs m p" by auto with v have "HOV ?msgs (the (?msgs q)) ≠ {}" by (auto simp: HOV_def HOrcvdMsgs_def) hence HOp: "0 < card (HOV ?msgs (the (?msgs q)))" by auto also from v have "… ≤ card (HOV ?msgs v)" by (simp add: MFR_def) finally have "HOV ?msgs v ≠ {}" by auto thus ?thesis by (auto simp: HOV_def HOrcvdMsgs_def) qed text ‹ @{term "TwoThirds msgs v"} holds if value ‹v› has been received from more than $2/3$ of all processes. › definition TwoThirds where "TwoThirds msgs v ≡ (2*N) div 3 < card (HOV msgs v)" text ‹ The next-state relation of algorithm \emph{One-Third Rule} for every process is defined as follows: if the process has received values from more than $2/3$ of all processes, the ‹last_vote› field is set to the smallest among the most frequently received values, and the process decides value $v$ if it received $v$ from more than $2/3$ of all processes. If ‹p› hasn't heard from more than $2/3$ of all processes, the state remains unchanged. (Note that ‹Some› is the constructor of the option datatype, whereas ‹ϵ› is Hilbert's choice operator.) We require the type of values to be linearly ordered so that the minimum is guaranteed to be well-defined. › definition OTR_nextState where "OTR_nextState r p (st::('val::linorder) pstate) msgs st' ≡ if (2*N) div 3 < card {q. msgs q ≠ None} then st' = ⦇ last_vote = Min {v . MFR msgs v}, decision = (if (∃v. TwoThirds msgs v) then Some (ϵv. TwoThirds msgs v) else decision st) ⦈ else st' = st" text ‹ The message sending function is very simple: at every round, every process sends its current proposal (field ‹last_vote› of its local state) to all processes. › definition OTR_sendMsg where "OTR_sendMsg r p q st ≡ last_vote st" subsection ‹Communication predicate for \emph{One-Third Rule}› text ‹ We now define the communication predicate for the \emph{One-Third Rule} algorithm to be correct. It requires that, infinitely often, there is a round where all processes receive messages from the same set ‹Π› of processes where ‹Π› contains more than two thirds of all processes. The ``per-round'' part of the communication predicate is trivial. › definition OTR_commPerRd where "OTR_commPerRd HOrs ≡ True" definition OTR_commGlobal where "OTR_commGlobal HOs ≡ ∀r. ∃r0 Π. r0 ≥ r ∧ (∀p. HOs r0 p = Π) ∧ card Π > (2*N) div 3" subsection ‹The \emph{One-Third Rule} Heard-Of machine› text ‹ We now define the HO machine for the \emph{One-Third Rule} algorithm by assembling the algorithm definition and its communication-predicate. Because this is an uncoordinated algorithm, the ‹crd› arguments of the initial- and next-state predicates are unused. › definition OTR_HOMachine where "OTR_HOMachine = ⦇ CinitState = (λ p st crd. OTR_initState p st), sendMsg = OTR_sendMsg, CnextState = (λ r p st msgs crd st'. OTR_nextState r p st msgs st'), HOcommPerRd = OTR_commPerRd, HOcommGlobal = OTR_commGlobal ⦈" abbreviation "OTR_M ≡ OTR_HOMachine::(process, 'val::linorder pstate, 'val) HOMachine" end