容错寄存器仿真算法的自动验证方法及其应用

理论计算机科学电子笔记149（2006）49-60www.elsevier.com/locate/entcs容错寄存器仿真Paul C. 阿蒂1美国马萨诸塞州波士顿东北大学计算机科学学院。和MIT CSAIL，Cambridge，MA，USA.Hana Chockler2IBM研究实验室，以色列海法。摘要容错分布式算法的设计和验证是一项复杂的任务。 通常，正确性的证明是手动完成的，因此取决于证明者的技能。使用自动验证方法，如模型检查，可以大大简化验证。然而，分布式算法的模型检测往往是棘手的，因为状态爆炸问题。在本文中，我们提出了一种新的方法来验证基于法定人数的分布式寄存器仿真算法与不可检测的崩溃失败的进程。我们的方法是基于投影和抽象，使我们能够减少整个系统的模型检查的任务，公平的模型检查的子系统组成的一个常数数量的进程。我们的方法是高度可扩展的，可以应用到一个大类的算法。 除了有效的验证之外，它还可以用于发现现有算法中的冗余。关键词：分布式算法，参数化系统，容错，崩溃故障，寄存器仿真，自动验证，模型检查1引言形式验证被广泛认为是确保大型复杂软件系统正确行为的关键手段。这些系统通常1电子邮件：attie@ccs.neu.edu2电子邮件：hanac@il.ibm.com1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.01650P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）分布式的，并且包含大量的组件或过程，这些组件或过程容易发生各种故障。因此，这种系统的分布式算法必须是容错的。这种算法的设计是一项复杂的任务，其正确性的手动证明通常非常复杂。这种系统的自动验证受到状态爆炸问题的限制，即使对于中等规模的系统，状态爆炸问题也变得尖锐最近在参数化系统领域的研究，即由（通常）小而简单的模块的潜在大量实例化组成的系统，使用了抽象和演绎验证等技术（参见[9]的调查）。这些技术都不涉及容错。本文研究了进程崩溃失效不可测我们假设有大量的进程，可以将其放入少量的读取器、写入器和服务器（存储共享数据对象的值），因此这些系统可以被视为参数化系统。在具有不可检测的崩溃故障的系统中，故障进程停止与其他进程的通信，但其他进程无法检测到故障也就是说，一个失败的过程与一个“非常慢”的过程是无法区分的我们不考虑拜占庭式的失败，失败的过程可以任意行为，特别是，可以偏离其算法。我们考虑的分布式算法模拟共享寄存器，并基于仲裁系统。在quorum系统中，每个广播操作只等待来自quorum进程的响应，而不是所有进程的响应。存在不同类型的法定人数系统。所有法定人数系统的共同特征是每两个法定人数的交集是非空的。把这个特征作为一个公理，我们抽象出一个特定的法定人数系统。我们提出了一种方法，通过完全可靠的模型检查过程，基于群体的并发算法的建模和验证的崩溃失败非正式地，我们的方法如下。我们用量化的LTL公式表示系统的正确性（安全性和活性）性质然后，我们证明了过程上的量化可以被子系统上的量化所取代，每个子系统包含常数数量的过程并执行常数数量的请求，同时保持公式的语义等价性。然后对这些小的子系统进行模型检查，从而得出整个系统的正确性在一般的系统中，我们必须验证所有可能的子系统，由于子系统的数量与进程的数量成指数关系，因此不能对任意数量的进程自动进行验证关键的想法，这使我们能够检查只有一小部分的子系统，是我们考虑的系统组成的一小部分P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）51侧突如果两个进程运行相同的算法，并且在执行的当前时刻处于相同的状态，则它们被放置在相同的等价类由于服务器进程存储寄存器的值，因此在检查等价性时也要考虑存储在服务器中因此，每个过程的直接实现都会产生一个具有无限数量状态的结构然而，由于我们只处理具有恒定数量进程的子系统，并且基于法定人数的决策仅基于时间戳之间的比较（而不是它们的绝对值），因此我们能够抽象时间戳的绝对值，而只使用它们的相对值。由于子系统中的请求数量是恒定的，因此时间戳的数量也是恒定的，因此我们能够表示它们的比较值由一个常数数量的布尔变量。当我们构建子系统时，我们将进程投影到子系统上，抽象出子系统中所有不可访问的状态和所有不可访问规划进程的主要问题是，在一个大型系统中，进程根据基于法定人数的决策执行转换由于在一个常数大小的子系统中，法定人数的过程是不可访问的，我们取代法定人数为基础的决定，非确定性的决定。这种替换产生了原始系统中不存在的非法执行第一种类型的非法执行是客户端进程在接收到最新的回复之前不确定地移动到输出被选择的状态我们总是在当前quorum与我们模型检查的小子系统中的所有其他quorum的交集中包含一个进程，从而过滤掉这样的执行第二种类型是进程停留在“等待答复”状态并且永远不会终止的执行我们通过用公平模型检查替换常规模型检查来过滤这种执行，其中公平性约束有效地表达了“总是有一个活的进程法定人数”的条件模型检查小型子系统的另一个优点是具有教育意义。也就是说，算法的一部分的必要性可以很容易地通过从模型中删除这一部分并对更改的子系统进行模型检查来验证。如果修改后的子系统仍然满足所需的属性（非空的），这意味着删除的部分对于算法的正确性不是必需的。52P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）2预赛2.1时态逻辑与Kripke结构在模型检查中，我们检查一个以Kripke结构（标记为状态转移图）给出的系统是否满足以时态逻辑公式（或有限自动机）给出的规范。在本文中，我们假设规格是在线性时序逻辑LTL [8，4]中给出的。术语poralogic的语义是用krepeke结构来定义的。我们使用Bu？chi公平性约束，如果一个执行访问一个公平的状态无限次，那么它就是公平2.2寄存器读/写寄存器（或简称为寄存器）类型支持具有任意初始状态vo∈Vals的值的任意集合Vals。它的调用是读和写（v），对于某些v∈Vals。它的响应是v和ack。它的顺序指定f要求每个写操作覆盖最后写入的值并返回ack（即f（write（v），w）=（ack，v））;每个读操作返回最后写入的值（即f（read，v）=（v，v））。 中系统由进程P1，P2，. . ，进程Pi通过读i和写i（v）形式的输入动作与共享寄存器交互，并输出形式为Vi和ACK的动作。读/写寄存器被称为k-reader/m- writer，如果只允许k个进程读，m个进程写寄存器。当读者（作者）的数量不受限制时，我们使用术语多读者（多作者）。我们现在定义几个寄存器属性。在我们的定义中，我们谈论读和写操作。与I/O操作（定义为原子操作）相反，操作在请求被放入系统时开始，并在结果返回时终止：读操作的结果是一个值，写操作的结果是写操作成功终止的指示当用量化的LTL表示寄存器属性时，我们用ri表示第i个读操作，用wi表示第i个写操作，用si表示第i个服务器。为了表达进程之间的顺序，我们为每个操作的开始和结束引入了新的布尔变量：opi.b（opi.e）在opi的第一个（最后一个）操作执行时从false变为true我们使用Lamport（op1严格地在op2之前）是G（op2.b→op1.e）的捷径，并且op1参与op2（op1is concurrently withop2）是<$（op1→op2）<$$>（op2→op1）的捷径，并且<$表示布尔蕴涵。 我们还使用变量wi.val作为值由wi写入，ri.val表示由ri读取的值，si.val表示si保存的值。这些值是数据值和时间戳的对，即opi。val=P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）53好吧，好吧。 当比较两个值时，我们说opi.val = opJ.val iJ Jjopi.val.v=opj.val.v和opi.val.ts=opj.val.ts。 设x是一个寄存器，σ是x的调用和响应的序列。以下单写入器多读取器系统中寄存器的定义取自[7]。• 安全寄存器：如果每个完整的读操作不与任何写操作重叠，则σ是安全的，如果还没有值被写入，则返回最新的写入值或初始值。一个寄存器x是安全的，如果它的所有迹σ都是安全的。从形式上讲，<$wi，r：G[（wi→r）<$（<$$>wj：wi→wj→r）<$（<$$>wk：wkParticipr）<$F（r.val = wi.val）]。（一）我们注意到，我们只表达了当有以前的写入时返回正确值的条件当没有以前的写，要求是平凡的表达。• 正则寄存器：如果σ是安全的，并且与某些写操作重叠的每个读操作返回重叠写的值之一或最新的非重叠值，则σ是正则的一个寄存器x是正则的，则它的所有迹σ都是正则的。形式上，该附加要求表示为<$wi，r：G[（wi→r）<$（<$$>wj：wi→wj→r）<$F（r.val = wi.val） wk：（wkParticipr（二）• 原子寄存器：σ是原子的，如果它是规则的，并且所有对σ的调用都可以线性化（参见[6]的定义）到一个顺序寄存器（也就是说，一个没有重叠操作的寄存器）。一个寄存器x是原子的，则它的所有迹σ都是原子的。从形式上讲，如果一个寄存器满足公式2，那么它就是原子的，此外，<$w1，w2，r1，r2：G[（（r1→r2）<$F（w2.val=r1.val）<$F（w1.val=r2.val））<$<$F（w1→w2）]。（三）为了这项工作的目的，我们认为一个操作是活的，如果最终达到终止状态（即，Fop.e成立）。2.3算法的特征化我们首先描述我们的方法所适用的算法R的类。R的特征如下。(i) R中的算法通过大量的服务器进程。54P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）(ii) 只有一个写程序3。(iii) 服务器可能会崩溃并停止响应请求。但是，始终存在一个有效的服务器法定人数(iv) 客户（作者和读者）是没有过错的。(v) 每个服务器在每个点只能保存一个值(vi) 所有值都带有（唯一的）时间戳。(vii) 在从服务器接收到不同的回复时，基于回复的时间戳来我们不限制每个客户端执行读/写值的轮数。然而，我们假设这个数字是恒定的。算法的每次调用（无论是读还是写）都可以与之前的调用隔离进行验证。这一观察使我们能够通过微进程对调用进行建模[2]。微进程实现单个操作（例如，一个单一的读或写），之后它被销毁。它的状态非常少，因此由微过程组成的系统可以很容易地进行模型检查。微进程的唯一问题是写入器应该存储当前的时间戳。我们通过假设将时间戳作为输入与输入值一起提供给写入器微进程来规避它在单写入器算法中，我们可以安全地假设这个输入时间戳是唯一的，并且随着每个后续请求而增加。在多作者算法中，需要更精细的推理。3基于Quorum的寄存器自动验证在这一节中，我们提出了我们的主要结果，即所需的安全性和活性性质可以在小的子系统中自动验证，整个系统的正确性可以从这些子系统的正确性中推导出来。这个结果由引理3.1和3.2得出。引理3.1来自R的算法的安全性质可以通过对有限个子系统的模型检验来验证，这些子系统包含常数数量的读取器和写入器。从本质上讲，我们证明了表示寄存器正确性的时间公式可以用普适量化器重写。公式的纯LTL部分最多涉及3我们的工作可以推广到多作者的情况。对于多个写入器进程，应执行额外的工作以证明时间戳的唯一性P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）554 客户. 由此产生的纯LTL公式为：safe=G[（wi→r）对于安全寄存器，n正则=G[（wi→r）（wi→wj→r）F（r.val=wi.val）<$（wkParticipr<$F（r.val=wk.val））]（5），用于常规寄存器，以及at=G[（（r1→r2）F（w1→w2）]（六）原子寄存器由于我们通过微进程对客户端进行建模，每个微进程只执行一个请求，因此子系统中的请求数量等于该子系统中的客户端数量。我们还没有完成，因为它仍然需要证明我们也能够考虑恒定数量的服务器。引理3.2引理3.1中的子系统可以由固定数量的服务器构成。 参与单个子系统的服务器数量以2 m为界，其中m是客户端（读取器或写入器）与该子系统中的服务器之间的通信回合数。证明是基于观察，在任何给定的时间在执行过程中有一个恒定数量的等价类的服务器。由于决策是基于时间戳而不是具有相同值的回复的数量做出的，因此我们只需要将每个等价类中的一个代表包括在子系统中由于每个通信回合将服务器集合除以2（分为在该回合中响应的服务器和未响应的服务器），因此m个回合将服务器集合除以2m。我们注意到引理3.2假设当前值存储在服务器的状态这导致在一个大系统中的状态数量无限然而，在我们考虑的常数大小的子系统中，值的数量是常数，因此每个服务器只有有限数量的状态是可达的。我们抽象出无法到达的状态。轮数取决于读取器和写入器的算法。例如，读取器微进程可以与服务器执行两轮通信，其中第一轮读取值，第二轮将其写入服务器。我们进一步注意到，没有回复任何客户端的服务器集可以忽略，因为它在系统的正确性中不起任何作用。结合引理3.1和引理3.2，我们能够通过模型检查一个常数数量的子模型来验证56P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）具有恒定数量（小）进程的系统它仍然显示如何基于法定人数的决定投射到小的子系统。我们通过用非确定性转换替换基于法定人数的转换来实现。显然，这种抽象创建了在全球系统中非法的执行。首先，一个进程现在可以无限地在等待仲裁响应的状态下循环，从而创建一个非终止执行。第二，现在允许它进入选择输出值的状态，而不管它收到的回复数量。我们通过用公平模型检查替换标准模型检查过程来处理第一个问题，其中公平性约束只允许执行进程等待仲裁回复的状态只发生有限次数的执行。这相当于始终存在一个有效的服务器法定人数的假设我们处理的第二个问题的产品Kripke结构的仔细建设在我们的产品Kripke结构中，我们希望消除所有与收到法定数量回复不一致的执行。我们依赖于法定人数系统的定义因此，我们构造小的子系统，使得对于子系统中的每一对通信轮，我们包括位于这两轮法定人数的交集中的单个服务器进程这确保了这对轮的正确安全属性得到验证，因为它们是由该服务器强制执行的。寄存器仿真的算法通常使用无界时间戳。幸运的是，由于我们的子系统由恒定数量的进程组成，并且使用了恒定数量的通信回合，因此我们能够抽象出无限的时间戳。对于单写入器系统中的安全、常规和原子寄存器的正确性属性，实际上，对于这些属性中的任何一个，写入小型子系统中的值的数量都不超过4。微调我们前面的推理使我们能够将参数化系统的验证减少到具有恒定数量进程的模型检查子系统我们表明，它succes考虑一个子系统与m个通信轮和 2m 个服务器。事实上，我们可以将子系统中的服务器数量减少到m（m−1）/2（轮对的数量）。事实上，对于R中算法的正确性证明来说，唯一必不可少的服务器是在读和写通信轮的法定人数的交叉点上的服务器。P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）574示例在本节中，我们将通过模拟共享读/写寄存器的算法示例来说明我们的方法我们从一个简单的单写入器多读取器系统中的安全寄存器的例子开始然后将其推广到Attiya等人在[3]中提出的算法。以下客户端和服务器进程的代码在一个总是存在大多数活动进程的系统中实现了单写入者假设下的安全寄存器[7]。作家（刘明）：增加TimeStamp;计数：= 0;向所有人发送TimeStamp和TimeStamp;在收到回复确认后，count：=count+1;直到count > n/2，其中n是进程数; return;服务器（MySQL）：在收到ECOMMECONDO后：案例分析：ReadRequest=ReadRequest：发送TimeStamp;M如果T imeStamp> LocalTimeStamp，则更新M;发送ACK;reader（）：计数：= 0;向所有人发送ReadRequest;在收到回复M，T imeStamp直到计数> n/2，其中n是进程数;选择消息M具有最大time-stampMaxT imeStamp;returnMaxTimeStamp;回想一下，安全寄存器满足等式4，该等式在三个写入器进程和一个读取器进程的子系统中被检查由于每个写入器进程调用一个写入请求，并且读取器进程调用一个读取请求，因此在子系统中存在写入和读取请求的法定人数的3个成对交叉点，并且因此存在3个服务器进程此外，在这个子系统中写入了三 因此，三个时间戳可以用三个布尔谓词来表示：p1（wi.val.ts > wj.val.ts）和p2（wi.val.ts >wk.val.ts），以及p3（wj.val.ts > wk.val.ts）。 由于系统有一个（全局）writer进程，因此在产品子系统中，三个写请求应该严格地彼此在前。而且，我们不必考虑wi→wj→r的顺序。单个写请求（即，微进程）和单个读请求到具有恒定数量进程的子系统上的投影在下图中呈现。我们假设正确的时间戳与输入值（即，val是一个元组）一起提供给了编写器微进程v，ts 通过抽象出子系统中不可访问的所有变量并计算所得结构的商抽象来获得投影。跃迁w1→w2和r1→r2是不确定的. 回想一下，我们通过替换58P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）SS1通过包括位于子系统中法定人数的交集中的服务器，具有公平模型检查和安全性的定期模型检查服务器进程将当前值及其时间戳存储在其状态中。因为在我们的子系统中有三个写请求，所以服务器进程在子系统上的投影具有有限数量的状态。图1显示了服务器进程在子系统上的投影，其中包含三个写操作。input（val）第0周w.b：=1send（ val）w1ack（）send（init−val）ss.b= 1read（）w.b：=0ackw.e：= 1（达到最大值）s0write（ val1）w2返回write（val2）write（val2），<$p1write（val3）子系统上写入（val）的投影s1s2s3write（ val1），p1读取r eq r0send（req）r1ack（val）r.b：=1o：= maxvalack（val）（majreached）read（）send（ val1）J J J1 2 3r.b：=0r.e：= 1r2返回（o）服务器在子系统read（）在子系统上的投影（maxval是具有最大时间戳的值）Fig. 1.安全寄存器仿真为了避免混乱的数字，我们省略了类似的过渡在S1和s2在S1和SJ。所有投影都以空闲状态结束而他们，也将永远在一起。由此产生的子系统是7个进程的产物，有3个写请求。因此，最大的进程是服务器，其大小取决于写请求的数量。在这种情况下，它有8个状态（每个值2个状态，初始状态和返回初始值因此，直接的实现导致可以用21个变量编码的子系统。过滤掉导致属性的空洞满足的交织，并注意到来自服务器的回复被假设为以已知的顺序接收，从而产生子系统，该子系统是3个客户端和2个服务器（其总共具有25个状态）、一个客户端（写入器wk）和一个服务器（其位于wk和r的法定人数的交集中）的顺序组合的叉积。与时间戳一起，这个子系统可以使用12个布尔变量进行编码Attiya等人的算法[3]用于在具有崩溃故障的单写入器多读取器异步消息传递系统中模拟常规寄存器SP.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）59与我们上面研究的阅读器进程代码中的示例不同在该算法中，读取器进程执行两轮：一轮读取请求，然后一轮写入请求，其中写入请求具有从读取请求接收的值阅读器微进程在子系统上的投影如下图所示。这种差异导致了寄存器的原子性。回想一下，原子性由等式5和等式6表示。在三个写入器微处理和一个微处理的子系统中检查等式5。读reqr10的r.b：=1send（ req）R1ack（ val）阅读器微处理器请注意，读取器发出一个读请求和一个写请求，因此子系统包含4个ack（val）o：=maxval（majreached）R2发送（o）服务器进程。世界上最大的子系统是一个服务器，它有10个返回（o）R4r.b：=0r.e：=1确认R3状态，从而产生子系统read（）在子系统上的投影可以使用最多30个布尔值进行编码（maxval是具有最大时间戳的值）变量在两个写入器和两个读取器微进程的子系统中检查等式6该子系统包含8个服务器，因此最终子系统可以使用最多44个布尔变量进行编码。对于这两个属性，应用上述推理进一步减小了子系统的大小。第二轮读的必要性通过抽象出第二轮读并对结果子系统进行模型检查，我们可以证明，为了确保总是返回最后一个前一个写值或并发写值的属性，我们只需要一轮读。另一方面，两轮读取对于证明原子性是必不可少事实上，我们可以构造一个子系统，其中两个写入顺序组合，一个读取与最后一个写入并发，其中等式5成立，自动生成有趣的见证来展示两种类型的满足：有一个执行，其中读取返回第一个写入写入的值，另一个执行，其中读取返回第二个写入写入的值由于这对两个读都是如此，无论它们的顺序如何，存在这样的执行，其中第一个读返回第二个写的值，第二个读返回第一个写的值5结论和今后的工作我们提出了一种方法来建模和验证分布式算法的寄存器仿真，允许崩溃故障少于法定数量的服务器。我们认为，整个系统的正确性（安全性和活性）属性可以在恒定大小的子系统中自动进行模型检查，然后60P.C. 阿蒂，H。Chockler/Electronic Notes in Theoretical Computer Science 149（2006）外推到整个系统。 我们通过用非确定性转换替换基于定额的转换来避免检查进程的定额，并且我们展示了如何过滤掉由非确定性创建的非法执行。通过小型抽象系统对分布式算法进行建模和自动验证，可以通过抽象出有问题的部分并对生成的系统进行模型检查，来帮助确定算法的哪些部分对于其正确性是真正重要的。虽然我们在本文中考虑的例子相当简单，但我们相信，将这些方法应用于更复杂的算法可能会带来有趣的见解，甚至改进现有的算法。我们构造的小的子系统的正确性意味着整个系统的正确性，这还有待于形式化地证明并发系统的成对表示[1]为这些证明提供了形式框架文[1]的方法可以从分析成对过程的产品推广到分析少量过程的产品。引用[1] P. C. Attie和E.A. 爱默生具有许多相似进程的并发系统的综合ACM Trans.程序. 浪系统，20（1）：51[2] P.C.阿蒂从动态规范综合大型动态并发程序。技术报告，东北大学，2003年。[3] H. Attiya，Bar-Noy A.，和D.多列夫在消息传递系统中健壮地共享内存。J. ACM，42（1）：124-142，Jan. 一九九五年[4] E.A.爱默生时态和模态逻辑。在理论计算机科学手册，B：16，pp。997-1072.麻省理工学院出版社，1990年。[5] 作者：Michael J. Lynch，and Michael S.帕特森不可能通过一个错误的过程达成分布式共识。J.ACM，32（2）：374[6] M. Herlihy和J.M.翼线性化：并发对象的正确性条件。ACM翻译计划。Lang.系统，12（3）：463[7] L.兰波特进程间通信-第二部分：算法。Distributed Computing，1（2）：86[8] Z. Manna和A.普努埃利并发程序的验证：时态框架。计算机科学中的正确性问题，215[9] L. Zuck和A.普努埃利 模型检查和抽象到 借助参数化系统。计算机语言-特别问题（出现）。