Timeline for Correctness proofs of classic Paxos and Fast Paxos
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 29, 2014 at 17:16 | comment | added | Michael Deardeuff | 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. | |
| Sep 28, 2014 at 2:27 | vote | accept | hengxin | ||
| Sep 28, 2014 at 2:27 | comment | added | hengxin |
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?
|
|
| Sep 27, 2014 at 1:40 | comment | added | hengxin | 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? | |
| Sep 26, 2014 at 17:31 | history | edited | Michael Deardeuff | CC BY-SA 3.0 |
invariants
|
| Sep 26, 2014 at 17:19 | comment | added | Michael Deardeuff | @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. | |
| Sep 26, 2014 at 7:03 | comment | added | hengxin | 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. | |
| Sep 26, 2014 at 4:44 | history | edited | Michael Deardeuff | CC BY-SA 3.0 |
expanded disclosure
|
| Sep 26, 2014 at 4:37 | review | First posts | |||
| Sep 26, 2014 at 8:09 | |||||
| Sep 26, 2014 at 4:34 | history | answered | Michael Deardeuff | CC BY-SA 3.0 |