Theory Paxos_Defs
section ‹The Paxos Algorithm›
theory Paxos_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps
begin
text ‹
This is a modified version (closer to the original Paxos) of PaxosDefs from the Heard Of
entry in the AFP.›
subsection ‹Model of the algorithm›
text ‹
The following record models the local state of a process.
›
record 'val pstate =
x :: 'val
mru_vote :: "(nat × 'val) option"
commt :: "'val option"
decide :: "'val option"
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'"
by(auto)
text ‹
Possible messages sent during the execution of the algorithm.
›