13
$\begingroup$

I am reading the "Fast Paxos" paper 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:

  1. 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)?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

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. 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<m$ and prove it holds for $n=m+1$.

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<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)?

This is again strong induction, so the case $j<k$ does rely on the cases of $k<j$ and $j=k$, but through 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; 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.)

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – hengxin
    Commented Sep 26, 2014 at 7:03
  • 1
    $\begingroup$ @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. $\endgroup$
    – Michael Deardeuff
    Commented Sep 26, 2014 at 17:19
  • $\begingroup$ 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? $\endgroup$
    – hengxin
    Commented Sep 27, 2014 at 1:40
  • $\begingroup$ 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? $\endgroup$
    – hengxin
    Commented Sep 28, 2014 at 2:27
  • 1
    $\begingroup$ Lamport explains the first type of hierarchy in his paper How to write a proof and gives an example of the second in Byzantizing Paxos by refinement. The second type of hierarchy is typically called a refinement, or a mapping. $\endgroup$
    – Michael Deardeuff
    Commented Sep 29, 2014 at 17:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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