The Single-Decree Synod: Overview

The Single-Decree Synod is the foundational protocol for nodes to agree on a single value and that all additional protocols are built upon.

Of course, Lamport doesn't want to spell that out simply. We're suddenly thrust us back even further in time. Now instead of legislators we have priests in a synod coming up with the original protocol.

2 The Single-Decree Synod
The Paxon Parliament evolved from an earlier ceremonial Synod of priests that was convened every 19 years to choose a single, symbolic decree. For centuries, the Synod had chosen the decree by a conventional procedure that required all priests to be present. But as commerce flourished, priests began wandering in and out of the Chamber while the Synod was in progress. Finally, the old protocol failed, and a Synod ended with no decree chosen. To prevent a repetition of this theological disaster, Paxon religious leaders asked mathematicians to formulate a protocol for choosing the Synod’s decree. The protocol’s requirements and assumptions were essentially the same as those of the later Parliament except that instead of containing a sequence of decrees, a ledger would have at most one decree.
LAMPORT, P. 5 — §2

Bluntly this layer to the allegory is just fucking stupid it adds nothing of value and additional cognitive overhead. Legislators or Priests they're all nodes. The religious overtones mean nothing besides maybe a slight node to Math being a religion onto itself and how this implementation requires a bit of faith on the constraints holding. The paper's main concern in why the algorithm works not how to actually implement it. Leslie conceives of solutions from first principles and correctness more then anything else. As he remarked in a lecture about paxos in Russia in 2019:

This Piece of Magic
What's important now is to understand - and I don't expect you to understand it now. But as you are reading now and go back and read the lectures the important thing is to think about it's not how this piece of magic is implemented but that given this piece of magic we've satisfied consensus.
Lamport, Leslie. Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1. YouTube video, 2019. Quoted at 1:12:32–1:12:52. Source

Below is a overview of what Section 2 covers in what I hope is an understandable format.

  • §2.1 Mathematical Results

    By far one of the most overloaded section of the white paper which is doing the following

    1. Defining the Ballot Concept/Container/Set formally $\mathcal{B}$
    2. Three constraints on a set of ballots that if true would guarantee consistency as shown by the latter sections.
    3. The proof proving this logically which consists of
      1. The formal definitions of the three constraints
      2. The formal definition of three functions
      3. A lemma proving the point that for any successful ballot with a larger id with a different decree it must be part of the null set. Hence it cannot exist.
      4. Proof of the Lemma by contradiction
      5. A theorem that states that any decree that comes from a ballot greater than a successful ballot must have the same decree.
      6. A theorem that states that any decree that comes from a ballot greater than a successful ballot must have the same decree.
      7. A final theorem that this will hold for all future ballots for this decree.

  • §2.2 The Preliminary Protocol

    This section introduces the preliminary protocol that satisfies these three constraints and hence guarantees safety for a single decree.

  • §2.3 The Basic Protocol

    Refines the Preliminary Protocol for crash resistance and metadata storage with the addition of simplifying what information a node need to stores to be correct and more easily ignore stale messages.

  • §2.4 The Complete Protocol

    Refines the Basic Protocol with the idea of of leadership and timers to optimize for performance while maintaining safety and increasing liveliness.

We have a lot of ground to cover.

← Assumptions
Synod Overview
Decree Example →