使用模型检测方法对Paxos算法进行验证与改进

何东炼，杨晋吉，赵淦森，管金平

(华南师范大学 计算机学院，广州 510631)

1 引 言

分布式是实现横向拓展，提升系统性能和可靠性的重要技术理论.现实实现中，分布式系统难以在分区失效、通信故障情况下对特定的状态形成全局共识和一致性，因此系统需要使用共识算法[1]来保证系统内的节点达成一致的状态.Paxos算法[2]是Lamport提出的一种共识算法，主要用于解决基于消息传递通信模型的分布式系统如何就某个值达成一致的共识，由于其在数据一致性方面的优秀表现，已被应用于许多重要的分布式服务中，并且存在多种变体.

Paxos算法在工业应用中具有明显优势并达到良好的性能和效果，因此对其进行深度的形式化分析和证明[3]工作至关重要.由于算法问题的复杂性，非形式化的证明往往容易出错，而形式化的验证，能够更好地对算法的性质进行分析与研究.模型检测[4]是形式化验证的主要方法之一，能够穷举目标模型的状态空间，以确定目标是否满足所需性质，常用于分布式系统的验证[5].

本文首先对Paxos算法及其研究进展进行介绍，然后根据算法流程对其进行形式化建模，以时态逻辑对算法的安全性、活性和活锁可能性进行描述，将模型与需要验证的性质输入模型检测器进行验证.验证结果表明，Paxos算法满足安全性和活性，但在运行过程中有发生活锁的可能，通过模型检测器重现了发生活锁时系统的运行轨迹并对其进行分析，最后对Paxos算法进行改进，解决其活锁问题并重新进行验证.

2 Paxos算法及其研究进展

随着分布式系统的迅速发展和广泛应用，用于分布式系统保持一致性的共识算法的研究和讨论也越来越多.Paxos算法最初由Lamport提出，之后学者们便不断对该算法进行改进，较为知名的有Multi-Paxos、Fast-Paxos、EPaxos、Raft等[6].Google的spanner[7]使用Multi-Paxos作为分布式共识保证的基础组件，PaxosStore[8]是腾讯开发的、用于支持微信核心业务的分布式存储系统.此外，Paxos算法也经常应用于软件定义网络及区块链研究[9，10].

目前，已有学者对Paxos算法的形式化验证进行了一些相关的工作，近年来的相关研究有：文献[11]使用SPIN对Paxos进行了建模，以断言的方式验证了算法的安全性.文献[12]使用TLAPS验证Multi-Paxos 的安全性.文献[13]使用有色Petri网对Paxos算法生成自动测试用例.文献[14]开发了一种基于有效命题逻辑的演绎验证方法，对Paxos及其几种变体的安全性进行了验证.文献[15]构建了Paxos的Heard-Of模型，使用PSync语言验证了模型的安全性和活性.文献[16]使用IronFleet对以Multi-Paxos为核心的状态机复制系统进行验证，证明了其安全性和活性.文献[17]使用交互式定理证明系统Coq对Paxos进行了安全性的验证.

而本文的主要工作有：

1)使用SPIN对Paxos算法进行形式化建模，以线性时序逻辑(Linear-time Temporal Logic，LTL)对算法的安全性、活性和活锁的性质进行描述.

2)对Paxos算法性质进行验证分析，还原算法不满足性质时的运行轨迹.

3)对Paxos算法进行改进，使算法满足所需的性质，并重新进行验证.

3 对Paxos算法进行模型检测

在模型检测中，验证目标是否满足某种性质，通常包含以下3个步骤：

1)建模.将需要进行验证的目标转化为能被模型检测器接受的模型.如果模型过于复杂，会发生状态空间爆炸问题，即系统过于复杂导致状态过多使验证失败，因此需要使用抽象或偏序约简等技术对模型进行化简.

2)规约.把目标需要验证的性质用时态逻辑表达式来进行表述.线性时序逻辑是常用的时态逻辑.

3)验证.将模型和时态逻辑表达式作为模型检测器的输入，运行检测器并检验结果.如果模型不满足性质，检测器通常可以提供一个模型不满足性质时的运行轨迹.

3.1 Paxos算法建模

Paxos算法把系统节点主要分为proposer，acceptor，和learner这3种角色.proposer提出提案，提案包括提案编号和提议的值.acceptor接收提案，若提案获得多数的acceptor接受，则称该提案被批准.learner学习提案，从acceptor学习最新被批准的提案值.传递消息的类型包括prepare，promise，propose，accept.在消息传递的过程中，不考虑消息遭到篡改的情况.

由图1的算法执行流程可知，proposer的工作流程如下：

图1 Paxos算法执行一次的流程

1)proposer发起一个编号N的提案，N全局唯一且单调递增.然后向多数派的acceptor发送包含N的prepare消息，多数派即超过acceptor数量的一半.消息还会携带发送者的ID以确定消息的来源，以下不再赘述.

Proposer→Acceptor：prepare(N)

2)proposer发送prepare消息后等待接收promise消息，用num1记下收到的消息数，记下收到的promise消息中编号最大的提案为Nmax.如果等待超时，proposer收到的promise消息数量不满足多数派，则提高提案编号N并重新发送prepare消息.如果proposer收到多数派的promise消息，则发送包含Nmax，V的propose消息给所有回复promise的acceptor.Nmax，V分别为收到的promise消息中编号最大提案的编号及对应的提案值，如果V为null，则由proposer自行设定(实验中令V等于proposer自身的ID).

Acceptor→Proposer：propose(Nmax，V)

3)由于Paxos算法中一个进程可以担任多种角色，为了减少模型的状态空间，实验中让proposer同时担任learner.因此，proposer等待接收accept消息，用num2记下收到的消息数.如果等待超时，proposer收到的accept消息数量不满足多数派，则提高提案编号N并重新发送prepare消息.如果proposer收到的accept消息满足多数派，则令voteEnd等于true，Value等于V，proposer进程结束.

定义proposer的结构体：

typedef ProposerMachine {

int ID，Value;

chan ch=[chanSize]of{mtype，int，int，int};

bool voteEnd=false;

};

其中ID为机器编号，Value为该机器的值，ch为消息信道，能够存储的消息量为chanSize，mtype为消息类型，voteEnd为结束标记.

算法中的事件则可用有限状态机的输入来表示，依据进程与事件之间的关系，可以得到状态和输入之间的转移关系.根据工作流程可得图2的proposer状态转移模型，其中!表示系统发送消息，而?表示系统接收消息.

图2 proposer状态转移模型

acceptor的工作流程如下：

1)当acceptor收到一个prepare消息后，检查消息中的N，若N大于ResN(初始为0)，则令ResN等于N，发送promise消息，消息包含AccN(初始为0)和AccV(初始为null).若N不大于ResN，则忽略该消息.

Acceptor→Proposer：promise(AccN，AccV)

2)当acceptor收到一个propose消息后，若消息中携带的编号N大于或等于ResN，则令AccN等于N，AccV等于V，并发送包含AccV的accept消息给propose以及learner.若N小于ResN，则忽略该消息.

Acceptor→Proposer，Learner：accept(AccV)

acceptor的结构体如下：

typedef AcceptorMachine {

int ID，ResN，AccN，AccV;

chan ch=[chanSize]of{mtype，int，int，int};

};

其中ID为机器编号，ResN为该机器收到的prepare消息的最高提案编号，AccN和AccV为该机器的收到的propose消息的编号最大的提案编号与提案值，ch为消息信道，可以存储的消息量为chanSize，mtype为消息类型.acceptor状态转移结构模型如图3所示.

图3 acceptor状态转移模型

3.2 验证属性的描述及其验证结果

由于需要就某个值达成一致的共识，分布式共识算法一般需要满足4个基本性质：有效性、一致性、完整性、可终止性.这4个性质可以总结为安全性和活性，安全性即有效性、一致性以及完整性，活性即可终止性.

首先定义全局变量，实验中proposer的数量为2，acceptor的数量为3，则多数派major的数量应为2，设置每个信道能够存储的最大消息量为4，初始轮次round为0.

定义实验状态及其含义如表1所示.

表1 实验状态

1)有效性的验证

有效性即进程只能选择已提出的值，其LTL表达式为：

validity {(true U(End0 && End1))→(true U [](Goal0 && Goal1))}

检测结果如下：

State-vector 596 byte，depth reached 9999，errors：0

2)一致性的验证

一致性即所有进程最终选择的值都相同，其LTL表达式为：

agreement{(trueU(End0 && End1))→(trueU[]Goal)}

检测结果如下：

State-vector 596 byte，depth reached 9999，errors：0

3)完整性的验证

完整即进程一旦选取了某个值，这个值就不会再改变.该性质可以转化了选取了某个值后就不会再次发起提案，其LTL表达式为：

integrity {(End0→[]End0)&&(End1→[]End1)}

检测结果如下：

State-vector 596 byte，depth reached 9999，errors：0

4)可终止性的验证

可终止性即系统中的所有进程最终都能够选择到某个值，其LTL表达式为：

termination{[](trueU(End0&& End1))}

检测结果如下：

State-vector 596 byte，depth reached 9999，errors：0

5)发生活锁可能性的验证

检测Paxos算法发生活锁可能性，即检测在有限的次数内Paxos算法是否能得到终止.假设发起提案的最大次数maxRound为50，LTL表达式为：

livelock{!((!End0&& !End1)Uround>maxRound)}

检测结果如下：

State-vector 596 byte，depth reached 3536，errors：1

检测表明算法并不能在限定的最大次数内结束.图4为检测器还原的算法不满足验证性质时的运行轨迹.

图4 发生活锁时的运行轨迹(部分)

由图4可知，Paxos算法运行过程中，当acceptor对一个提案A发送promise消息后，如果再接到另一个编号更高的提案B的prepare请求，将再次进行promise，此时，提案A的propose请求将被忽略，然后发送的提案A的proposer再次提高编号进行prepare请求，这样两个proposer会交替提高编号进行prepare请求，导致产生活锁.

4 改进Paxos算法以解决活锁问题

分布式系统应用一般需要连续确定多个值，由于Paxos算法有产生活锁的可能，直接使用会造成效率低下，因此在实际的应用中一般采用Multi-Paxos算法.

Multi-Paxos算法即使用一系列的Paxos算法实例来确定一系列的值.由于Paxos算法存在活锁问题的主要原因是各个进程可以公平地发起提案请求，导致各个进程可以交替地提高编号发起提案，于是Multi-Paxos算法通过选举leader的方式，让proposer提案请求发送给leader，然后leader充当原来proposer的职能执行Paxos算法.这样没有proposer竞争发起提案，因此可以解决活锁问题.

Multi-Paxos算法并没有详细说明如何进行选举，本文使用一种基于优先级的选举算法对Paxos进行类Multi-Paxos改进并重新进行验证.设置proposer使其拥有各自的优先级，在proposer发起提案请求之前，先向其他所有的proposer发送hello消息查找自己的leader，其他proposer收到hello消息后，回应ack消息，消息包含自己的优先级.当proposer收到ack消息后将优先级最大的proposer作为自己的leader，然后让leader代替自己发起提案.算法改进后的流程如图5所示.

图5 改进Paxos算法执行一次的流程(选举后)

算法改进后的proposer的工作流程如下：

1)proposer进程运行后将启动两个线程：listener与leader.

2)proposer准备发起请求.若此时没有确定leader，将向其他proposer的listener线程发送hello消息，收到ack消息后将最高优先级的proposer(可以为自身)作为leader.

Proposer→Listener：hello()

若已确定leader，则向leader发送request消息.

Proposer→Leader：request()

3)proposer等待接收accept消息，用num2记下收到的消息数.如果等待超时，proposer收到的accept消息数量不满足多数派，则认为leader状态不佳.重新确定leader后再次发送request消息.如果proposer收到的accept消息满足多数派，则表明提案被选定，令Value等于V，proposer进程结束.

listener的工作流程如下：

listener线程等待接收其他proposer的hello消息，收到消息后会回复带有proposer优先级的ack消息.

Listener→Proposer：ack(priority)

leader的工作流程如下：

1)leader线程等待接收到request消息，收到消息后发起一个编号N的提案，N为全局唯一且单调递增.然后向多数派的acceptor发送包含N的prepare消息.

Leader→Acceptor：prepare(N)

2)leader等待接收promise消息.收到promise消息后，用num1记下收到的消息数，记下收到的promise消息中编号最大的提案为Nmax.如果等待超时，leader收到的promise消息数量不满足多数派，则提高提案编号N并重新发送prepare消息.如果leader收到多数派的promise消息，则发送propose消息给所有回复promise的acceptor，消息包含Nmax，V及发起request消息的proposer的ID.Nmax，V分别为收到的promise消息中编号最大提案的编号及其对应的提案值，如果V为null，则由leader自行设定(实验中令V等于leader自身的ID).

Leader→Acceptor：propose(Nmax，V，IDproposer)

修改proposer的结构体如下：

typedef ProposerMachine {

int ID，Value，priority;

chan ch=[chanSize] of { mtype，int，int，int };

bool voteEnd=false;

};

图6为子线程listener与leader的状态转移模型.

图6 listener和leader状态转移模型

改进后proposer的状态转移模型如图7所示.

图7 改进后的proposer状态转移模型

acceptor的工作流程如下：

1)当acceptor收到一个prepare消息后，检查消息中的N，若N大于ResN(初始为0)，则令ResN等于N，发送promise消息，消息包含AccN(初始为0)和AccV(初始为null).若N不大于ResN，则忽略该消息.

Acceptor→Leader：promise(AccN，AccV)

2)当acceptor收到一个propose消息后，若消息中携带的编号N大于或等于ResN，则令AccN等于N，AccV等于V，并直接发送包含AccV的accept消息给发起request消息的proposer.若N小于ResN，则忽略该消息.

Acceptor→Proposer：accept(AccV)

改进后的acceptor状态转移模型基本没有变化.

设置proposer的优先级等于其ID值，重新将模型输入，检测Paxos算法发生活锁可能性.

检测结果如下：

State-vector 988 byte，depth reached 1049，errors：0

模型检测器没有发现错误，即没有发生活锁问题.

5 结 语

本文以Paxos算法作为研究对象，基于模型检测工具SPIN，对算法进行了形式化建模，并对该算法的安全性、活性、发生活锁可能性使用LTL语言进行了描述，经过分析验证，结果表明Paxos算法满足安全性和活性，但存在发生活锁的可能，并重现了活锁发生时模型的运行轨迹.为了解决Paxos算法发生的活锁问题，本文使用了一种为proposer添加优先级的类Multi-Paxos改进算法，通过选举leader的方式，让leader代替proposer提交提案.该方法优点是增加了算法的灵活性，可以指定不同proposer的优先级，在实际应用中，优先级可以根据相应的权重算法进行动态调整，从而实现proposer的负载均衡，经验证，当leader单一存在时，可以解决Paxos算法中发生的活锁现象.由于可能存在优先级相同及网络不佳等问题，可能会发生同时存在多leader情况，然而即便如此也能大幅降低可能发生的活锁现象，当所有proposer的优先级一样时，改进后的算法会退化为普通的paxos算法，即每个proposer成为自身的leader.

Paxos算法可以应用在许多场景中，由于Paxos算法的复杂性，对其进行形式化建模与验证后，可以使Paxos算法获得更高的可信度，以及更好地研究该算法在不同场景与范围中的应用情况.同时，Paxos存在很多变种算法，今后的工作可以以本文的Paxos算法模型为基础或参考，对Paxos的改进算法进行验证与分析.