Theory CT_Defs

section ‹Chandra-Toueg $\diamond S$ Algorithm›

theory CT_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps

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

record 'val pstate =
  x :: 'val                ― ‹current value held by process›
  mru_vote :: "(nat × 'val) option"
  commt :: "'val"   ― ‹for coordinators: the value processes are asked to commit to›
  decide :: "'val option"  ― ‹value the process has decided on, if any›

text ‹The algorithm relies on a coordinator for each phase of the algorithm.
  A phase lasts three rounds. The HO model formalization already provides the 
  infrastructure for this, but unfortunately the coordinator is not passed to
  the @{term sendMsg} function. Using the infrastructure would thus require 
  additional invariants and proofs; for simplicity, we use a global 
  constant instead.›

consts coord :: "nat  process"
specification (coord)
  coord_phase[rule_format]: "r r'. three_phase r = three_phase r'  coord r = coord r'"

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

datatype 'val msg =
  ValStamp "'val" "nat"
| NeverVoted
| Vote "'val"
| 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"

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"

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

definition CT_initState where
  "CT_initState p st crd 
   mru_vote st = None
    decide st = None

definition mru_vote_to_msg :: "'val pstate  'val msg" where
  "mru_vote_to_msg st  case mru_vote st of
    Some (ts, v)  ValStamp v ts
    | None  NeverVoted"

fun msg_to_val_stamp :: "'val msg  (round × 'val)option" where
  "msg_to_val_stamp (ValStamp v ts) = Some (ts, v)"
  | "msg_to_val_stamp _ = None"

definition msgs_to_lvs ::
  "(process  'val msg)
   (process, round × 'val) map"
  "msgs_to_lvs msgs  msg_to_val_stamp m msgs"

definition send0 where
  "send0 r p q st 
   if q = coord r then mru_vote_to_msg st else Null"

definition next0 
  :: "nat 
   'val pstate 
   (process  'val msg)
   'val pstate
  "next0 r p st msgs crd st'  let Q = dom msgs; lvs = msgs_to_lvs msgs in
      if p = coord r
      then (st' = st  commt := (case_option (x st) snd (option_Max_by fst (ran (lvs |` Q))))  )
      else st' = st"

definition send1 where
  "send1 r p q st 
   if p = coord r then Vote (commt st) else Null"

definition next1 
  :: "nat 
   'val pstate 
   (process  'val msg)
   'val pstate
  "next1 r p st msgs crd st' 
   if msgs (coord r)  None
   then st' = st  mru_vote := Some (three_phase r, val (the (msgs (coord r))))  
   else st' = st"

definition send2 where
  "send2 r p q st  (case mru_vote st of
    Some (phs, v)  (if phs = three_phase r then Vote v else Null)
    | _  Null

― ‹processes from which a vote was received›
definition votes_rcvd where
  "votes_rcvd (msgs :: process  'val msg) 
   { (q, v) . msgs q = Some (Vote v) }"

definition the_rcvd_vote where
  "the_rcvd_vote (msgs :: process  'val msg)  SOME v. v  snd ` votes_rcvd msgs"

definition next2 where
  "next2 r p st msgs crd st' 
   if card (votes_rcvd msgs) > N div 2
   then st' = st  decide := Some (the_rcvd_vote msgs) 
   else st' = st

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

definition CT_sendMsg :: "nat  process  process  'val pstate  'val msg" where
  "CT_sendMsg (r::nat) 
   if three_step r = 0 then send0 r
   else if three_step r = 1 then send1 r
   else send2 r"

  CT_nextState :: "nat  process  'val pstate  (process  'val msg) 
                        process  'val pstate  bool"
  "CT_nextState r 
   if three_step r = 0 then next0 r
   else if three_step r = 1 then next1 r
   else next2 r"

subsection ‹The \emph{CT} Heard-Of machine›

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

definition CT_Alg where
     CinitState = CT_initState,
      sendMsg = CT_sendMsg,
      CnextState = CT_nextState "

text ‹The CT algorithm relies on \emph{waiting}: in each round, the
  coordinator waits until it hears from $\frac{N}{2}$ processes. This
  it reflected in the following per-round predicate.›

  CT_commPerRd :: "nat  process HO  process coord  bool" 
  "CT_commPerRd r HOs crds  
    three_step r = 0  card (HOs (coord r)) > N div 2"

  CT_commGlobal where
  "CT_commGlobal HOs coords 
      ph::nat. c::process.
           coord (nr_steps*ph) = c
          (p. c  HOs (nr_steps*ph+1) p)
          (p. card (HOs (nr_steps*ph+2) p) > N div 2)"

definition CT_CHOMachine where
     CinitState = CT_initState,
      sendMsg = CT_sendMsg,
      CnextState = CT_nextState,
      CHOcommPerRd = CT_commPerRd,
      CHOcommGlobal = CT_commGlobal "
  "CT_M  (CT_CHOMachine::(process, 'val pstate, 'val msg) CHOMachine)"