对论文中的 P2b 证明过程感到困惑 Paxos made simple
Confusing about P2b proving process in paper Paxos made simple
我正在阅读论文 Paxos made simple 但卡在了 P2b.
的证明部分
规则P2的内容b:
If a proposal with value v is chosen, then every higher-numbered proposal issued by any proposer has value v.
这是 Leslie Lamport 的证明部分：
To discover how to satisfy P2b, let’s consider how we would prove that it holds. We would assume that some proposal with number m and value v is chosen and show that any proposal issued with number n > m also has value v. We would make the proof easier by using induction on n, so we can prove that proposal number n has value v under the additional assumption that every proposal issued with a number in m . . (n − 1) has value v , where i . . j denotes the set of numbers from i through j . For the proposal numbered m to be chosen, there must be some set C consisting of a majority of acceptors such that every acceptor in C accepted it. Combining this with the induction assumption, the hypothesis that m is chosen implies:
Every acceptor in C has accepted a proposal with number in m ..(n − 1), and every proposal with number in m ..(n − 1) accepted by any acceptor has value v
所以归纳过程是：
- 基本情况：已选择值为 v 的提案 m
- 归纳步骤：任何数量为 m ..(n-1) 的提议都具有价值 v
为什么暗示：
Every acceptor in C has accepted a proposal with number in m ..(n − 1)
我只是无法弥补差距，为什么每个接受者在C中需要接受编号在[=中的提案32=]m..(n-1)?
P1保证acceptor必须接受收到的第一个提议，P2a 保证只有具有所选值的编号较高的提案才能被接受者接受，但我只是不明白隐含声明的要点。
鉴于该论文中的语言，很容易被细节所困扰。我建议改用 Understanding Paxos。它要详细得多，但它在没有设置符号或上标的情况下介绍了算法的实际使用方法和原因以及周围问题。
这是整个正确性证明的图片说明。
- 假设已经为编号为 P 和 Q 的两个提案学习了值，其中 P < Q:
- 再假设P的学习值为X，Q的学习值为Y，其中X≠Y：
- 这意味着 P 和 Q 的建议值分别为 X 和 Y。每个提案最多只能有一个值：
- 现在考虑 P 和 Q 之间提出的所有其他建议：
- 设R为第一个值为≠X的提案。希望清楚 P < R ≤ Q:
- 换句话说，编号≥ P 和 < R 的提案都具有值 X:
- 设 S 为在 P 处发送阶段 2b 消息的节点集。（在你的问题中 S 称为 C，但我已经绘制了这些图片，所以我坚持使用 S）。由于多数重叠，这组节点必须与在 R:
发送阶段 1b 消息的节点组重叠
- 考虑重叠的节点之一。它必须先在 P 发送其阶段 2b 消息，然后 在 R 发送其阶段 1b 消息，因为这就是阶段 1b 消息的用途。
- 它可能也为编号为 >P 的提案发送了阶段 2b 消息，但不能为编号为 ≥R 的提案发送了消息，因为这是阶段 1b 消息的规则。但是所有 ≥ P 且 < R 的提案都具有值 X，因此它发送阶段 2b 消息的编号最高的提案肯定具有值 X:
- 现在考虑为提案 R 发送阶段 1b 消息的所有其他节点。其中一些可能没有接受之前的提案；有些人可能已经接受了编号 < P 的提案，但他们都接受了编号 < R 的提案，并且其中至少有一个接受了一个提案 ≥ P，因此他们中的任何一个接受的编号最高的提案的值为 X:
矛盾就在这里：根据阶段2a消息的规则，这意味着在R提出的值毕竟必须是X。
在您看来，这可能是与 Paxos Made Simple 论文中的证明截然不同的证明，因为它似乎是靠矛盾工作的，并且其中没有明确的归纳法。事实上，第 5 步中的技术 "suppose there is a counterexample and then consider the smallest such" 实际上只是伪装的归纳法，根据我的经验，这是一种更易于理解的呈现方式。将那一步变成明确的归纳是一个有趣的练习，如果你喜欢那种东西的话。
你问题中提到的集合C是发送phase 2b消息接受P处提案的acceptor集合。这不一定与在R发送phase 1b消息的那些集合相同，但是这些集合确实相交，这是重要的因素。
C中的每个acceptor都接受了一个编号为m ..(n − 1)的提案
因为已经选择了值为 v 的提议 m，所以必须存在一些由大多数接受者组成的集合 C，使得 C 中的每个接受者都接受它，并且 m ..(n − 1) 包含 m
我正在阅读论文 Paxos made simple 但卡在了 P2b.
的证明部分规则P2的内容b:
If a proposal with value v is chosen, then every higher-numbered proposal issued by any proposer has value v.
这是 Leslie Lamport 的证明部分：
To discover how to satisfy P2b, let’s consider how we would prove that it holds. We would assume that some proposal with number m and value v is chosen and show that any proposal issued with number n > m also has value v. We would make the proof easier by using induction on n, so we can prove that proposal number n has value v under the additional assumption that every proposal issued with a number in m . . (n − 1) has value v , where i . . j denotes the set of numbers from i through j . For the proposal numbered m to be chosen, there must be some set C consisting of a majority of acceptors such that every acceptor in C accepted it. Combining this with the induction assumption, the hypothesis that m is chosen implies:
Every acceptor in C has accepted a proposal with number in m ..(n − 1), and every proposal with number in m ..(n − 1) accepted by any acceptor has value v
所以归纳过程是：
- 基本情况：已选择值为 v 的提案 m
- 归纳步骤：任何数量为 m ..(n-1) 的提议都具有价值 v
为什么暗示：
Every acceptor in C has accepted a proposal with number in m ..(n − 1)
我只是无法弥补差距，为什么每个接受者在C中需要接受编号在[=中的提案32=]m..(n-1)?
P1保证acceptor必须接受收到的第一个提议，P2a 保证只有具有所选值的编号较高的提案才能被接受者接受，但我只是不明白隐含声明的要点。
鉴于该论文中的语言，很容易被细节所困扰。我建议改用 Understanding Paxos。它要详细得多，但它在没有设置符号或上标的情况下介绍了算法的实际使用方法和原因以及周围问题。
这是整个正确性证明的图片说明。
- 假设已经为编号为 P 和 Q 的两个提案学习了值，其中 P < Q:
- 再假设P的学习值为X，Q的学习值为Y，其中X≠Y：
- 这意味着 P 和 Q 的建议值分别为 X 和 Y。每个提案最多只能有一个值：
- 现在考虑 P 和 Q 之间提出的所有其他建议：
- 设R为第一个值为≠X的提案。希望清楚 P < R ≤ Q:
- 换句话说，编号≥ P 和 < R 的提案都具有值 X:
- 设 S 为在 P 处发送阶段 2b 消息的节点集。（在你的问题中 S 称为 C，但我已经绘制了这些图片，所以我坚持使用 S）。由于多数重叠，这组节点必须与在 R: 发送阶段 1b 消息的节点组重叠
- 考虑重叠的节点之一。它必须先在 P 发送其阶段 2b 消息，然后 在 R 发送其阶段 1b 消息，因为这就是阶段 1b 消息的用途。
- 它可能也为编号为 >P 的提案发送了阶段 2b 消息，但不能为编号为 ≥R 的提案发送了消息，因为这是阶段 1b 消息的规则。但是所有 ≥ P 且 < R 的提案都具有值 X，因此它发送阶段 2b 消息的编号最高的提案肯定具有值 X:
- 现在考虑为提案 R 发送阶段 1b 消息的所有其他节点。其中一些可能没有接受之前的提案；有些人可能已经接受了编号 < P 的提案，但他们都接受了编号 < R 的提案，并且其中至少有一个接受了一个提案 ≥ P，因此他们中的任何一个接受的编号最高的提案的值为 X:
矛盾就在这里：根据阶段2a消息的规则，这意味着在R提出的值毕竟必须是X。
在您看来，这可能是与 Paxos Made Simple 论文中的证明截然不同的证明，因为它似乎是靠矛盾工作的，并且其中没有明确的归纳法。事实上，第 5 步中的技术 "suppose there is a counterexample and then consider the smallest such" 实际上只是伪装的归纳法，根据我的经验，这是一种更易于理解的呈现方式。将那一步变成明确的归纳是一个有趣的练习，如果你喜欢那种东西的话。
你问题中提到的集合C是发送phase 2b消息接受P处提案的acceptor集合。这不一定与在R发送phase 1b消息的那些集合相同，但是这些集合确实相交，这是重要的因素。
C中的每个acceptor都接受了一个编号为m ..(n − 1)的提案 因为已经选择了值为 v 的提议 m，所以必须存在一些由大多数接受者组成的集合 C，使得 C 中的每个接受者都接受它，并且 m ..(n − 1) 包含 m