Two-phase commit

InductiveCoordinator states#✓fully proved

In two-phase commit the coordinator is in one of three states: waiting (collecting votes), committed (it has decided commit) or aborted (it has decided abort).

inductive CoordState
  /-- Collecting votes. -/
  | waiting
  /-- Decided commit. -/
  | committed
  /-- Decided abort. -/
  | aborted
  deriving DecidableEq

Used by 14

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · Initial state of two-phase commit · Two-phase commit invariant · Multistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · A committed participant has a committed coordinator · Updating one participant's state · Global states of two-phase commit · Transitions of two-phase commit

InductiveParticipant states in two-phase commit#✓fully proved

A participant is in one of four states: working (it has not voted), prepared (it voted yes and waits for the decision), committed, or aborted (it voted no, or learned of an abort).

inductive PartState
  /-- Has not voted. -/
  | working
  /-- Voted yes; waits for the decision. -/
  | prepared
  /-- Committed. -/
  | committed
  /-- Aborted (voted no, or learned an abort). -/
  | aborted
  deriving DecidableEq

Used by 14

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · Initial state of two-phase commit · Two-phase commit invariant · Multistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · A committed participant has a committed coordinator · Updating one participant's state · Global states of two-phase commit · Transitions of two-phase commit

StructureGlobal states of two-phase commit#✓fully proved

For a set \(P\) of participants, a global state consists of a coordinator state together with a participant state for each participant \(p \in P\).

structure State (P : Type*) where
  /-- The coordinator's state. -/
  coord : CoordState
  /-- Each participant's state. -/
  part : P → PartState

Uses 2 · Used by 16

Statement usesCoordinator states · Participant states in two-phase commit

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · Initial state of two-phase commit · Two-phase commit invariant · Multistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · Two-phase commit as a transition system · A committed participant has a committed coordinator · Reachable states of two-phase commit · Updating one participant's state · Transitions of two-phase commit · Reachable states are closed under steps

InductiveTwo-phase commit actions#✓fully proved

The actions of the two-phase commit protocol over a set \(P\) of participants are: a participant \(p \in P\) votes yes; a participant \(p\) votes no; the coordinator decides commit; the coordinator decides abort; a participant \(p\) learns the commit decision; and a participant \(p\) learns the abort decision.

inductive Action (P : Type*)
  | voteYes (p : P)
  | voteNo (p : P)
  | decideCommit
  | decideAbort
  | learnCommit (p : P)
  | learnAbort (p : P)

Used by 6

Used byMultistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · Two-phase commit as a transition system · Reachable states of two-phase commit · Transitions of two-phase commit · Reachable states are closed under steps

DefinitionUpdating one participant's state#✓fully proved

For a global state \(s\), a participant \(p\) and a participant state \(x\), the updated state has the same coordinator state as \(s\), gives participant \(p\) the state \(x\), and leaves the state of every other participant unchanged.

def State.setPart (s : State P) (p : P) (x : PartState) : State P :=
  ⟨s.coord, Function.update s.part p x⟩

Uses 3 · Used by 2

Statement usesCoordinator states · Participant states in two-phase commit · Global states of two-phase commit

Used byMultistep transitions preserve the two-phase commit invariant · Transitions of two-phase commit

InductiveTransitions of two-phase commit#✓fully proved

The protocol steps from a global state \(s\) to a global state \(t\) by an action exactly in the following cases. A working participant \(p\) may vote yes, after which \(p\) is prepared, or vote no, after which \(p\) is aborted. If the coordinator is waiting and every participant is prepared, the coordinator may decide commit, after which it is committed. If the coordinator is waiting, it may decide abort, after which it is aborted. If the coordinator has committed, a prepared participant \(p\) may learn the commit, after which \(p\) is committed. If the coordinator has aborted, a prepared or working participant \(p\) may learn the abort, after which \(p\) is aborted. In each step every other part of the state is unchanged.

Cslib.Distributed.TwoPhaseCommit.Step · 15 lines

inductive Step : State P → Action P → State P → Prop
  | voteYes (s : State P) (p : P) (h : s.part p = .working) :
      Step s (.voteYes p) (s.setPart p .prepared)
  | voteNo (s : State P) (p : P) (h : s.part p = .working) :
      Step s (.voteNo p) (s.setPart p .aborted)
  | decideCommit (s : State P) (hc : s.coord = .waiting) (h : ∀ p, s.part p = .prepared) :
      Step s .decideCommit ⟨.committed, s.part⟩
  | decideAbort (s : State P) (hc : s.coord = .waiting) :
      Step s .decideAbort ⟨.aborted, s.part⟩
  | learnCommit (s : State P) (p : P) (hc : s.coord = .committed)
      (h : s.part p = .prepared) :
      Step s (.learnCommit p) (s.setPart p .committed)
  | learnAbort (s : State P) (p : P) (hc : s.coord = .aborted)
      (h : s.part p = .prepared ∨ s.part p = .working) :
      Step s (.learnAbort p) (s.setPart p .aborted)

Uses 5 · Used by 3

Statement usesTwo-phase commit actions · Coordinator states · Participant states in two-phase commit · Global states of two-phase commit · Updating one participant's state

Used byMultistep transitions preserve the two-phase commit invariant · Two-phase commit as a transition system · Reachable states are closed under steps

DefinitionTwo-phase commit as a transition system#✓fully proved

For a set \(P\) of participants, the labelled transition system whose states are the global states of the protocol, whose labels are the protocol actions, and whose transitions are the protocol steps.

def lts : LTS (State P) (Action P) where
  Tr := Step

Uses 3 · Used by 4

Statement usesTwo-phase commit actions · Global states of two-phase commit · Transitions of two-phase commit

Used byMultistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · Reachable states of two-phase commit · Reachable states are closed under steps

DefinitionInitial state of two-phase commit#✓fully proved

The initial state of the two-phase commit protocol: the coordinator is waiting and every participant is working.

def initial : State P := ⟨.waiting, fun _ => .working⟩

Uses 3 · Used by 3

Statement usesCoordinator states · Participant states in two-phase commit · Global states of two-phase commit

Used byThe two-phase commit invariant holds in reachable states · Reachable states of two-phase commit · Reachable states are closed under steps

DefinitionReachable states of two-phase commit#✓fully proved

A global state \(s\) is reachable when some finite sequence of protocol actions leads by protocol steps from the initial state, in which the coordinator is waiting and every participant is working, to \(s\).

def Reachable (s : State P) : Prop := (lts (P := P)).CanReach initial s

Uses 4 · Used by 9

Statement usesTwo-phase commit actions · Global states of two-phase commit · Initial state of two-phase commit · Two-phase commit as a transition system

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · The two-phase commit invariant holds in reachable states · A committed participant has a committed coordinator · Reachable states are closed under steps

TheoremReachable states are closed under steps#✓fully proved

If a global state \(s\) of the two-phase commit protocol is reachable and some action takes \(s\) to \(t\) in one protocol step, then \(t\) is reachable.

theorem Reachable.step {s t : State P} {a : Action P} (hs : Reachable s) (h : Step s a t) :
    Reachable t

Uses 6

Statement usesTwo-phase commit actions · Reachable states of two-phase commit · Global states of two-phase commit · Transitions of two-phase commit

Proof usesInitial state of two-phase commit · Two-phase commit as a transition system

StructureTwo-phase commit invariant#✓fully proved

A global state \(s\) of the two-phase commit protocol satisfies the invariant when two conditions hold: if the coordinator has committed, then every participant is prepared or committed; and every committed participant has a committed coordinator.

structure Inv (s : State P) : Prop where
  coord_committed : s.coord = .committed →
    ∀ p, s.part p = .prepared ∨ s.part p = .committed
  part_committed : ∀ p, s.part p = .committed → s.coord = .committed

Uses 3 · Used by 9

Statement usesCoordinator states · Participant states in two-phase commit · Global states of two-phase commit

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · Multistep transitions preserve the two-phase commit invariant · The two-phase commit invariant holds in reachable states · A committed participant has a committed coordinator

TheoremMultistep transitions preserve the two-phase commit invariant#✓fully proved

If a state \(s\) of the two-phase commit protocol satisfies the inductive invariant and a state \(t\) is reached from \(s\) by a finite sequence of transitions, then \(t\) satisfies the invariant.

theorem inv_mtr {s t : State P} {as : List (Action P)} (hm : (lts (P := P)).MTr s as t)
    (hs : Inv s) : Inv t

Uses 8 · Used by 1

Statement usesTwo-phase commit actions · Two-phase commit invariant · Global states of two-phase commit · Two-phase commit as a transition system

Proof usesCoordinator states · Participant states in two-phase commit · Updating one participant's state · Transitions of two-phase commit

Used byThe two-phase commit invariant holds in reachable states

TheoremThe two-phase commit invariant holds in reachable states#✓fully proved

For every set \(P\) of participants, every global state of the two-phase commit protocol that is reachable from the initial state satisfies the inductive invariant, that is, both of the following hold: if the coordinator has committed, then every participant is prepared or committed; and every committed participant has a committed coordinator.

theorem inv_reachable {s : State P} (h : Reachable s) : Inv s

Uses 9 · Used by 7

Statement usesTwo-phase commit invariant · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit actions · Coordinator states · Participant states in two-phase commit · Initial state of two-phase commit · Multistep transitions preserve the two-phase commit invariant · Two-phase commit as a transition system

Used byAn aborted participant rules out a coordinator commit · Atomicity between participants · Validity for participants · An aborted coordinator has no committed participant · Validity for the coordinator · A committed coordinator has no aborted participant · A committed participant has a committed coordinator

TheoremAtomicity between participants#✓fully proved

For every set \(P\) of participants, in every reachable state of the two-phase commit protocol, if some participant \(p\) has committed, then no participant \(q\) has aborted.

This is the participant part of condition AC1 of Bernstein, Hadzilacos and Goodman.

theorem atomicity {s : State P} (h : Reachable s) {p q : P}
    (hp : s.part p = .committed) : s.part q ≠ .aborted

Uses 6

Statement usesParticipant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesCoordinator states · Two-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremValidity for the coordinator#✓fully proved

In every reachable state of the two-phase commit protocol, if the coordinator has decided commit, then every participant voted yes, that is, every participant is prepared or committed.

This is the coordinator form of condition AC3 of Bernstein, Hadzilacos and Goodman.

theorem coord_committed_imp_all_voted_yes {s : State P} (h : Reachable s)
    (hc : s.coord = .committed) (q : P) :
    s.part q = .prepared ∨ s.part q = .committed

Uses 6

Statement usesCoordinator states · Participant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremValidity for participants#✓fully proved

In every reachable state of the two-phase commit protocol, if some participant has committed, then every participant voted yes, that is, every participant is prepared or committed.

This is the participant form of condition AC3 of Bernstein, Hadzilacos and Goodman; that the coordinator has then decided commit is the separate result that a committed participant has a committed coordinator.

theorem committed_imp_all_voted_yes {s : State P} (h : Reachable s) {p : P}
    (hp : s.part p = .committed) (q : P) :
    s.part q = .prepared ∨ s.part q = .committed

Uses 6

Statement usesParticipant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesCoordinator states · Two-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremAn aborted participant rules out a coordinator commit#✓fully proved

In every reachable state of the two-phase commit protocol, if some participant has aborted, then the coordinator has not decided commit.

theorem aborted_imp_not_committed {s : State P} (h : Reachable s) {p : P}
    (hp : s.part p = .aborted) : s.coord ≠ .committed

Uses 6

Statement usesCoordinator states · Participant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremA committed participant has a committed coordinator#✓fully proved

In every reachable state of the two-phase commit protocol, if some participant has committed, then the coordinator has committed.

This is the atomicity condition AC1 of Bernstein, Hadzilacos and Goodman between a participant and the coordinator.

theorem part_committed_coord_committed {s : State P} (h : Reachable s) {p : P}
    (hp : s.part p = .committed) : s.coord = .committed

Uses 6

Statement usesCoordinator states · Participant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremA committed coordinator has no aborted participant#✓fully proved

In every reachable state of the two-phase commit protocol, if the coordinator has decided commit, then no participant has aborted.

This is the coordinator–participant part of condition AC1 of Bernstein, Hadzilacos and Goodman.

theorem coord_committed_part_not_aborted {s : State P} (h : Reachable s)
    (hc : s.coord = .committed) (q : P) : s.part q ≠ .aborted

Uses 6

Statement usesCoordinator states · Participant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit invariant · The two-phase commit invariant holds in reachable states

TheoremAn aborted coordinator has no committed participant#✓fully proved

In every reachable state of the two-phase commit protocol, if the coordinator has decided abort, then no participant has committed.

This is the coordinator–participant part of condition AC1 of Bernstein, Hadzilacos and Goodman.

theorem coord_aborted_part_not_committed {s : State P} (h : Reachable s)
    (hc : s.coord = .aborted) (q : P) : s.part q ≠ .committed

Uses 6

Statement usesCoordinator states · Participant states in two-phase commit · Reachable states of two-phase commit · Global states of two-phase commit

Proof usesTwo-phase commit invariant · The two-phase commit invariant holds in reachable states

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.