2
$\begingroup$

I am reading Paxos Made Simple. I am quite confused about the proof of P2b. It said

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.

How can he add the additional assumption? Is it reasonable? In reality, proposal numbered in m..(n - 1) can have value other than v, isn't it?

I am really confused about that, please help! Thanks

$\endgroup$
1
$\begingroup$

Note: I have had a similar question about the correctness proof of Paxos and Fast Paxos before and posted it here. Wish the excellent answer to it be helpful to you.


A few words about this paper:

Leslie Lamport has his own, very impressive writing style. He is not satisfied with the common pattern of stating a theorem, proving it, moving on to another theorem, and so on. He is good at demonstrating the way how to solve a problem. In his paper, you will see that proof does not follow a theorem; instead, it comes along with a theorem. The paper "Paxos Made Simple" is a typical example of this style.


About your questions:

Your question (1): How can he add the additional assumption? Is it reasonable?

Leslie Lamport is using strong induction. The goal here is to prove

$P2^{b}:$ If a proposal with value $v$ i chosen (say, with number $m$), then every higher-numbered proposal issued by any proposer has value $v$.

We apply strong induction to natural number $\mathbb{N}$. I summarize the proof as follows and explain it later.

  • The base case is "some proposal with number $m$ and value $v$ is chosen".

  • The strong induction hypothesis is "every proposal issued with a number in $m .. (n-1)$ has value $v$".

  • The induction step to prove $P2^{b}$: Combining the premise of "$m$ is chosen (with value $v$)" with the above induction hypothesis, we get (for reference, I call it $C$-condition):

$C$-condition: Every acceptor in $C$ (defined in the paper) 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$.

Now, Lamport introduces $P2^{c}$, which, along with the above $C$-condition, is sufficient for $P2^{b}$.

You can think of this induction process step by step:

  1. The base case $m$ is trivially valid.
  2. Given that step 1 is valid, the argument in "The induction step" above (of course with $P2^{C}$) shows that the proposals numbered $m+1$ has value $v$.
  3. Given both step 1 and step 2 are valid, the same argument shows that the proposals numbered $m + 2$ has value $v$.
  4. And so on.

This also answers your second question.

Your question (2): In reality, proposal numbered in $m..(n - 1)$ can have value other than v, isn't it?

No, it isn't. The Paxos algorithm guarantees that all the proposals with larger numbers than $m$ must have value $v$, given that $m$ is chosen with value $v$.

$\endgroup$
  • $\begingroup$ Now I understand the additional assumption comes from strong induction. But I still have many questions. 1)Why you say the base case P(m) is trivial? Can you make it clear a bit? For me, If P(m) holds, then when proposal m is chosen, a higher-numbered proposal, say m+1, issued by other proposer must also has value v. But I can't figure it out. Unless on your strong induction, proposal m..n-1 has value v, so P(m) is true. But I think we should make strong induction after we have checked the base case P(m) is true. $\endgroup$ – StrikeW Nov 17 '14 at 4:56
  • $\begingroup$ 2) The inference of C-condition is the most confusing. On my view, you showed that the C-condition follows by just replace m with m..(n-1), isn't it? If it is, I can't bridge the gap from m to m..(n-1) on my mind. $\endgroup$ – StrikeW Nov 17 '14 at 5:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.