这些是我在学习了Paxos算法后的笔记。这里的主要目标是加深我自己对该算法的理解，但也许有人会发现这个关于Paxos的解释很有用！这篇文章假设我对数学符号很熟练。
我必须承认，我花了很长时间来理解分布式共识。我读了一大堆论文(在议会兼职期间，Paxos做了简单实用的BFT，寻找一个可以理解的共识算法，CASPaxos：没有日志的复制状态机)，但它们没有意义。或者说，没有什么具体的东西是不清楚的，但同时，我无法回答核心问题：
帕克索斯算法或如何赢得图灵奖讲座(我不敢相信我当时真的在圣彼得堡，错过了这个！)。
我现在认为事情实际上比人们想象的要简单得多：-)。
Paxos是一种实现分布式共识的算法。假设你有N台机器，它们在故障网络上通信。网络可能会延迟、重新排序和松散消息(尽管它不会破坏它们)。一些机器可能会死掉，可能会稍后返回。由于网络延迟，“机器死了”和“机器暂时无法到达”是无法区分的。我们要做的是让机器就某个值达成一致。这里的“同意”是指，如果一台机器说“值是X”，而另一台机器说“值是Y”，那么“机器死了”和“机器暂时无法到达”是无法区分的。我们要做的是让机器就某个值达成一致。这里的“同意”是指，如果一台机器说“值是X”，而另一台说“值是Y”，那么X必需等于Y。机器回答“我还不知道”是可以的。
这个公式的问题是，Paxos是一个基本但微妙的算法。要理解它(至少对我来说)，需要一个精确的数学公式。所以，让我们再试一次。
什么是Paxos？Paxos是一个关于集合的定理！这绝对是数学的，而且是真的(只要你把数学建立在集合论的基础上)，但是没有什么帮助。所以，让我们再试一次。
系统的特征是一种状态。系统以离散的步骤演化：每一步都将系统从一个状态带到另一个状态。转变是不确定的：从一个当前的S1，你可能会到达不同的下一个状态S2和S3。(非决定论为一个松散的网络建模)。无限的系统状态序列被称为一种行为：
由于非决定论，潜在的可能行为的数量是无限的，不朽的，依赖于转移函数，我们也许能够证明，对于任何行为中的任何状态，某些条件都是正确的。
让我们从一个简单的例子开始，并介绍一些符号。我不会使用TLA+，因为我不喜欢它的具体语法。
该示例对整数计数器进行建模。每一步计数器都会递减或递增(非确定性)，但不会变得太大或太小。
集合：ℕ--带零的自然数变量：Counter∈ℕInit≡Counter=0Next≡(Counter<；9∧Counter'；=Counter+1)∨(Counter>；0∧Counter'；=Counter-1)定理：∀I：0≤Counter_I≤9--NOTATION--≡：定义等于--∧："；和"；，CONNECT-∨："；或"；，析取。
系统的状态是一个单变量的 - 计数器，它包含一个自然数，通常我们会用一组固定的变量来表示任何系统的状态，即使系统在逻辑上由几个组件组成，我们也会用一个统一的状态对其进行建模。
初始化公式指定初始状态，计数器为零。请注意=是数学等式，而不是赋值。Init是一个基于状态的谓词。
下一步，定义了一个非确定性转移函数，它是关于状态对S1和S2的谓词。COUNTER是S1状态下的变量，COUNTER#39；是S2状态下的对应变量。简而言之，如果下列条件之一成立，则从S1到S2的转换是有效的：
S1中的COUNTER值小于9，S2中的COUNTER值大于1。
S1中的COUNTER值大于0，S2中的COUNTER值小于1。
NEXT对于({COUNTER：5}，{COUNTER：6})为真。NEXT对于({COUNTER：5}，{COUNTER：5})为FALSE。
0→1→2→3→4→5→6→7→8→9。
%0→%1→%2→%3→%3→%2→%1→%0。
1→2→3→4→5：初始化不适用于初始状态。
0→1→0→-1：Next不适用于(0，-1)对。
“行为”是指初始状态满足Init，然后每个转换都满足。
我们可以陈述并证明关于这个系统的一个定理：对于每个行为中的每个状态，计数器的值都在0到9之间。Proof是通过归纳法得出的：
如果条件对于状态S1为真，并且接下来对于(S1，S2)成立，则条件对于S2为真。
与通常的归纳法一样，有时我们会想要证明一个更强的性质，因为它为归纳法步骤提供了更强大的基础。
总之，我们使用两个谓词Init和Next定义了一个非确定性状态机。Init是限制可能的初始状态的状态谓词。接下来是状态对上的谓词，它定义了一个非确定性的转移函数。Vars部分将状态描述为一组固定的类型化变量。集合定义辅助固定集合，其元素是变量的值。定理部分指定了关于行为的谓词：根据Init和Next演化的步骤序列。
这个定理不会自动从Init和Next得到证明。或者，我们可以在计算机上模拟一系列可能的行为，并针对具体情况检查定理。如果可达状态集足够小(有限将是一个很好的开始)，我们可以枚举所有行为并产生暴力证明。如果可达状态太多，我们不能用这种方式证明定理，但我们通常可以通过找到反例来证明它是错误的。这就是我们的想法。如果可达状态太多，我们就不能用这种方式证明定理，但我们通常可以通过找到反例来证明它是错误的。这就是我们的想法：如果可达状态集足够小(有限将是一个好的开始)，我们可以列举所有行为并产生暴力证明。
掌握了基本词汇后，让我们开始慢慢构建Paxos。我们首先定义共识是什么。因为这是数学，所以我们将使用集合来完成。
集合：𝕍--任意值集合Vars：SELECTED∈2^𝕍--值子集定理：∀i：|SELECTED_I|≤1∧∀i，j：i≤j∧SELECTED_I≠{}⇒CHOSED_I=SELECTED_j--NOTATION--{}：空集--2^X：由X的所有子集组成的集合，幂集--|X|：集合的基数(大小。
系统的状态是一组选定的值。要使这组值构成共识(随着时间的推移)，我们需要两个条件来满足：
如果我们在某个时间点选择一个值，我们会坚持使用它(数学友好：任何两个选择的值都相等)
集合：𝕍--任意值集合Vars：SELECTED∈2^VARS--值子集Init≡SELECTED={}Next≡SELECTED={}∧∃v∈𝕍：SELECTED'；={v}定理：∀i：|SELECTED_i|≤1∧∀i，j：i≤j∧(SELECTED_I≠{}⇒SELECTED_i=SELECTED_j)。
在初始状态下，选择的值集为空。如果当前选择的值集为空，我们可以执行一个步骤，在这种情况下，我们可以选择任意值。
这在技术上打破了我们的行为理论：我们要求行为是无限的，但对于这个规范，我们只能迈出一步。修复方法是允许空步骤：根本不改变状态的步骤总是有效的。我们称这样的步骤为“卡顿步骤”。
一致性定理第一个条件的证明是一个平凡的归纳，第二部分的证明实际上是非平凡的，这里有一个示意图，假设i和j是违反条件的指标，它们在状态空间中可能相距很远，所以我们不能立即应用下一个条件，所以我们选择最小的J1∈[i+1；使得条件是违反的，设i1=j1-1，(i1，j1)对仍然违反条件，但这一次它们是后续步骤，我们可以证明下一步不适用于它们，从而得出证明。(i1，j1)对(i1，j1)对仍然违反条件，但这次是后续步骤，我们可以证明下一步不适用于它们，从而得出证明。
让我们尝试将其扩展到真正分布式的情况，其中我们有N台机器(“接受者”)，我们从形式化的朴素共识算法开始：让接受者为值投票，并选择获得多数选票的值。
集合：𝕍--任意值集合𝔸--有限接受者集合Vars：Votes∈2^(𝔸×𝕍)--(接受者，值)对的集合Init≡Votes={}Next≡∃a∈𝔸：∃v∈V：Votes'；=Votes∪{(a，v)}∧∀v∈V：(a，v)∉voteselected≡{v∈V：|{a∈𝔸：(a，v)∈Votes}|>；|𝔸|/2}。
系统的状态是所有接受者投出的所有选票的集合。我们将一张选票表示为接受者和它所投的值的一对。最初，这组选票是空的。在每一步上，一些接受者为某个值投下一票(将(a，v)对加到这组选票中)，但前提是它还没有投票。请记住，NEXT是状态对上的谓词，所以我们检查现有选票的选票，但在选票中添加一个新的选票#39；如果投票支持该值的接受者集合({a∈𝔸：(a，v)∈Votes})至少是所有接受者集合的一半，则选择该值。换句话说，如果大多数接受者投票支持该值。
让我们证明多数投票协议的共识定理。类型错误，不竞争。共识定理是关于由选定变量组成的国家行为的谓词。这里，选定不是变量，选票是！SELECTED是一个将当前状态映射到某个布尔值的函数。
虽然直观上很清楚这种情况下的“共识定理”是什么样子，但让我们来精确一下。让我们使用多数规则f将具有投票变量的状态映射到具有所选变量的状态。此映射自然扩展到相应行为(步骤序列)之间的映射：
F(Votes_0→Votes_1→...)=f(Votes_0)→f(Votes_1)→...=SELECTED_0→SELECTED_1→...。
现在我们可以准确地说，对于多数投票规范的每一种行为B，定理对f(B)都成立。这提供了一种更好的证明方法！我们证明了我们的映射f是同态，而不是直接证明定理(这同样需要i1，j1技巧)。也就是说，我们证明了如果Votes_0→Votes_1→…。投票是多数投票规范的行为，然后是f(_0)→f(Votes_1)→…。是一种共识规范的行为，这让我们可以重用现有的证据。
最初的步骤是微不足道的，但让我们把它说清楚，只是为了欣赏人类大脑可以浏览的细节的数量。
F({∈：{}})={Choose：{v∈𝔸V：|{a∈：(a，v)∈{}}|>；|𝔸|/2}}={Choose：{v∈V：|{}|>；|𝔸|/2}}={Choose：{v∈V：0>；|𝔸|/2}}={Choose：{v∈V：False}}={Choose：{}}。
让我们证明，如果多数票的next_m支持(Votes，Votes&39；)，那么共识的next_c支持(f(Votes)，f(Votes&39；))。我们前进的道路上有一个障碍：这个声明是错误的！考虑一个有三个接受者和两个值的情况：𝔸={a1，a2，a3}，𝕍={v1，v2}。考虑一下投票数和投票数的以下值：
投票={(a1，v1)，(a2，v1)，(a1，v2)}投票'；={(a1，v1)，(a2，v1)，(a1，v2)，(a3，v2)}。
如果你只是机械地检查下一步，你会发现它起作用了！A3还没有投票，所以现在可以投票了，问题是SELECTED(VORTS)={v1}和SELECTED(VORTS'；)={V1，V2}。
我们试图证明的太多了！F仅适用于可从Init访问的州，并且无法访问A1投票两次的投票值错误。
因此，我们首先要证明一个引理：每个接受者至多投票一次。然后，我们可以在至多一次投票的假设下证明next_m(Votes，Votes&39；)=next_c(f(Votes)，f(Votes&39；))。具体地说，如果|f(Votes)|大于1，那么我们可以选择投票给不同值的两个多数，这样可以确定一个接受者投了两次票，这是一个矛盾的问题。剩下的就留给读者练习了：)，如果|f(Votes)|大于1，那么我们可以选择两个多数投票给不同的值，这样就可以确定一个接受者投了两次票，这是矛盾的。剩下的就留给读者练习了：)。
因此，多数票确实实现了共识。让我们更仔细地看看“多数”条件。这显然很重要。如果我们将选择定义为。
选择的≡{v∈V：|{a∈𝔸：(a，v)∈Votes}|>；0}。
我们使用的多数属性是任何两个多数都有至少一个共同的接受者，但是任何其他具有此属性的条件也同样适用。例如，我们可以为每个接受者分配一个整数权重，并要求权重之和大于一半。作为一个更具体的例子，考虑一组for接受者{a，b，c，d}。在这个例子中，我们来看一下FOR接受者的集合{a，b，c，d}，例如，我们可以为每个接受者分配一个整数权重，并要求权重之和大于一半。作为一个更具体的例子，考虑一组for接受者{a，b，c，d}。
集合：𝕍--任意值集合𝔸--有限接受者集合ℚ∈2^𝔸--仲裁集合假设：∀Q1，Q1∈ℚ：Q1∩Q2≠{}Vars：Votes∈2^(𝔸×𝕍)--(接受者，值)对集合Init≡Votes={}Next≡∃a∈𝔸：∃v∈V：Votes'；=Votes∪{(a，v)}∧∀v∈V：(a，v)∉Votes Choose≡{v∈V：∃q∈ℚ：AllVoted For(q，v)}AllVoted for(q，v)≡∀a∈q：(a，v)∈Votes。
我们需要指定一组Quorum - Set a，它由接受者的子集组成，这样每两个Quorum至少有一个共同的接受者。如果存在一个Quorum，使得每个成员都投票支持该值，则选择该值。
这里有一件奇怪的事情值得注意。Consensus是整个系统的属性，我们没有一个“地方”可以指着说“嘿，就是它，这就是共识”。想象3个接受者，坐在地球、金星和火星上，在v1和v2值之间进行选择，他们可以执行法定投票算法，而根本不需要相互沟通。他们必须在不知道他们同意的具体值的情况下达成共识！然后，外部观察者可以旅行到这三个行星，收集选票，发现选择的值，但这个功能并不是算法本身的组成部分。
好的，我们刚刚描述了一种在N台机器之间寻找共识的算法，证明了它的共识定理，并注意到它具有惊人的通信效率：零消息。我们应该领取图灵奖吗？
嗯，不，Quorum Vote - 有一个很大的问题，它可能会被卡住。具体地说，如果有三个值，选票在它们之间平均分配，那么就不会选择任何值，只可能出现卡顿的步骤。如果你可以投票给不同的值，可能会出现两个值都得不到多数票的情况。投票满足安全属性，但不满足活性属性 - ，即使所有机器都在线并且通信完美，算法也可能会卡住。
这个问题有一个简单的解决办法，在许多“民主”政府中有着丰富的历史传统。让我们进行投票，让我们选择多数人选择的值，但让我们只允许投票给单一的候选值：
集合：𝕍--任意值集合𝔸--有限接受者集合ℚ∈2^𝔸--仲裁集合假设：∀Q1，Q1∈ℚ：Q1∩Q2≠{}Vars：Votes∈2^(𝔸×𝕍)--(接受者，值)对集合Init≡Votes={}Next≡∃a∈𝔸，v∈V：∀(a1，v1)∈Votes：v1=v∧Votes'；=Votes∪{(a，v)}Selected≡{v∈V：∃q∈ℚ：AllVoted For(q，v)}AllVoted For(q，v)≡∀a∈q：(a，v)∈Votes。
新的条件规定，只有在所有其他票数都相同的情况下，接受者才能投票。作为特例，如果票数为空，接受者可以投票支持任何值(但所有其他接受者随后都必须投票支持该值)。
从数学的角度看，这个算法是完美的。从实用的角度来看，并非如此：接受人投第一票需要以某种方式确保它确实是第一票。这个问题的明显解决办法是给每个接受人分配一个唯一的整数，称人数最多的接受人为“领先者”，只允许领先者投第一张决定性的一票。
因此，接受者首先相互沟通，弄清楚谁是领导者，然后领导者投票，追随者跟随。但这也违反了活跃性：如果领导者死亡，追随者就会无限期地等待。解决这个问题的一个办法是，如果领导者死亡，让第二高接受者接管领导权。但在我们的假设下，很难将领导人去世的情况与网络连接非常糟糕的情况区分开来。因此，天真地选择继任者会导致分裂投票和再次停滞不前(众所周知，权力交接在现实生活中对威权政权也是有问题的！)。如果有某种形式的…就好了。分布式协商选出领袖算法！
这是我们开始讨论真正的Paxos的地方：-)它从“投票投票”算法开始。这个算法和我们已经看到的算法一样，没有定义任何消息。相反，消息传递是一个实现细节，所以我们稍后再讨论它。
回想一下，舞弊投票要求所有接受者投票给单一的值。它不受分开投票的影响，但当领先者脱机时容易被卡住。抽签背后的想法是有许多轮投票，即抽签。在每一轮投票中，接受者只能投票给单一的值，所以每一票都可能被卡住。但是，由于我们正在进行多轮投票，有些选票会取得进展。如果值是由一定的法定人数选择的，那么它就是在投票中选出的。如果值是在某些选票中选出的，那么它就是在一个整体的算法中选出的，如果它是在一些选票中选出的，那么它就是在一个整体的算法中选出的。
图灵奖的问题是：我们如何确保没有两个选票选择不同的值？请注意，如果两个选票选择相同的值也是可以的。
让我们真的粗暴地强行回答这个问题。首先，假设选票是有序的(例如，用自然数编号)。假设我们想要在选票b中选择某个值v来投票。什么时候v是安全的？好的，当其他任何选票都不能选择其他值v1时。让我们把这个限制得更紧一些。
如果任何较小的选票b1(b1<；b)没有选择也不会选择除v之外的任何值，则值v在选票b处是安全的。
所以，简单地说，我们只需要预测未来将选择哪些价值观，我们就完成了！我们稍后会处理这个问题，但让我们首先说服自己，如果我们只选择安全的价值观进行投票，我们就不会违反共识规范。
所以，当我们在某一次投票中选择一个安全值v时，它可能会在这次投票中被选中。我们需要检查它是否不会与任何其他值冲突。对于较小的选票，这很容易 - ，这是安全条件的定义。如果我们与将来投票中选择的某个值v1发生冲突怎么办？嗯，这个值也是安全的，所以无论谁选择了v1，都肯定它不会与v冲突。
我们如何解决预知问题？我们将要求接受者承诺不在某些选票中投票。例如，如果你正在寻找一个安全的b选票值，并且知道有一个法定人数Q，这样每个法定人数成员从未在较小的选票中投票，并且承诺永远不会在较小的选票中投票，你可以确定任何值都是安全的。事实上，任何较小选票中的任何法定人数都将至少有一个成员拒绝投票给任何值。
好的，但是如果有一些法定成员已经在一些选票b1和b中投票给了某个v1呢？(深呼吸，下一句话是Paxos核心思想的核心)。嗯，这意味着v1在b1是安全的，所以，如果b1和b之间没有选票，v1在b！(呼气)也是安全的。换句话说，要在b选择一个安全值，我们：
在法定人数成员已经投出的所有选票中，我们选择得票数最高的一张。
为了实现“永不投票”的承诺，每个接受者将保持maxBal值，永远不会在小于或等于maxBal的选票中投票。
让我们停止挥手，把这个算法付诸数学。另外，我们还没有考虑消息，只是假设每个接受者都可以观察整个系统的状态。
集合：𝔹--编号的选票集合(例如，ℕ)𝕍--任意值集合𝔸--接受者的有限集合ℚ∈2^𝔸--仲裁集合假设：∀Q1，Q1∈ℚ：Q1∩Q2≠{}Vars：--(接受者，选票，值)三重投票集合∈2^(𝔸×𝔹×𝕍)--将接受者映射到选票编号或-1的函数。--MAXBAL：：𝔸->；𝔹∪{-1}MaxBal∈(𝔹∪{-1})^𝔸Vote(a，b)≡∃v∈𝕍：(a，b，v)∈votesSafe(v，b)≡∃q∈ℚ：∀a∈q：maxBal(A)≥b-1∧∃b1∈𝔹∪{-1}：∀b2∈[b1+1；B-1]，a∈q：，投票(a，b2)∧b1=-1∨。
.