Paxos作用
功能: 在多个节点协同工作的场景下，一致性地决定一个变量的值
理解的重点
在每一个中间条件被推导出来的时候，都必须思考一下，Paxos如何保持节点之间的一致性。是预设条件还是条件中已经包含了一致性。
Paxos模型
下面使用论文中的模型叙述推导过程(省去listener以简化模型)，其中:
- 实体
- Value(决议): 变量的值，下面会用v代称
- Proposal(议案): 包含决议和一个唯一的id，下面会用p{n, v}代称
- proposer(提案人): 提出议案的节点
- accepter(接受人): 决定议案是否被接受的节点
- 动作
- prepare request: 由proposer发起
- response(回应): accepter对proposer的prepare request的回应
- choose(选择) / accept(确认): accepter对proposer的accept request的回应。
Paxos的推导
那么现在就需要从必要条件，推导出可实行的充分条件。在满足这些充分条件的情况下，就能得出变量的值一致这个断言。
模型等价必要条件: 多数派accepter选择了同一个决议
那么可以先推导出充分条件的一部分:
P1: 每个accepter必须接受他第一个收到的决议
其中P1可以充分保证，即使仅仅一个Proposer提出了一个决议，这个决议也会被选择。假如没有P1，那么accepter完全可以等待永远不会到来的下一个决议，那么最终可能出现无休止等待的结果。P1保证了accepter最终将选择一个决议。
但是P1仍然不能充分保证，多数派accepter选择同一个决议。比如一共三个accepter，都各自选择了不同的决议的情况。所以我们需要完善P1，引出P2去充分保证，多数派accepter选择同一个决议。
P2: 如果一个决议v被多数派选择，那么编号更高且被选择的决议，必须包含v
首先描述一下新的模型: proposer可以提出议案，accepter可以批准多个议案，每个议案包含一个决议和唯一编号。那么我们现在想要推导的条件变成了，多数派accepter选择了同一个提案。这个新条件蕴含前一个模型的条件（多数派accepter选择了同一个决议）。
下面详细推理一下P2是如何解决多数派这个问题的。因为大多数中文论坛上并没有详细描述，所以我用榆木脑子脑补了一天，得到了P2的完整详细描述:
- 多数派选择提案，并不意味着多数派的accepter全部已经选择了提盘p{n,v}，而是多数派中所有accepter，或者选择了提案p{n,v}，或者还没有选择任何提案
- 如果一个决议v被任意多数派选择，这意味着只要存在足够的 选择了决议v的accepter 和 没有选择任何决议的accepter，这两者的数量和超过半数。那么这两个集合就可以组合成一个选择了决议v的多数派
- 编号更高且被选择的提案包含v，这意味着所有accepter在2条件达成以后，所能选择的决议一定是v。这样2条件中的多数派中，没有选择任何提案的accepter，最后选择的决议也一定是v，防止了翻转。
- 最重要的就是保证多数派的弱一致性，无论通信、计算是否异步，请求到达顺序、中间过程如何，多数派都会达到最终一致的状态，选择了同一个提案。最终使用了二阶段执行，来保证多数派的弱一致性。
为了保证多数派一致性，P2并不类似与P1，要求单节点选择第一个收到的提案。所以P2也蕴含了一个风险，因为不断到来的新提案，永远无法到达最终一致的状态。
P2A. 如果一个议案{n, v}被选择，那么任何acceptor批准的议案（编号更高）包含的决议都是v。
相比P2，P2A的要求更加具体，容易实现。同时P2A包含P2。
P2B. 如果一个议案{n, v}被选择，那么此后，任何proposer提出的议案（编号更高）包含的决议都是v。
通过限制“提出议案”的行为，可以间接限制“批准议案”的行为。P2B与P2A基本等效，不过P2B相比起来有更高的容错性，它有效阻止了部分Acceptor因为宕机等原因产生的错误的批准行为。
P2C. 对于任意的v和n，如果议案{n, v}被提出，那么存在一个由acceptor的多数派组成的集合S，或者a) S中没有acceptor批准过编号小于n的议案，或者b) 在S的任何acceptor批准的所有议案（编号小于n）中，v是编号最大的议案的决议。
P2C(a)意味着存在一个多数派没有选择过议案，P2C(b)意味着存在一个多数派已经选择了议案(n{m, v})，只有这两种情况下能够提出议案。这意味着如果一个议案已经被多数派选择，那么accepter只能批准相同提议(v)的序号更高的议案，也就是P2A。多以P2C包含P2B包含P2A。
P2C相比P2B，其实是增加了没有议案被多数派选择前的行为指导。更加具体更易实现。同时P2C已经解决了多数派弱一致的具体实现的问题，就是由Proposer去寻找并判定多数派的最终一致结果，并维护这个结果。因此即使多数派仍然处于不一致状态(部分节点未批准决议v)，但因为新的议案必定包含v，所以这些不一致节点最终也会达到一致状态。
但是P2C距离真正的弱一致性还缺一个锁，因为查询最终一致结果和提出符合最终一致结果的议案之间，可能会产生查询结果变更。因为空节点（未批准任何提案的节点）可以属于任何一个多数派，如果它在两阶段中间批准了旧的提案，并且这一行为导致了原先多数派消失(因为失去空节点，所以数量不足)，那么第二阶段的提案就会导致最终一致性的混乱。
因此在两阶段之间的锁是有必要的，通过改进P1来实现这个锁:
P1A. acceptor可以批准一个编号为n的议案，当且仅当它没有回应过一个编号大于n的prepare请求。
P1A就像是一个前向锁，锁住了旧提案的批准请求，但是又防止了死锁的风险，因为它允许被新提案所覆盖。
具体实现
经过一番条件推导，具体实现已经很简单了，可以细化到各节点的行为:
Accepter
- 如果接收到的prepare请求的编号n大于它已经回应的任何prepare请求，它就回应已经批准的编号最高的议案（如果有的话），并承诺不再回应任何编号小于n的议案
- 如果收到了议案{n, v}的accept请求，它就批准该议案，除非它已经回应了一个编号大于n的议案。
Proposer
- Proposer选择一个议案编号n，向acceptor的多数派发送编号也为n的prepare请求。
- 如果收到了多数acceptor对prepare请求（编号为n）的回应，它就向这些acceptor发送议案{n, v}的accept请求，其中v是所有回应中编号最高的议案的决议，或者是proposer选择的值，如果回应说还没有议案。
伪代码
func accepter(request) {
static atomic accepted = 0 // 批准的提案号
static atomic responsed = 0 // 回应的提案号
if (request.type == PREPARE and
request.seq > responsed) { // 如果接收到的prepare请求编号大于已回应编号
responsed = request.req
response(request.src, accepted) // 回应已经批准的提案
}
if (request.type == ACCEPT and
accepted <= request.seq) { // 如果收到的accept请求编号不小于已批准提案
accepted = request.seq
accept(request) // 批准提案
}
}
func proposer(stage=INIT) {
static atomic seq = 0
switch (stage):
case INIT: // Init阶段
// proposer需要知道集群目前最大的n，才能提出更新的议案
request(SEQ,
callback = lambda ret: set_seq(ret)
)
break
case PREAPRE: // Prepare阶段
request_multi(PREPARE,
seq = seq,
callback = lambda ret: quorum_max(ret)
)
break
case ACCEPT: // Accept阶段
request_multi(
seq = seq
)
break
}
