<blockquote>
  <p>Why can we assume that property CP held when acceptor a0 voted for v in round k? It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?</p>
</blockquote>

<p>You're looking at an instance of <em><a href="http://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction">strong induction</a></em>. In simple induction you assume the property holds for $n=m$ and prove it holds for $n=m+1$. In strong induction you assume the property holds for $\forall n: n&lt;m$ and prove it holds for $n=m+1$.</p>

<p><strong>Basis</strong> (I believe): $j = 0$. That is, the null round (since rounds start at 1). This is trivially true, which is probably why it was not stated explicitly.</p>

<p><strong>Inductive step</strong>: Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j &lt; i$.</p>

<p>Believe it or not, this is only a <em>proof sketch</em>. The real proof is in the <em>Part Time Parliament</em> paper. (Some consider the paper cryptic, others consider it humorous.)</p>

<hr>

<blockquote>
  <p>How is this obtained?</p>
  
  <p>In my opinion, the correctness proof of the case $j&lt;k$ relies (recursively) on those of cases of $k&lt;j&lt;i$ and $j=k$.</p>
  
  <p>Therefore, how can we conclude the case $j&lt;k$ without first proving $j=k$ completely (namely, missing the subcase of $j=k$ where $V$ contains more than one value)? </p>
</blockquote>

<p>This is again strong induction, so the case $j&lt;k$ does rely on the cases of $k&lt;j$ and $j=k$, but <em>through the induction hypothesis</em>, namely from the previous Paxos round.</p>

<hr>

<p>General tips for Lamport's proofs.</p>

<p>Lamport uses a technique of hierarchical proofs. For example, the structure of the proof on pages 7-8 looks somewhat like this:</p>

<ul>
<li>Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j &lt; i$.
<ol>
<li>Observation 1</li>
<li>Observation 2</li>
<li>Observation 3</li>
<li>$k = argmax (...)$</li>
<li>case k = 0</li>
<li>case k > 0
<ul>
<li>case k &lt; j</li>
<li>case k = j</li>
<li>case j &lt; k</li>
</ul></li>
</ol></li>
</ul>

<p>Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm <em>maps onto</em> (or <em>"extends"</em>) the simpler algorithm. This doesn't seem to be happening on page 18, but it is something to look out for. (The proof on page 18 appears to be a <em>modification</em> of the proof a pages 7-8; not an <em>extension</em> of it.)</p>

<p>Lamport relies heavily on <a href="http://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction">strong induction</a>; he also tends to think in terms of <em>sets</em> instead of numbers. So you may get empty sets where others would have zeros or nulls; or set unions where others would have addition.</p>

<p>Proving correctness of asynchronous message-passing systems needs an omniscient view of the system with respect to <em>time</em>. For example, when considering actions in round $i$, keep in mind that the actions for some round $j &lt; i$ <em>may not have happened temporally!</em>. And yet Lamport states these potentially future events in past tense.</p>

<p>Lamports systems and proofs tend to have a variable or set of variables that are only allowed to go in one direction; only incrementing numbers and only adding to sets. This is used extensively in his proofs. For example, on page 8 Lamport shows how he neutered the future ability of $a$ to cast another vote:</p>

<blockquote>
  <p>...Since it set $rnd[a]$ to $i$ upon sending a message, $a$ could not subsequently have cast a vote in any round numbered less than $i$....</p>
</blockquote>

<p>It's definitely a brain-stretcher to prove these kinds of systems.</p>

<p><strong>(update)</strong>: List out the invariants; Lamport uses a lot of invariants when developing and his proofs. They are sometimes scattered throughout the proofs; sometimes they are only present in the machine-checked proof. Reason about each invariant; why is it there? How does it interact with the other invariants? How does each step in the system keep this invariant?</p>

<hr>

<p><strong>Full disclosure</strong>: I hadn't read <em>Fast Paxos</em> until I was asked to answer this question; and only looked at the pages cited. I'm an engineer and not a mathematician; my brush with Lamport's work is based purely on the need to correctly invent and maintain large-scale distributed systems.</p>

<p>My answer relies heavily on my experience with Lamport's work. I have read several of Lamport's protocols and proofs; I professionally maintain a paxos-based system; I have written and proven a high-throughput consensus protocol, and again professionally maintain a system based on it (I'm trying to get my company to allow me to publish a paper). I <em>have</em> collaborated on an insignificant paper with Lamport, in which I met with him thrice (the paper is still pending peer review.) </p>

CC BY-SA 3.0
2014-09-26T07:03:05.847Z
Thanks for your time, the answers, and the excellent comments on Lamport's proofs! *For Paxos:* Now, I can catch the basic idea of Lamport's proof. However, the time flow in my mind goes *back*: We are at round $i$ and have $k=max()$. To prove $CP(v,i)$, we examine the cases of $k<j<i$ and $j=k$, and *recursively* prove $CP(v,k)$. Namely, $CP(v,k)$ involves another $k'=max()$, cases of $k'<j'< k$ and $j'=k'$, and $CP(v,k')$. This recursion terminates at $k^{n'}=0$. In this way, the recursion is on $k$s. I have difficulty in translating it into strong induction with time flowing *forward*.
hengxin
CC BY-SA 3.0
2014-09-26T17:19:37.420Z
@hengxin When reasoning about my system/proof; I thought about it as time going forward. I would start out with $i=0$ and make sure all the invariants are met; I would then go with $i=1$ and make sure all the invariants are met; and so on. That reminds me to add some more Lamport pointers.
Michael Deardeuff
CC BY-SA 3.0
2014-09-27T01:40:49.813Z
*For Fast Paxos* ($P_{18}$), is the inductive hypothesis that "$\forall v \in V, CP(v,i)$" (see the $j < k$ case in $P_{18}$)? However, at the bottom of $P_{17}$, it says *We must find a value $v$ in $V$ that satisfies $CP(v,i)$*. So, is that inductive hypothesis too strong?
hengxin
CC BY-SA 3.0
2014-09-28T02:27:15.193Z
Finally, I came to realize what the invariant is and how the strong induction works. Thanks again. BTW, you mentioned that `Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm maps onto (or "extends") the simpler algorithm`, therefore, could you please show an example or cite a related paper? In addition, do your papers have pre-printed, (commercially) unclassified editions?
hengxin
CC BY-SA 3.0
2014-09-29T17:16:36.853Z
Lamport explains the first type of hierarchy in his paper *[How to write a proof](http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf)* and gives an example of the second in *[Byzantizing Paxos by refinement](http://research.microsoft.com/en-us/um/people/lamport/pubs/web-byzpaxos.pdf)*. The second type of hierarchy is typically called a *refinement*, or a *mapping*.
Michael Deardeuff
CC BY-SA 3.0
2014-09-26T04:34:15.293Z
2014-09-26T17:31:36.523Z
2014-09-26T17:31:36.523Z
Michael Deardeuff
<p>I am reading the <a href="http://research.microsoft.com/pubs/64624/tr-2005-112.pdf" rel="noreferrer">"Fast Paxos" paper</a> by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos.</p>

<p>For consistency, the value $v$ picked by the coordinator in phase $2a$ in round $i$ should satisfy</p>

<blockquote>
  <p>$CP(v,i):$ For any round $j &lt; i$, no value other than $v$ has been or might yet be chosen in round $j$.</p>
</blockquote>

<hr>

<p><strong>For classic Paxos</strong>, the proof (Page 8) is split into three cases: $k &lt; j &lt; i$, $j = k$, and $j &lt; k$, where $k$ is largest round number in which some acceptor has reported to the coordinator by phase $1b$ message. I failed to understand the argument for the third case:</p>

<blockquote>
  <p>Case $j &lt; k$. We can <em>assume by induction</em> that property $CP$ held when acceptor $a_0$ voted for $v$ in round $k$. This implies that no value other than $v$ has been or might yet be chosen in round $j$. </p>
</blockquote>

<p>My question is:</p>

<blockquote>
  <ol>
  <li>Why can we assume that property $CP$ held when acceptor $a_0$ voted for $v$ in round $k$? </li>
  </ol>
  
  <p>It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?</p>
</blockquote>

<hr>

<p><strong>For Fast Paxos</strong>, the same argument (Page 18) goes on. It says,</p>

<blockquote>
  <p>Case $j &lt; k$. For any $v$ in $V$, no value other than $v$ has been or might yet be chosen in round $j$. </p>
</blockquote>

<p>My question is:</p>

<blockquote>
  <ol start="2">
  <li>How is this obtained? <strong>In particular, why is "For any $v$ in $V$" here?</strong></li>
  </ol>
  
  <p>In my opinion, the correctness proof of the case $j &lt; k$ relies (recursively) on those of cases of $k &lt; j &lt; i$ and $j = k$.   </p>
  
  <p>Therefore, how can we conclude the case $j &lt; k$ without first proving $j = k$ completely (namely, missing the subcase of $j = k$ where $V$ contains more than one value)? </p>
</blockquote>

<ds.algorithms><dc.distributed-comp><proofs>
Correctness proofs of classic Paxos and Fast Paxos
hengxin
# Correctness proofs of classic Paxos and Fast Paxos

(Asked by: username_0 on 2014-09-24)

I am reading the ["Fast Paxos" paper](http://research.microsoft.com/pubs/64624/tr-2005-112.pdf) by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos.

For consistency, the value $v$ picked by the coordinator in phase $2a$ in round $i$ should satisfy

> $CP(v,i):$ For any round $j < i$, no value other than $v$ has been or might yet be chosen in round $j$.

---

**For classic Paxos**, the proof (Page 8) is split into three cases: $k < j < i$, $j = k$, and $j < k$, where $k$ is largest round number in which some acceptor has reported to the coordinator by phase $1b$ message. I failed to understand the argument for the third case:

> Case $j < k$. We can *assume by induction* that property $CP$ held when acceptor $a\_0$ voted for $v$ in round $k$. This implies that no value other than $v$ has been or might yet be chosen in round $j$.

My question is:

> 1. Why can we assume that property $CP$ held when acceptor $a\_0$ voted for $v$ in round $k$?
>
> It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?

---

**For Fast Paxos**, the same argument (Page 18) goes on. It says,

> Case $j < k$. For any $v$ in $V$, no value other than $v$ has been or might yet be chosen in round $j$.

My question is:

> 2. How is this obtained? **In particular, why is "For any $v$ in $V$" here?**
>
> In my opinion, the correctness proof of the case $j < k$ relies (recursively) on those of cases of $k < j < i$ and $j = k$.
>
> Therefore, how can we conclude the case $j < k$ without first proving $j = k$ completely (namely, missing the subcase of $j = k$ where $V$ contains more than one value)?

**Tags:** ds.algorithms, dc.distributed-comp, proofs


---

## 1 answers

### Answer by username_1 on 2014-09-26. Score: 10 | Accepted answer

> Why can we assume that property CP held when acceptor a0 voted for v in round k? It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?

You're looking at an instance of *[strong induction](http://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction)*. In simple induction you assume the property holds for $n=m$ and prove it holds for $n=m+1$. In strong induction you assume the property holds for $\forall n: n

**Basis** (I believe): $j = 0$. That is, the null round (since rounds start at 1). This is trivially true, which is probably why it was not stated explicitly.

**Inductive step**: Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j < i$.

Believe it or not, this is only a *proof sketch*. The real proof is in the *Part Time Parliament* paper. (Some consider the paper cryptic, others consider it humorous.)

---

> How is this obtained?
>
> In my opinion, the correctness proof of the case $j
>
> Therefore, how can we conclude the case $j

This is again strong induction, so the case $jthrough the induction hypothesis, namely from the previous Paxos round.

---

General tips for Lamport's proofs.

Lamport uses a technique of hierarchical proofs. For example, the structure of the proof on pages 7-8 looks somewhat like this:

* Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j < i$.
  1. Observation 1
  2. Observation 2
  3. Observation 3
  4. $k = argmax (...)$
  5. case k = 0
  6. case k > 0
     + case k < j
     + case k = j
     + case j < k

Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm *maps onto* (or *"extends"*) the simpler algorithm. This doesn't seem to be happening on page 18, but it is something to look out for. (The proof on page 18 appears to be a *modification* of the proof a pages 7-8; not an *extension* of it.)

Lamport relies heavily on [strong induction](http://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction); he also tends to think in terms of *sets* instead of numbers. So you may get empty sets where others would have zeros or nulls; or set unions where others would have addition.

Proving correctness of asynchronous message-passing systems needs an omniscient view of the system with respect to *time*. For example, when considering actions in round $i$, keep in mind that the actions for some round $j < i$ *may not have happened temporally!*. And yet Lamport states these potentially future events in past tense.

Lamports systems and proofs tend to have a variable or set of variables that are only allowed to go in one direction; only incrementing numbers and only adding to sets. This is used extensively in his proofs. For example, on page 8 Lamport shows how he neutered the future ability of $a$ to cast another vote:

> ...Since it set $rnd[a]$ to $i$ upon sending a message, $a$ could not subsequently have cast a vote in any round numbered less than $i$....

It's definitely a brain-stretcher to prove these kinds of systems.

**(update)**: List out the invariants; Lamport uses a lot of invariants when developing and his proofs. They are sometimes scattered throughout the proofs; sometimes they are only present in the machine-checked proof. Reason about each invariant; why is it there? How does it interact with the other invariants? How does each step in the system keep this invariant?

---

**Full disclosure**: I hadn't read *Fast Paxos* until I was asked to answer this question; and only looked at the pages cited. I'm an engineer and not a mathematician; my brush with Lamport's work is based purely on the need to correctly invent and maintain large-scale distributed systems.

My answer relies heavily on my experience with Lamport's work. I have read several of Lamport's protocols and proofs; I professionally maintain a paxos-based system; I have written and proven a high-throughput consensus protocol, and again professionally maintain a system based on it (I'm trying to get my company to allow me to publish a paper). I *have* collaborated on an insignificant paper with Lamport, in which I met with him thrice (the paper is still pending peer review.)

> **Comments:**
> **username_0**: Thanks for your time, the answers, and the excellent comments on Lamport's proofs! *For Paxos:* Now, I can catch the basic idea of Lamport's proof. However, the time flow in my mind goes *back*: We are at round $i$ and have $k=max()$. To prove $CP(v,i)$, we examine the cases of $k<j<i$ and $j=k$, and *recursively* prove $CP(v,k)$. Namely, $CP(v,k)$ involves another $k'=max()$, cases of $k'<j'< k$ and $j'=k'$, and $CP(v,k')$. This recursion terminates at $k^{n'}=0$. In this way, the recursion is on $k$s. I have difficulty in translating it into strong induction with time flowing *forward*.  
> **username_1**: @username_0 When reasoning about my system/proof; I thought about it as time going forward. I would start out with $i=0$ and make sure all the invariants are met; I would then go with $i=1$ and make sure all the invariants are met; and so on. That reminds me to add some more Lamport pointers.  
> **username_0**: *For Fast Paxos* ($P_{18}$), is the inductive hypothesis that "$\forall v \in V, CP(v,i)$" (see the $j < k$ case in $P_{18}$)? However, at the bottom of $P_{17}$, it says *We must find a value $v$ in $V$ that satisfies $CP(v,i)$*. So, is that inductive hypothesis too strong?  
> **username_0**: Finally, I came to realize what the invariant is and how the strong induction works. Thanks again. BTW, you mentioned that `Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm maps onto (or "extends") the simpler algorithm`, therefore, could you please show an example or cite a related paper? In addition, do your papers have pre-printed, (commercially) unclassified editions?  
> **username_1**: Lamport explains the first type of hierarchy in his paper *[How to write a proof](http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf)* and gives an example of the second in *[Byzantizing Paxos by refinement](http://research.microsoft.com/en-us/um/people/lamport/pubs/web-byzpaxos.pdf)*. The second type of hierarchy is typically called a *refinement*, or a *mapping*.  

---

