Theory LastVotingDefs

theory LastVotingDefs
imports "../HOModel"
begin

section ‹Verification of the \emph{LastVoting} Consensus Algorithm›

text ‹
  The \emph{LastVoting} algorithm can be considered as a representation of
  Lamport's Paxos consensus algorithm~\<^cite>‹"lamport:part-time"›
  in the Heard-Of model. It is a coordinated algorithm designed to
  tolerate benign failures. Following~\<^cite>‹"charron:heardof"›, we formalize
  its proof of correctness in Isabelle, 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 CHO model.
›

typedecl Proc ― ‹the set of processes›
axiomatization where Proc_finite: "OFCLASS(Proc, finite_class)"
instance Proc :: finite by (rule Proc_finite)

abbreviation
  "N ≡ card (UNIV::Proc set)"   ― ‹number of processes›

text ‹
  The algorithm proceeds in \emph{phases} of $4$ rounds each (we call
  \emph{steps} the individual rounds that constitute a phase).
  The following utility functions compute the phase and step of a round,
  given the round number.
›

definition phase where "phase (r::nat) ≡ r div 4"

definition step where "step (r::nat) ≡ r mod 4"

lemma phase_zero [simp]: "phase 0 = 0"
by (simp add: phase_def)

lemma step_zero [simp]: "step 0 = 0"
by (simp add: step_def)

lemma phase_step: "(phase r * 4) + step r = r"
  by (auto simp add: phase_def step_def)

text ‹
  The following record models the local state of a process.
›

record 'val pstate =
  x :: 'val                ― ‹current value held by process›
  vote :: "'val option"    ― ‹value the process voted for, if any›
  commt :: bool            ― ‹did the process commit to the vote?›
  ready :: bool            ― ‹for coordinators: did the round finish successfully?›
  timestamp :: nat         ― ‹time stamp of current value›
  decide :: "'val option"  ― ‹value the process has decided on, if any›
  coordΦ :: Proc           ― ‹coordinator for current phase›

text ‹
  Possible messages sent during the execution of the algorithm.
›

datatype 'val msg =
  ValStamp "'val" "nat"
| Vote "'val"
| Ack
| Null  ― ‹dummy message in case nothing needs to be sent›

text ‹
  Characteristic predicates on messages.
›

definition isValStamp where "isValStamp m ≡ ∃v ts. m = ValStamp v ts"

definition isVote where "isVote m ≡ ∃v. m = Vote v"

definition isAck where "isAck m ≡ m = Ack"

text ‹
  Selector functions to retrieve components of messages. These functions
  have a meaningful result only when the message is of an appropriate kind.
›

fun val where
  "val (ValStamp v ts) = v"
| "val (Vote v) = v"

fun stamp where
  "stamp (ValStamp v ts) = ts"

text ‹
  The ‹x› field of the initial state is unconstrained, all other
  fields are initialized appropriately.
›

definition LV_initState where
  "LV_initState p st crd ≡
     vote st = None
   ∧ ¬(commt st)
   ∧ ¬(ready st)
   ∧ timestamp st = 0
   ∧ decide st = None
   ∧ coordΦ st = crd"

text ‹
  We separately define the transition predicates and the send functions
  for each step and later combine them to define the overall next-state relation.
›

― ‹processes from which values and timestamps were received›
definition valStampsRcvd where
  "valStampsRcvd (msgs :: Proc ⇀ 'val msg) ≡
   {q . ∃v ts. msgs q = Some (ValStamp v ts)}"

definition highestStampRcvd where
  "highestStampRcvd msgs ≡ 
   Max {ts . ∃q v. (msgs::Proc ⇀ 'val msg) q = Some (ValStamp v ts)}"

text ‹
  In step 0, each process sends its current ‹x› and ‹timestamp›
  values to its coordinator.

  A process that considers itself to be a coordinator updates its
  ‹vote› field if it has received messages from a majority of processes.
  It then sets its ‹commt› field to true.
›

definition send0 where
  "send0 r p q st ≡
   if q = coordΦ st then ValStamp (x st) (timestamp st) else Null"

definition next0 where
  "next0 r p st msgs crd st' ≡
      if p = coordΦ st ∧ card (valStampsRcvd msgs) > N div 2
      then (∃p v. msgs p = Some (ValStamp v (highestStampRcvd msgs))
                ∧ st' = st ⦇ vote := Some v, commt := True ⦈ )
      else st' = st"

text ‹
  In step 1, coordinators that have committed send their vote to all
  processes.

  Processes update their ‹x› and ‹timestamp› fields if they
  have received a vote from their coordinator.
›

definition send1 where
  "send1 r p q st ≡
   if p = coordΦ st ∧ commt st then Vote (the (vote st)) else Null"

definition next1 where
  "next1 r p st msgs crd st' ≡
   if msgs (coordΦ st) ≠ None ∧ isVote (the (msgs (coordΦ st)))
   then st' = st ⦇ x := val (the (msgs (coordΦ st))), timestamp := Suc(phase r) ⦈
   else st' = st"

text ‹
  In step 2, processes that have current timestamps send an acknowledgement
  to their coordinator.

  A coordinator sets its ‹ready› field to true if it receives a majority
  of acknowledgements.
›

definition send2 where
  "send2 r p q st ≡
   if timestamp st = Suc(phase r) ∧ q = coordΦ st then Ack else Null"

― ‹processes from which an acknowledgement was received›
definition acksRcvd where
  "acksRcvd (msgs :: Proc ⇀ 'val msg) ≡
   { q . msgs q ≠ None ∧ isAck (the (msgs q)) }"

definition next2 where
  "next2 r p st msgs crd st' ≡
   if p = coordΦ st ∧ card (acksRcvd msgs) > N div 2
   then st' = st ⦇ ready := True ⦈
   else st' = st"

text ‹
  In step 3, coordinators that are ready send their vote to all processes.

  Processes that received a vote from their coordinator decide on that value.
  Coordinators reset their ‹ready› and ‹commt› fields to false.
  All processes reset the coordinators as indicated by the parameter of
  the operator.
›

definition send3 where
  "send3 r p q st ≡
   if p = coordΦ st ∧ ready st then Vote (the (vote st)) else Null"

definition next3 where
  "next3 r p st msgs crd st' ≡
      (if msgs (coordΦ st) ≠ None ∧ isVote (the (msgs (coordΦ st)))
       then decide st' = Some (val (the (msgs (coordΦ st))))
       else decide st' = decide st)
   ∧ (if p = coordΦ st
      then ¬(ready st') ∧ ¬(commt st')
      else ready st' = ready st ∧ commt st' = commt st)
   ∧ x st' = x st
   ∧ vote st' = vote st
   ∧ timestamp st' = timestamp st
   ∧ coordΦ st' = crd"

text ‹
  The overall send function and next-state relation are simply obtained as
  the composition of the individual relations defined above.
›

definition LV_sendMsg :: "nat ⇒ Proc ⇒ Proc ⇒ 'val pstate ⇒ 'val msg" where
  "LV_sendMsg (r::nat) ≡
   if step r = 0 then send0 r
   else if step r = 1 then send1 r
   else if step r = 2 then send2 r
   else send3 r"


definition
  LV_nextState :: "nat ⇒ Proc ⇒ 'val pstate ⇒ (Proc ⇀ 'val msg) 
                       ⇒ Proc ⇒ 'val pstate ⇒ bool"
  where
  "LV_nextState r ≡
   if step r = 0 then next0 r
   else if step r = 1 then next1 r
   else if step r = 2 then next2 r
   else next3 r"


subsection ‹Communication Predicate for \emph{LastVoting}›

text ‹
  We now define the communication predicate that will be assumed for the
  correctness proof of the \emph{LastVoting} algorithm.
  The ``per-round'' part is trivial: integrity and agreement are always ensured.

  For the ``global'' part, Charron-Bost and Schiper propose a predicate
  that requires the existence of infinitely many phases ‹ph› such that:
  \begin{itemize}
  \item all processes agree on the same coordinator ‹c›,
  \item ‹c› hears from a strict majority of processes in steps 0 and 2
    of phase ‹ph›, and
  \item every process hears from ‹c› in steps 1 and 3 (this is slightly
    weaker than the predicate that appears in~\<^cite>‹"charron:heardof"›, but
    obviously sufficient).
  \end{itemize}

  Instead of requiring infinitely many such phases, we only assume the
  existence of one such phase (Charron-Bost and Schiper note that this is enough.)
›

definition
  LV_commPerRd where
  "LV_commPerRd r (HO::Proc HO) (coord::Proc coord) ≡ True"

definition
  LV_commGlobal where
  "LV_commGlobal HOs coords ≡
      ∃ph::nat. ∃c::Proc.
           (∀p. coords (4*ph) p = c)
         ∧ card (HOs (4*ph) c) > N div 2
         ∧ card (HOs (4*ph+2) c) > N div 2
         ∧ (∀p. c ∈ HOs (4*ph+1) p ∩ HOs (4*ph+3) p)"


subsection ‹The \emph{LastVoting} Heard-Of Machine›

text ‹
  We now define the coordinated HO machine for the \emph{LastVoting} algorithm
  by assembling the algorithm definition and its communication-predicate.
›

definition LV_CHOMachine where
  "LV_CHOMachine ≡
    ⦇ CinitState = LV_initState,
      sendMsg = LV_sendMsg,
      CnextState = LV_nextState,
      CHOcommPerRd = LV_commPerRd,
      CHOcommGlobal = LV_commGlobal ⦈"

abbreviation 
  "LV_M ≡ (LV_CHOMachine::(Proc, 'val pstate, 'val msg) CHOMachine)"

end