On correctness proof of Rabia

Background

I'm playing with TLA+ and thinking about how to specify the protocol. I'm not sure whether the desired proof is expressible in TLA+. So I'm trying to write a pen-and-paper proof first. Since it is informal, I cannot guarantee its correctness, but I try to make it as rigorous as possible.

Assumption

First, we assume there is a strict order of values proposed by clients (to abstract away the timestamp).

Network Assumption: "eventually successful delivery", no packet loss, large enough buffer to hold all messages.

State it formally: For any message m, there exists a time T when all (non-failed) nodes receive m.

Properties

The updated WeakMVC algorithm (errata):

INFO

# WeakMVC invoked with proposal p at a particular node.
# Phase 1: Exchange protocols.
Send(PROPOSAL, p) to all
Wait for ≥ n − f PROPOSAL messages
if proposal p appears more than ⌊ n / 2 ⌋ + 1 times:
    state ← p # Node will propose p
else:
    state ← ⊥ # Node will propose ⊥
# Phase 2: Use Ben-Or to reach agreement.
r ← 1
while True:
    Send(STATE, r, state) to all
    Wait until receiving ≥ n − f STATE messages for round r
    states ← set of sates in received STATE messages from round r # states has at most 2 elements.
    if state s appears ≥ ⌊ n / 2 ⌋ + 1 times in round-r STATE messages:
        v ← s
    else:
        v ← ?
    Send(VOTE, r, v) to all
    Wait until receiving ≥ n − f VOTE messages for round r
    if non-? vote v′ appears ≥ f + 1 times in round-r VOTEs:
        return v′ # Termination
    elif non-? vote v′ appears at least once in round-r VOTE messages:
        state ← v′
    else:
      # states (Line 15) must have exactly two elements: ⊥ and p a proposal selected in Phase 1.
      c ← CommonCoin(r)
      if c = 0:
          state ← ⊥
      else:
          state ← non-⊥ element p in states
    r ← r + 1

Properties from Ben-Or's

Corollary 3 (Uniform validity) If any process p decides v, then v is the initial value of some process.

Corollary 2 (Uniform agreement) If some processes p and p′ decide v and v′ in round k ≥ 1 and k′ ≥ 1, respectively, then v = v′.

Termination with probability 1.

Properties from WeakMVC (updated)

Majority: If a process decides a non-⊥ value v, then v is previously proposed by a majority of the processes.

This is an important property to of the updated algorithm. This ensures the safety of multiple Ben-Or consensus rounds.

Proof, Without Pipeline

There exists a time T when all the client requests is received by all the nodes. Then we need to prove two goals:

1. At time T, for the committed log: (a) agreement is reached, (b) validity (the value is proposed by a client), and (c) no double commit of the same value.
2. Whatever the log at time T is, the network will reach consensus on the remaining requests.

1(a) and 1(b) are ensured by Ben-Or's algorithm.

1(c) is ensured by the Majority property of WeakMVC: Prove by contradiction. Suppose one node commits the same value v twice at consensus round r and r′. Then, here must be a majority of nodes that propose v in both round r and round r′. These two majorities must intersect, so there exists a node that proposes v in both rounds. This contradicts with the algorithm that discards the duplicate proposal.

For 2, the remaining requests are defined as the client requests that are not in the committed log at time T. All the nodes will propose them in the same order, by Uniform validity, the decided value must be the proposed value, meaning that the remaining requests will be correctly decided.

Termination with probability 1 is still guaranteed, as long as the number of client requests is finite.

With Pipeline

Safety is still guaranteed (for the updated version): the arguments for 1(a), 1(b), and 1(c) are independent of how a node picks a value to propose.

What is not guaranteed is liveness, because we now do not have much control over the order of the remaining requests.

Unfortunatly, the "propose by order" fix by Professor Panda is not enough to ensure liveness.

"Propose by order" fix: a node cannot propose a value that is smaller than any committed or on-going value.

A counterexample: There are two nodes A and B. The pipeline number is 2. We call each pipeline thread (process, goroutine, something like that) a worker, then each node has worker 1 and worker 2. We use (P, i) to denote the worker i of node P.

A receives a client request p and B receives a client request q.

Consensus round 1 (seq 1): (A, 1) proposes p and (B, 1) proposes q. Then (A, 2) proposes q. (B, 2) cannot propose p because it is smaller than q. So (B, 2) is blocked. Consensus round 1 failed, they commit ⊥. At this time, either (B, 1) or (B, 2) proposes p because it is released from the "on-going" status and is the smallest value now. Without loss of generality, let's say (B, 1) proposes p. Consensus round 2 (seq 2): (A, 2) proposes q and (B, 1) proposes p. Consensus round 3 (seq 3) also starts immediately: (B, 2) proposes q. Right now, (A, 1) cannot propose p and is blocked. Consensus round 2 failed, they commit ⊥. And so on.