注意：此网页是从单词Original自动转换而来的。格式和图片可能有问题。要查看预期表单，请单击以下链接之一。
更早的版本出现在分布式算法ed中。Babaoglu和Marzullo，计算机科学讲稿1151，Springer，1996，第1-17页。摘要、后记、Acrobat、Word。。Lamport展示了复制的确定性状态机是实现高可用性系统的一般方法，给出了副本可以用来就每个输入达成一致的一致算法。他的Paxos算法是在没有实时保证的情况下获得共识的最容错的方式。因为一般的共识是昂贵的，实用的系统将其保留用于紧急情况，并将租赁(超时锁定)用于大部分计算。本文阐述了高效高可用计算的一般方案，给出了理解并发和容错程序的一般方法，并以Paxos算法为例进行了推导。如果系统按需迅速提供服务，则该系统是可用的。用较少的可用组件制作高可用性系统的唯一方法是使用冗余，这样即使系统的某些部分出现故障，系统也可以正常工作。最简单的冗余是复制：为每个部分制作几个副本或复制品。
本文阐述了如何利用副本构建高效的高可用性系统，并对关键算法进行了详细的描述和非形式化的正确性证明。几乎所有的想法都归功于Leslie Lamport：复制状态机[5]、Paxos一致性算法[7]，以及指定和分析并发系统的方法[6]。我之所以写这篇论文，是因为我看过Lamports的文件后，仍然花了很长时间来理解这些方法，以及如何有效地使用它们。令人惊讶的是，尽管他们优雅而强大，但似乎很少有人知道他们。
在下一节中，我们将解释如何构建既高效又高度可用的复制状态机，并给出一致性的容错算法。第三节介绍了共识问题及其应用的一些背景知识。第4节回顾了我们用来编写规范的方法，并使用它以几种形式给出了一致意见的精确规范。在第5节中，我们介绍了Paxos一致性算法背后的基本思想，并从该思想和规范中推导出该算法。最后，我们解释了一些重要的优化，并总结了我们的结论。
冗余是不够的；要发挥作用，就必须进行协调。要做到这一点，最简单的方法是让每个无故障的副本执行相同的操作。则任何无故障的副本都可以提供输出；如果副本不是故障停止的，则需要来自f个副本的相同输出将容忍f-1个故障。更复杂类型的冗余(例如纠错码)更便宜，但它们取决于所提供的服务的特殊属性。
在本节中，我们将说明如何以完全通用和高度容错的方式协调副本。然后，我们探索一种称为租赁的优化，它使协调在几乎所有情况下都非常有效。
我们如何安排每个复制品做同样的事情？采用Lamport[5]首次提出的方案，我们将每个副本构建为确定性状态机，这意味着转换关系是从(状态，输入)到(新状态，输出)的函数。通常将这些副本中的一个称为进程。在相同状态下启动并看到相同输入序列的几个进程将执行相同的操作，即以相同的状态结束并生成相同的输出。因此，要实现高可用性，我们所需要的就是确保所有未出错的进程都能看到相同的输入。这方面的专业术语是共识(有时称为协议或可靠广播)。我们非正式地说，如果几个过程都在某些价值上达成一致，那么它们就会达成共识；我们稍后会给出一个正式的定义。
因此，如果几个进程实现了相同的确定性状态机，并且在输入的值和顺序上达成了共识，那么它们也会做同样的事情。通过这种方式，可以复制任意计算，从而使其高度可用。当然，我们可以通过在输入集合上定义一些总顺序来使顺序成为输入值的一部分，例如，通过将它们编号为1、2、3、……
在许多应用程序中，输入是从客户端到复制服务的请求。例如，复制的存储服务可能具有读取(A)和写入(a，d)输入，而飞机飞行控制系统可能具有ReadInstrument(I)和RaiseFlaps(D)输入。不同的客户端通常独立地生成它们的请求，因此不仅需要就请求是什么达成一致，而且还需要就服务它们的顺序达成一致。要做到这一点，最简单的方法是用连续的整数对它们进行编号，从1开始。这在主拷贝复制中完成，因为一个进程(主)很容易分配连续的编号。因此，存储服务将同意输入1=WRITE(x，3)和输入2=READ(X)。
当请求的总顺序不是从连续整数导出时，还有许多其他方案可以在请求顺序上达成共识；请参阅Schneiders调查[11]。这些方案用一个完全有序的集合(例如，(客户端UID，时间戳)对)中的一些值来标记每个输入，然后设计一种方法来确保您已经看到标签小于给定值的所有输入。这很复杂，实际系统通常使用主节点对输入进行排序。
容错共识是昂贵的。单个进程的独占访问(也称为锁定)成本很低，但它不能容错-如果一个进程在持有锁时失败，则其他任何人都无法访问该资源。向锁添加超时可实现容错锁或租约。因此，进程持有状态组件或资源的租约，直到到期时间；我们说，当进程持有租约时，它是资源的主进程。在租约到期之前，任何其他进程都不会接触该资源。当然，要实现这一点，进程必须具有同步的时钟。更准确地说，如果两个进程的时钟之间的最大偏差是e，并且进程Ps的租期在时间t到期，则P知道在Ps个时钟的时间t之前没有其他进程会接触到该资源。
当主机持有租约时，它可以自由地读写资源。写入必须花费有限的时间，以便可以保证写入失败或先于租约到期后开始的任何操作；对于SCSI磁盘等资源来说，这可能是一个严重的问题，因为它的排序保证较弱，写入可能需要的时间上限很长。
事务处理系统中的锁通常是租用的；如果它们过期，事务将中止，这意味着它的写入被撤消，事务等同于跳过。使用事务作用域之外的租用的进程必须注意提供任何必要的原子性，例如，通过确保资源在每次原子写入之后处于良好状态(这称为仔细写入)，或者通过使用基于日志的标准重做或撤消方法[4]。如果被租赁的资源本身被复制，则几乎可以肯定后者是必要的。
进程可以通过在资源到期前续订其租约来保持对资源的控制。它还可以释放租约，也许是根据需要。但是，如果您无法与持有租约的进程对话(可能是因为它失败了)，则必须等待租约到期后才能接触其资源。因此，在续订租约的成本和(可能)失败后必须等待租约到期的时间之间存在权衡。短期租约意味着在恢复期间等待时间较短，但续订租约的成本较高。长期租赁意味着在恢复期间需要等待很长时间，但续约成本较低。
租约最常用于在知道状态不能更改的情况下，授予进程缓存状态的某些部分(例如缓存行或文件的内容)的权利。因为租约是一种锁，所以它可以有一种模式来确定它的持有者可以执行哪些操作。如果租赁是独占的，则其进程可以自由更改租赁状态。这类似于拥有者对高速缓存线的访问或多端口磁盘的所有权。
在容错系统中，必须通过运行协商一致的方式授予和续订租约。如果这么多地使用共识仍然太昂贵，解决方案是分层租赁。运行一次协商一致选举沙皇C，并给予C国家大部分地区的租赁权。现在C把x和y上的分租租给主人。每个主服务器控制其自己的资源。房主们与沙皇续签了转租合同。这很便宜，因为它不需要任何协调。沙皇以协商一致的方式续签租约。这更贵，但只有一份沙皇租约。此外，沙皇可以很简单，不太可能失败，所以更长的租期可能是可以接受的。
通过将共识、租赁和层次结构的思想结合起来，可以构建高可用性、高效率的系统。
如果几个过程都同意某个称为结果的允许值(如果它们可以就任何值达成一致，那么解决方案将是微不足道的：总是同意0)，那么几个过程就会达成共识。因此，与共识的接口有两个动作：允许一个值，并读取结果。当所有非故障进程都知道结果时，一致算法终止。
除了通用复制状态机之外，还有许多专门的一致性应用程序。三个受欢迎的是：
分布式事务，其中所有进程都需要就事务是提交还是中止达成一致。每笔交易都需要就其结果达成单独的共识。
成员资格，在这种情况下，协作提供高可用性服务的一组进程需要就哪些进程当前作为该组的成员运行达成一致。每次流程失败或重新开始工作时，都必须达成新的共识。
如果没有缺点，达成共识是很容易的。下面是一个简单的实现。有固定的领导流程。它获得所有允许操作，选择结果，并告诉每个人。如果它失败了，你就不走运了。标准的两阶段提交是这样工作的：如果所有参与者都准备好了，则允许值为Commit，如果至少有一个参与者失败，则中止。如果领导者失败了，结果可能是未知的。
另一个简单的实现是拥有一组进程，每个进程选择一个值。如果多数人选择相同的值，这就是结果(可能的多数人是具有任意两个多数人具有非空交集的属性的子集)。如果进程选择的值没有多数，则没有结果。如果多数党的一些成员失败了，结果将是未知的。
当存在缺陷时，达成共识是很棘手的。在一个异步系统中(在这个系统中，一个无故障的过程可能需要任意的时间来进行转换)，具有完美的链接，甚至只有一个有故障的过程，没有保证终止的共识的算法[3]。在同步系统中，即使进程有任意或恶意的错误(拜占庭协议)，也有可能达成共识，但在发送的消息和时间上代价高昂[9]。
我们正在研究这样的系统，其状态是某个(不一定是有限的)状态空间中的一个元素，以及将系统从一种状态带到另一种状态的一组动作(不一定是确定性的)。数据抽象、并发程序、分布式系统和容错系统都可以用这种方式建模。通常，我们将状态空间描述为称为变量的较小空间的笛卡尔乘积。
在指定这样的系统时，我们将一些操作或变量指定为外部操作或变量，而将其余操作或变量指定为内部操作或变量。我们关心的是外部操作的序列(或者等价地，外部变量的值序列)，因为我们假设您不能从系统外部观察内部操作或变量。我们称这样的序列为系统的踪迹。规范是一组跟踪，或者相当于跟踪上的谓词。这样的集合称为属性。
我们可以定义两种特殊的性质。非正式地，安全属性断言不会发生任何糟糕的事情；它是顺序程序部分正确性的推广。活跃性属性断言好事最终会发生；它是终止性的推广。您总是可以通过查看跟踪的某个有限前缀来判断该跟踪没有安全属性，但是对于活动属性，您永远不能这样做。任何属性(即任何一组操作序列)都是安全性属性和活跃性属性[2]的交集。
在本文中，我们只讨论安全属性。这似乎是合适的，因为我们知道异步共识没有终止算法。这也是幸运的，因为活动性属性更难处理。
由状态机定义安全属性很方便，状态机的动作也分为外部动作和内部动作。机器的所有外部动作序列定义一个安全属性。不要将这些规范状态机与我们使用共识实现的复制状态机混淆。
Y的每一个迹都是X的迹，也就是说，Y的安全性质蕴含着X的安全性质。
第一个要求确保您不能通过观察Y来判断它不是X；Y永远不会做X不会做的坏事。第二个确保Y做了X应该做的所有好事。我们不会再说任何关于活泼的事了。我们可以更简明地说明这个定义：实现就是隐含。
按照这种方法，要指定具有状态的系统，我们必须首先定义状态空间，然后描述动作。我们选择状态空间是为了使规范清晰，而不是为了反映实现的状态。对于每个动作，我们都会说明它对国家的影响，以及它是外部的还是内部的。我们通过一系列操作(其中一个是Read(X)返回3)，对一个带有参数和结果(如read(X))的操作进行建模；当客户端读取x且结果为3时，就会发生此操作。
记法很重要，因为它可以帮助您思考正在发生的事情。创造一个合适的词汇。
对不起，我给你写了这么长的信，我没时间写短的。
帕斯卡我们现在已经准备好给出协商一致的具体说明。有一个被初始化为nil的结果变量，以及一个可以被调用任意次的操作ALLOW(V)。还有一个要读取结果变量的操作结果；它必须返回nil或v(这是一些允许操作的参数)，并且必须始终返回相同的v。
：每一个非零的结果都是一样的。：非零结果等于某个允许值。有效性意味着结果不能是任何任意值，但必须是允许的值。共识是通过选择某个允许值并将其分配给结果来达成的。此规范在到达允许值时即时做出选择。
下面是该规范的精确版本，我们称之为C。它给出了状态机的状态和操作。该州为：
在这里，外部操作用*标记。保护是一个前提条件，在当前状态下必须为真，才能使动作发生；对于这两个动作都为真(用空格表示)。选择..。或者.。表示非确定性选择，如Dijkstras保护命令。
请注意，即使在做出选择之后，也允许结果返回零。这反映了这样一个事实：在具有多个副本的实现中，结果通常是通过仅与其中一个副本对话来实现的，而该副本可能还没有了解到选择。
接下来，我们给出了具有终止性的一致性规范T。一旦发生内部终止操作，就可以保证结果不会为零。您可以通过调用Done来了解算法是否已经终止。我们通过装箱来标记C中的更改。
：结果：值？{nil}最初为空请注意，规范T没有说明是否会实际发生终止。结果总是返回nil的实现满足T。这看起来可能不令人满意，但这是我们使用异步实现所能做的最好的。换句话说，更强的规范将排除异步实现。
最后，这里是延迟共识的一个更复杂的规格D。它累积允许的值，然后在内部操作Agree中选择其中之一。
：OUTPUT：VALUE？{nil}初始空完成：Bool初始FALSE很明显D实现了T。但是，要使用下一节中描述的抽象函数方法来证明这一点，需要一个预测变量或反向模拟[1，10]，因为C和T一看到允许值就会选择结果，而实现可能会在很长时间之后才做出选择。我们给出D规格有两个原因。其一是有些人发现它比T更容易理解，尽管它有更多的状态和更多的动作。另一种是将对预言变量的需要转移到D实现T的证明中，从而简化了Paxos实现D的更为微妙的证明。
在本节中，我们首先解释用于显示实现符合规范的抽象函数方法。该方法具有通用性和实用性。然后，我们给出了一些设计和理解实现的提示，并用抽象函数说明了前面给出的简单实现的方法和提示。下一节将展示如何使用该方法和提示推导Lamports Paxos一致性算法。
工具的定义告诉我们必须做什么(忽略活跃性)：证明Y的每一条痕迹都是X的一条痕迹。从头开始做这件事是痛苦的，因为一般来说，每条痕迹都是无限长的，而Y有无限多的痕迹。因此，证明需要归纳法，我们希望有一种证明方法可以一劳永逸地完成这一归纳法。幸运的是，有一种通用的方法可以证明Y实现了X，而不需要对每种情况下的踪迹进行显式推理。这种方法最初是由Hoare发明的，目的是证明数据抽象的正确性。它被Lamport[6]等人推广到任意并发系统。
该方法的工作方式如下所示。首先，定义一个从Y状态到X状态的抽象函数f，然后展示Y模拟X：
2)对于每个Y动作和每个可达状态y 有一系列X操作(可能为空) 外在也是一样的， 这样这张图就可以往返了。
如果在丢弃所有内部动作后X动作序列与Y动作序列相同，则它们在外部上与Y动作相同。因此，如果Y动作是内部的，那么所有的X动作都必须是内部的(可能根本不是)。如果Y动作是外部的，则除了一个必须与Y动作相同的X动作之外，所有的X动作都必须是内部的。
简单的归纳表明Y实现了X：对于任何Y行为，我们都可以构造一个外部相同的X行为，方法是使用(2)将每个Y动作映射到外部相同的X动作序列。那么X动作的序列在外部将与原始的Y动作序列相同。
如果Y实现了X，是否总是可以用这种方法来证明它。答案是几乎是。可能需要通过添加辅助历史和预测变量Acc来修改Y。
.