Distributed algorithms for solving the consensus problem

In the consensus problem, each process of a distributed algorithm is given a boolean value at the beginning. Then by exchanging messages asynchronously, they are supposed to agree on one of the initial boolean values. This file contains a very general definition of such a distributed algorithm.

Borrowing an idea from Leslie Lamport, we allow the LTS defined by such an algorithm to "stutter" at any time, in the sense of taking a dummy step without changing the global state of the distributed algorithm. This idea enables us to focus on infinite executions alone without loss of generality, because an algorithm that has run out of useful steps to take can always take the stuttering step. Pathological executions in which the stuttering step is taken forever when there is useful work to be done are outlawed by the fairness assumptions defined in Consensus.lean.

The types P, M, and S below are the types of processes (more precisely, process identifiers), messages contents, and process states. Eventually P will be assumed to be finite in the form of [Fintype P], but that assumption will be added only where necessary. No assumption whatsoever will be made about M and S. In particular, they could be infinite.

structure Cslib.FLP.Message (P : Type u_4) (M : Type u_5) : Type (max u_4 u_5)

The type of messages that processes send to each other.

• dest : P

  The destination of a message.

• msg : Bool ⊕ M

  The content of the message, where the Bool option is used to carry to the initial boolean value to each process.

theorem Cslib.FLP.Message.ext {P : Type u_4} {M : Type u_5} {x y : Message P M} (dest : x.dest = y.dest) (msg : x.msg = y.msg) : x = y

theorem Cslib.FLP.Message.ext_iff {P : Type u_4} {M : Type u_5} {x y : Message P M} : x = y ↔ x.dest = y.dest ∧ x.msg = y.msg

def Cslib.FLP.instDecidableEqMessage.decEq {P✝ : Type u_4} {M✝ : Type u_5} [DecidableEq P✝] [DecidableEq M✝] (x✝ x✝¹ : Message P✝ M✝) : Decidable (x✝ = x✝¹)

Equations

• Cslib.FLP.instDecidableEqMessage.decEq { dest := a, msg := a_1 } { dest := b, msg := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cslib.FLP.instDecidableEqMessage {P✝ : Type u_4} {M✝ : Type u_5} [DecidableEq P✝] [DecidableEq M✝] : DecidableEq (Message P✝ M✝)

Equations

• Cslib.FLP.instDecidableEqMessage = Cslib.FLP.instDecidableEqMessage.decEq

structure Cslib.FLP.ProcState (S : Type u_4) : Type u_4

The type of a process's local state.

• state : S

  The internal state of a process.

• out : Option Bool

  The state component used by a process to signal the boolean value it decides on.

structure Cslib.FLP.State (P : Type u_4) (M : Type u_5) (S : Type u_6) : Type (max (max u_4 u_5) u_6)

The global state of the distributed algorithm.

• msgs : Multiset (Message P M)

  A multiset containing all messages that are in-flight (namely, they have been sent but not yet received). Note that being a multiset implies that the messages are not ordered.

• proc : P → ProcState S

  A map giving the local states of all processes.

structure Cslib.FLP.Algorithm (P : Type u_4) (M : Type u_5) (S : Type u_6) : Type (max (max u_4 u_5) u_6)

The specification of a distributed algorithm for solving the consensus problem. Note that each field below can depend on a process's identifier (recall that each Message contains its destination's identifier), so the algorithm is not required to be uniform across processes.

• init : P → S

  A map specifying the initial state of each process.

• next : Message P M → ProcState S → S

  A map specifying how a process changes its internal state upon receiving a message.

• send : Message P M → ProcState S → Multiset (Message P M)

  A map specifying what messages a process sends out upon receiving a message.

• out : Message P M → ProcState S → Option Bool

  A map specifying the boolean decision a process makes upon receiving a message, where none means that no decision is made.

@[reducible, inline]

abbrev Cslib.FLP.Action (P : Type u_4) (M : Type u_5) : Type (max u_5 u_4)

The type of labels of the LTS defined by an Algorithm, where some m denotes the reception of message m and none denotes a stuttering step.

Equations

• Cslib.FLP.Action P M = Option (Cslib.FLP.Message P M)

def Cslib.FLP.DestIn {P : Type u_1} {M : Type u_2} (ps : Set P) : Action P M → Prop

DestIn ps x means that if x ≠ none, then x = some m with m.dest ∈ ps.

Equations

• Cslib.FLP.DestIn ps (some m) = (m.dest ∈ ps)
• Cslib.FLP.DestIn ps none = True

def Cslib.FLP.Algorithm.start {P : Type u_1} {M : Type u_2} {S : Type u_3} [Fintype P] (a : Algorithm P M S) (inp : P → Bool) : State P M S

Given inp : P → Bool, the initial state of the algorithm a contains a single message carrying the boolean value inp p to each process p, where the initial internal state is a.init p and no decision has been made. The assumption [Fintype P] is made because a multiset may contain only finitely many elements.

Equations

• a.start inp = { msgs := Multiset.map (fun (p : P) => { dest := p, msg := Sum.inl (inp p) }) Finset.univ.val, proc := fun (p : P) => { state := a.init p, out := none } }

def Cslib.FLP.Algorithm.recvMsg {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (m : Message P M) (s : State P M S) : State P M S

The specification of how the global state of the algorithm changes when a process p receives a message m. (This function will be used only when such a message m exists.) Note that once p has made a boolean decision in its out field, it is not allowed to "change its mind" anymore.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.FLP.Algorithm.lts {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) : LTS (State P M S) (Action P M)

The transition relation of the LTS defined by the algorithm a. Note that the stuttering step is always allowed.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.FLP.Algorithm.Reachable {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (inp : P → Bool) (s : State P M S) : Prop

a.Reachable inp s means that s is a reachable state of a given the initial inp.

Equations

• a.Reachable inp s = a.lts.CanReach (a.start inp) s

@[reducible, inline]

abbrev Cslib.FLP.State.ProcDecided {P : Type u_1} {M : Type u_2} {S : Type u_3} (s : State P M S) (p : P) (b : Bool) : Prop

s.ProcDecided p b means that process p is decided on the boolean value b in the state s.

Equations

• s.ProcDecided p b = ((s.proc p).out = some b)

def Cslib.FLP.State.Decided {P : Type u_1} {M : Type u_2} {S : Type u_3} (s : State P M S) (b : Bool) : Prop

s.Decided b means that at least one process is decided on the boolean value b in the state s.

Equations

• s.Decided b = ∃ (p : P), s.ProcDecided p b

def Cslib.FLP.State.Agreed {P : Type u_1} {M : Type u_2} {S : Type u_3} (s : State P M S) : Prop

s.Agreed says that all boolean values decided on in state s must agree with each other.

Equations

• s.Agreed = ∀ (b b' : Bool), s.Decided b ∧ s.Decided b' → b = b'

def Cslib.FLP.Algorithm.SafeConsensus {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) : Prop

a.SafeConsensus says that in any reachable state of a, (1) all boolean values decided on in that state must agree with each other and (2) that boolean value (if it exists) must be one of the boolean values given by inp at the beginning. a.SafeConsensus is the minimal correctness requirement on a and is a safety property (hence its name).

Equations

• a.SafeConsensus = ∀ (inp : P → Bool) (s : Cslib.FLP.State P M S), a.Reachable inp s → s.Agreed ∧ ∀ (b : Bool), s.Decided b → ∃ (p : P), inp p = b

theorem Cslib.FLP.Algorithm.tr_none {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s s' : State P M S} (h : a.lts.Tr s none s') : s = s'

The stuttering step does not change the global state.

theorem Cslib.FLP.Algorithm.reachable_start {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] : a.Reachable inp (a.start inp)

The initial state is reachable.

theorem Cslib.FLP.Algorithm.reachable_stable {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] {s s' : State P M S} (hr : a.Reachable inp s) (hc : a.lts.CanReach s s') : a.Reachable inp s'

If s is reachable from the initial state and s' is reachable from s, then s' is reachable from the initial state.

theorem Cslib.FLP.Algorithm.procDecided_stable {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s s' : State P M S} {p : P} {b : Bool} (hd : s.ProcDecided p b) (hc : a.lts.CanReach s s') : s'.ProcDecided p b

If p is decided on the boolean value b in s and s' is reachable from s, then p is still decided on b in s'.

theorem Cslib.FLP.Algorithm.decided_stable {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s s' : State P M S} {b : Bool} (hd : s.Decided b) (hc : a.lts.CanReach s s') : s'.Decided b

If at least one process is decided on the boolean value b in s and s' is reachable from s, then at least one process is still decided on b in s'.

theorem Cslib.FLP.Algorithm.recvMsg_comm {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {m1 m2 : Message P M} {s : State P M S} (hd : m1.dest ≠ m2.dest) (h1 : m1 ∈ s.msgs) (h2 : m2 ∈ s.msgs) : m2 ∈ (a.recvMsg m1 s).msgs ∧ m1 ∈ (a.recvMsg m2 s).msgs ∧ a.recvMsg m2 (a.recvMsg m1 s) = a.recvMsg m1 (a.recvMsg m2 s)

If m1 and m2 are both inflight and they have different destinations, then receiving them in either order produces the same end state.

theorem Cslib.FLP.Algorithm.tr_diamond {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {x1 x2 : Action P M} {s s1 s2 : State P M S} (hx1 : DestIn ps x1) (hs1 : a.lts.Tr s x1 s1) (hx2 : DestIn psᶜ x2) (hs2 : a.lts.Tr s x2 s2) : ∃ (s' : State P M S), a.lts.Tr s1 x2 s' ∧ a.lts.Tr s2 x1 s'

A diamond property for the transition relation a.lts.Tr.

theorem Cslib.FLP.Algorithm.mTr_notRcvd_enabled {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s t : State P M S} {xl : List (Action P M)} {m : Message P M} (hst : a.lts.MTr s xl t) (hs : m ∈ s.msgs) (hxl : some m ∉ xl) : m ∈ t.msgs

A message that is in-flight stays in-flight as long as it is not received (finite execution version).

theorem Cslib.FLP.Algorithm.omega_notRcvd_enabled {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {k : ℕ} {m : Message P M} (he : a.lts.OmegaExecution ss xs) (hm : m ∈ (ss k).msgs) (hn : ∀ (j : ℕ), k ≤ j → xs j ≠ some m) (j : ℕ) : k ≤ j → m ∈ (ss j).msgs

A message that is in-flight stays in-flight as long as it is not received (infinite execution version).