Confusing about P2b proving process in paper Paxos made simple

Question

I'm reading the paper Paxos made simple but got stuck on the proving part for P2^b.

Content of rule P2^b:

If a proposal with value v is chosen, then every higher-numbered proposal issued by any proposer has value v.

And this is the proving part by Leslie Lamport:

To discover how to satisfy P2^b, let’s consider how we would prove that it holds. We would assume that some proposal with number m and value v is chosen and show that any proposal issued with number n > m also has value v. We would make the proof easier by using induction on n, so we can prove that proposal number n has value v under the additional assumption that every proposal issued with a number in m . . (n − 1) has value v , where i . . j denotes the set of numbers from i through j . For the proposal numbered m to be chosen, there must be some set C consisting of a majority of acceptors such that every acceptor in C accepted it. Combining this with the induction assumption, the hypothesis that m is chosen implies:

Every acceptor in C has accepted a proposal with number in m ..(n − 1), and every proposal with number in m ..(n − 1) accepted by any acceptor has value v

So the induction process is:

• Base case: proposal m with value v has been chosen
• Inductive step: any proposal in number m ..(n-1) have value v

Why it implies that:

Every acceptor in C has accepted a proposal with number in m ..(n − 1)

I just can't bridge the gap, why does every acceptor in C need to accepted a proposal with number in m..(n-1)?

P1 guarantees that acceptor must accept the first proposal received, P2^a guarantees that only the higher-numbered proposals with the chosen value could be accepted by acceptors, but I just don't get the point of the implied statement.

Answer 1

Here is a pictorial explanation of the whole correctness proof.

1. Suppose that values have been learned for two proposals, numbered P and Q, where P < Q:

2. Furthermore suppose for a contradiction that the value learned for P was X and the value learned for Q was Y, where X ≠ Y:

3. This means that the values proposed for P and for Q were X and Y respectively. Each proposal can only have at most one value:

4. Now contemplate all the other proposals that were made between P and Q:

5. Let R be the first proposal whose value was ≠X. It is hopefully clear that P < R ≤ Q:

6. In other words, proposals numbered ≥ P and < R all have value X:

7. Let S be the set of nodes that sent phase 2b messages at P. (S is called C in your question, but I already had these pictures drawn so I'm sticking with S). Because majorities overlap, this set of nodes must overlap the set of nodes that sent phase 1b messages at R:

8. Contemplate one of the nodes that was in the overlap. It must have sent its phase 2b message at P before sending its phase 1b message at R, because that's what phase 1b messages are for.

9. It may have sent a phase 2b message for a proposal numbered >P too, but cannot have sent one for a proposal numbered ≥R, because that's the rule for phase 1b messages. But all proposals that are ≥ P and < R have value X, so the highest-numbered proposal for which it had sent a phase 2b message definitely has value X:

10. Now contemplate all the other nodes that sent phase 1b messages for proposal R. Some of them may have accepted no previous proposal; some may have accepted proposals numbered < P, but they all accepted proposals numbered < R and at least one of them accepted a proposal ≥ P, so the highest-numbered proposal accepted by any of them has value X:

Herein lies the contradiction: by the rules for phase 2a messages, this means that the value proposed at R must be X after all.

This may look to you like a substantially different proof from the one in the Paxos Made Simple paper since it seems to work by contradiction and has no explicit induction in it. In fact, the technique "suppose there is a counterexample and then consider the smallest such" in step 5 is really just that induction in disguise, and my experience has been that this is a more accessible way to present it. It's an interesting exercise to turn that step into an explicit induction, if you like that sort of thing.

The set C mentioned in your question is the set of acceptors that sent phase 2b messages to accept the proposal at P. This is not necessarily the same set as the ones that sent phase 1b messages at R, but those sets do intersect and that is the important factor.