2
$\begingroup$

I am reading Leslie Lamport's Paxos Made Simple paper.

Can someone explain why $P2^c$ implies $P2^b$?

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

$P2^c$ For any $v$ and $n$, if a proposal with value $v$ and number $n$ is issued, then there is a set $S$ consisting of a majority of acceptors such that either

  1. no acceptor in $S$ has accepted any proposal numbered less than $n$, or
  2. $v$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$.
$\endgroup$
2
$\begingroup$

We prove it ($P2^c \implies P2^b$) by strong induction (wiki). This proof has actually been given in the "Paxos Made Simple" paper (see the arguments between $P2^b$ and $P2^c$). I re-organize it in the order of "what we know, what we want to prove, and how to prove". Hope it helps.


What we know:

Base case: Some proposal with number $m$ and value $v$ is chosen.

Inductive assumption: Every proposal issued with a number in $m \ldots (n-1)$ has value $v$.

The chosen rule of a proposal: For the proposal number $m$ to be chosen, there must be some set $C$ consisting of a majority of acceptors such that every acceptor in $C$ accepted it.

The issue rule of a proposal: It is the existence of a set $S$ such that $P2^c (1)$ + $P2^c (2)$.

What we want to prove is:

Goal: Any proposal issued with number $n > m$ also have value $v$.


Proof:

Combining "base case" and "chosen-rule" with "inductive assumption", we obtain:
The $C$-condition: Every acceptor in $C$ has accepted a proposal with number in $m \ldots (n-1)$ (Note: because at least each of them has accepted a proposal with number $m$),
and every proposal with number in $m \ldots (n-1)$ accepted by any acceptor has value $v$ (Note: due to the inductive assumption and the fact that a proposal must be issued by a proposer before it can be accepted by an acceptor).

Now consider the set $S$ in $P2^c$ which consists of a majority of acceptors. Because $S \cap C \neq \emptyset$, $P2^c(1)$ cannot happen. Then $P2^c(2)$ must be true. $P2^c(2)$ is actually the "value-issued rule": the value $v'$ of the proposal with number $n$ is the value of the highest-numbered proposal among all proposals numbered less than $n$ accepted by the acceptors in $S$, therefore $v' = v$ because of the $C$-condition.


Related posts:

$\endgroup$

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.