在纸张Paxos中混淆P2b证明过程变得简单

Question

我正在阅读Paxos简单的文章，但却被困在P2b的证明部分。

规则P2b的内容：

如果选择了具有值v的提议，则由任何提议者发布的每个更高编号的提议具有值v。

这是Leslie Lamport的证明部分：

为了发现如何满足P2b，让我们考虑如何证明它是成立的。我们假设选择了一些数字为m和值为v的提案，并表明任何以数字n> m发出的提案也具有值v。我们可以通过在n上使用归纳来使证明更容易，因此我们可以证明提议编号为n具有v值的额外假设是每个提案都以m为单位发出。 。 （n - 1）具有值v，其中i。 。 j表示从i到j的数字集。对于选择编号为m的提议，必须有一些由大多数接受者组成的集合C，使得C中的每个接受者都接受它。将此与归纳假设相结合，选择m的假设意味着：

C中的每个接受者都接受了一个数字为m ...（n - 1）的提案，并且任何接受者接受的数字为m ...（n - 1）的提案都具有价值v

所以归纳过程是：

• 基本情况：已选择具有值v的提议m
• 归纳步骤：数量为​​m ...（n-1）的任何提议都具有值v

为什么它意味着：

C中的每个接受者都接受了一个数字为m的提案。（n - 1）

我只是无法缩小差距，为什么C中的每个接受者都需要接受一个数字为m ...（n-1）的提案？

P1保证接受者必须接受收到的第一个提议，P2a保证只有具有所选值的更高编号的提议可以被接受者接受，但我只是没有得到隐含声明的要点。

Answer 1

这是整个正确性证明的图解说明。

1. 假设已经为两个提案学习了数值，编号为P和Q，其中P <Q：

2. 此外，假设矛盾的是，为P学习的值是X，并且为Q学习的值是Y，其中X≠Y：

3. 这意味着为P和Q建议的值分别为X和Y.每个提案最多只能有一个值：

4. 现在考虑P和Q之间提出的所有其他提议：

5. 设R是第一个值为≠X的提案。希望很清楚P <R≤Q：

6. 换句话说，编号≥P且<R的提议都具有值X：

7. 设S是在P处发送阶段2b消息的节点集（在你的问题中S被称为C，但我已经绘制了这些图片，所以我坚持使用S）。由于多数重叠，这组节点必须与在R处发送阶段1b消息的节点集重叠：

8. 考虑重叠中的一个节点。它必须在P处发送其阶段2b消息，然后在R处发送其阶段1b消息，因为这是1b阶段消息的用途。

9. 它可能已经为编号> P的提议发送了阶段2b消息，但是不能为编号≥R的提议发送一个消息，因为这是1b阶段消息的规则。但是所有≥P和<R的提案都有X值，因此它发送阶段2b消息的最高编号提案肯定具有值X：

10. 现在考虑为提案R发送1b阶段消息的所有其他节点。其中一些节点可能已经接受了之前的提议;有些人可能接受了编号为<P的提案，但他们都接受了编号为<R的提案，并且其中至少有一个提案接受了提案≥P，因此其中任何一个提出的编号最高的提案都有X值：

这里存在矛盾：根据阶段2a消息的规则，这意味着在R处提出的值毕竟必须是X.

这可能看起来像是与Paxos Made Simple论文中的证据截然不同，因为它似乎是矛盾的，并且没有明确的归纳。实际上，这种技术“假设有一个反例，然后在第5步中考虑最小的这种”实际上只是伪装的归纳，而我的经验是，这是一种更容易呈现的方式。如果你喜欢那种东西，将这一步变成明确的归纳是一项有趣的练习。

您问题中提到的集合C是发送阶段2b消息以接受P处的提议的接收器集合。这不一定与在R处发送阶段1b消息的集合相同，但这些集合确实相交，即重要因素。

Answer 2

根据该论文中的语言，很容易挂起细节。我建议改用Understanding Paxos。它更冗长，但是它可以在没有设置符号或上标的情况下遍历方法和原因以及周围问题以实际使用算法。

Answer 3

C中的每个接受者都接受了一个数字为m的提议。（n - 1）因为已经选择了具有值v的提议m，所以必须有一些C由大多数接受者组成，这样C中的每个接受者都接受它，和m ..（n - 1）包含m