Paxos Consensus

Single-decree Paxos (Synod protocol) from Lamport’s “Paxos Made Simple”. The spec verifies that if two ballots both achieve majority acceptance, they must have proposed the same value.

The spec

Source

module Paxos

// Single-decree Paxos (Synod protocol)
// From: Lamport, "The Part-Time Parliament" / "Paxos Made Simple"
// Safety formulation based on Lamport's Voting/Paxos TLA+ specs
// N is the last acceptor index (N+1 acceptors, 0..N)
// MaxBallot is the last ballot number (0..MaxBallot)
// V is the last value index (V+1 possible values, 0..V)
// Quick BFS:       specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock --fast
//                  316K states, <1s
// Strenuous BFS:   specl check paxos.specl -c N=3 -c MaxBallot=3 -c V=2 --no-deadlock --fast
//                  3.35M states, ~9s
// Quick symbolic:  specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock --symbolic
//                  k-induction, 0.03s
// Strenuous sym:   specl check paxos.specl -c N=10 -c MaxBallot=10 -c V=3 --no-deadlock --symbolic
//                  k-induction, ~90s

const N: Int
const MaxBallot: Int
const V: Int

// Per acceptor: highest ballot promised (-1 = none)
var maxBal: Dict[Int, Int]

// Per acceptor: highest ballot voted in (-1 = never voted)
var maxVBal: Dict[Int, Int]

// Per acceptor: value of highest vote (-1 = never voted)
var maxVal: Dict[Int, Int]

// Per ballot: proposed value (-1 = not yet proposed)
var proposed: Dict[Int, Int]

// Per ballot × acceptor: has accepted?
var accepted: Dict[Int, Dict[Int, Bool]]

// A value v is safe to propose at ballot b if there exists a quorum Q
// (majority of acceptors) where all members promised b and either:
// (a) no member has ever voted, or
// (b) the highest vote among Q members below b has value v
func SafeAt(b, v) {
    any Q in powerset(0..N):
        len(Q) * 2 > N + 1
        and (all a in Q: maxBal[a] >= b)
        and (
            (all a in Q: maxVBal[a] == -1)
            or (any c in 0..MaxBallot:
                c < b
                and (all a in Q: maxVBal[a] <= c)
                and (any a in Q: maxVBal[a] == c and maxVal[a] == v)))
}

init {
    maxBal = {a: -1 for a in 0..N};
    maxVBal = {a: -1 for a in 0..N};
    maxVal = {a: -1 for a in 0..N};
    proposed = {b: -1 for b in 0..MaxBallot};
    accepted = {b: {a: false for a in 0..N} for b in 0..MaxBallot};
}

// Acceptor a promises not to participate in any ballot lower than b
action Promise(b: 0..MaxBallot, a: 0..N) {
    require b > maxBal[a];
    maxBal = maxBal | {a: b};
}

// Proposer proposes value v for ballot b (must be safe)
action Propose(b: 0..MaxBallot, v: 0..V) {
    require proposed[b] == -1;
    require SafeAt(b, v);
    proposed = proposed | {b: v};
}

// Acceptor a votes for the proposed value in ballot b
action Accept(b: 0..MaxBallot, a: 0..N) {
    require proposed[b] != -1;
    require maxBal[a] <= b;
    maxBal = maxBal | {a: b};
    maxVBal = maxVBal | {a: b};
    maxVal = maxVal | {a: proposed[b]};
    accepted = accepted | {b: (accepted[b] | {a: true})};
}

// Agreement: if two ballots both achieve majority acceptance,
// they must have proposed the same value
invariant Agreement {
    all b1 in 0..MaxBallot: all b2 in 0..MaxBallot:
        (len({a in 0..N if accepted[b1][a]}) * 2 > N + 1
         and len({a in 0..N if accepted[b2][a]}) * 2 > N + 1)
        implies proposed[b1] == proposed[b2]
}

// Validity: any proposed value is in the valid range
invariant Validity {
    all b in 0..MaxBallot: proposed[b] != -1 implies (proposed[b] >= 0 and proposed[b] <= V)
}

What to notice

• powerset and nested quantifiers. The SafeAt function iterates over all subsets of acceptors (powerset(0..N)) to find a quorum that satisfies the safety condition. This is the most complex expression in any showcase spec.
• Set comprehensions for quorum check. len({a in 0..N if accepted[b][a]}) * 2 > N + 1 counts accepted votes.
• Both BFS and symbolic. This is the best example for exercising both verification modes: BFS at N=3 (3.35M states, ~9s), symbolic at N=10 (k-induction, ~90s).

specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock