随着大数据的普及, 分布式系统成为计算机科学十分热门的一个研究方向.分布式系统主要面临两方面的考验:在出现节点错误时, 分布式系统需要保证其可以正常地将错误节点切换到其他备用节点; 在某个节点进行数据更新时, 分布式系统需要保证其更新顺序可以被其他节点以相同的顺序复制, 以此来保证整个系统数据副本的一致性.为了解决分布式系统的这些问题, 人们提出了大量的分布式算法.然而, 它们的正确性常常被非形式化地证明.当算法变得复杂时, 非形式化的正确性证明就容易出错.一个证明如果能被严格验证, 就可以获得更高的可信度.

形式化方法是计算机科学的重要理论基础, 它以严格的数学化和机械化方法为基础, 对数学理论或者计算系统进行建模、规约和验证, 并以此解决和改善一系列数学方面或者软件安全性方面的问题.大量的工业实践表明:在开发复杂的硬件和软件系统时, 我们将更多的精力花在验证系统的正确性上, 而不是构建系统上.经过几十年的不断努力和发展, 形式化方法在验证越来越多的数学证明和新兴系统中发挥着越来越重要的作用.形式化验证大致有两类方法:模型检验和定理证明.模型检验对系统模型的状态空间进行了穷举, 以确定在执行所有状态之后是否满足目标结果.虽然模型检验有很多优势, 比如其检验过程基本上是自动化的以及如果存在不满足系统所需的属性时会给出一个反例等, 但是模型检验在随着待验证系统的规模越来越大时, 不可避免地会遇到状态爆炸问题, 以致于难以解决规模大的实际问题.另一方面, 定理证明的基本思想是将系统规范转化为数学理论, 然后通过生成中间证明步骤来构造定理证明, 或者反驳它.因为定理证明利用数学上的递归、归纳原理能够很好地解决系统模型过大的问题, 故其相对于模型检测有一定的优势.

在定理证明中, 会用到许多交互定理证明器, 也被称为辅助证明工具, Coq便是最受欢迎的定理证明工具之一.Coq实现了一种被称为Gallina语言的高级数学语言^[1], 该语言基于一种被称为归纳构造演算(CIC)的基础理论, 这个理论将高阶逻辑和多类型的函数式编程语言结合在一起, 用户对Coq中已证明定理的信心便来自于构造演算的性质.在推理和编程方面, Coq拥有强大的表达能力, 可以构造简单的项, 执行简单的证明, 学习复杂的算法, 直到建立完整的理论.Coq具有一个交互式的编译环境, 用户可以边证明、边调整、边修改, 使证明中的错误和不足及时得到改正和补充, 非常地友好.除了用于形式化地验证数学定理, 例如著名的四色定理^[2]外, Coq还成功地应用于确保系统的硬件和软件系统的可靠性, 包括乘法器电路^[3]、编译器^[4]、邮件服务协议^[5]和自稳定协议^[6]等.

本文将在辅助证明工具Coq中, 对分布式共识算法Basic Paxos进行形式化地建模与验证.分布式共识是分布式计算中的一个基本问题, 它要求一组进程在某些值上达成一致.当为了容错而复制分布式服务时, 共识是必不可少的, 因为非故障副本必须一致.不幸的是, 当进程或消息信道可能失败时, 很难达成共识.Paxos^[7]是Lamport为解决分布式共识而开发的一种重要算法, 已经在许多重要的分布式服务中使用, 例如Google Chubby^[8], Microsoft Autopilot^[9]以及WeChat PaxosStore^[10]等.Basic Paxos处理在没有共享内存的情况下并发运行的进程就单个值达成一致的问题, 在这种情况下, 进程可能崩溃, 稍后可能恢复, 消息可能会无限期丢失或延迟.在Basic Paxos中, 每个进程可能重复提出一些值, 并等待来自进程的适当子集的适当答复, 同时也适当答复其他进程; 如果足够多的进程没有错误, 可以对某些值进行投票, 最终达成共识.

自20世纪90年代末创建以来, 人们常常很难理解Paxos^[11].后来, Lamport针对Basic Paxos^[12]写了一个更简单的算法阶段的描述.许多工作已经花费在Paxos的形式化规范和验证上.比如:Lamport基于TLA+^[13]和TLAPS^[14]完成了对Simple Paxos的形式化规范和验证, 在此基础上, Chand等人完成了对Multi-Paxos的验证^[15], 他们运用动作时序逻辑, 将算法的规范和证明分别在不同的辅助工具中完成; Kellomaki采用模型检验的方法, 在PVS里将Simple Paxos算法抽象为状态、行为以及状态和行为之间的转移关系, 对其做了初步地规范和验证^[16]; Jaskelioff等人将DiskPaxos的基于TLA+的规范转换到Isabelle/HOL进行正确性验证^[17].近些年来, Padon等人^[18]使用一种自动验证分布式协议的EPR框架, 在这种框架中, 他们将算术运算、集合操作以及高阶逻辑全部抽象为一阶逻辑处理; 同时, 他们在算法抽象中改变了一些细节处理, 如算法的某些请求只是要求向大部分参与者发送, 但是他们要求向所有参与者发送等一些算法层面的改动.Garcia等人^[19]将算法抽象为基于多轮次的读/写的寄存器类抽象, 将整个算法区分为不同的模块, 基于Rely/Guarantee框架实现了模块化的验证.从总体方法学上讲, 本文和上述文献属于同一类工作, 依然是采用基于模型的形式化验证, 不是对Paxos算法在某个具体程序语言中的代码实现进行验证.与这些工作不同的是, 我们基于交互式定理证明工具Coq, 利用高阶逻辑和归纳构造演绎原理, 将Basic Paxos算法涉及的基础类型、数据结构和算法流程进行抽象, 以精确的数理定义形式给出其形式化定义, 整个建模过程没有对算法层面做任何更改; 同时, 整个建模和验证都在Coq里完成, 没有借助额外的辅助工具.我们对验证过程的信心完全基于Coq的归纳构造演绎原理, 没有引入其他的自定义逻辑和验证框架.此外, 与模型检验相比, 交互式定理证明的好处是:在算法验证中, 我们只要求参与投票的进程数量有限, 而不限制其具体大小.在Paxos的形式化建模与验证中, 主要解决了以下几个困难点.

(1)  用投票轮次的全序关系解决算法的时序复杂性.

Paxos是在非拜占庭的异步消息传递系统中解决分布式共识问题的算法.系统中的消息传递可能会延时、重复或者丢失, 但是不会被篡改, 所以以精确的时序去定义消息的发送与到达会非常困难.因此, 我们以消息不会被篡改的原则, 在每一轮消息的传递中增加一个投票轮次的信息来表示属于哪一轮投票, 投票轮次可以反映系统中消息的轮次前后关系, 以此来推进系统达成共识.

(2)  设置全局消息通道以解决发送和响应动作.

系统的所有参与者都可以有不同的执行速度, 并且可能宕机, 也可能重启.在这种情景中, 每个参与者随时可能发送、接收消息, 也随时可能发生故障, 所以如何去表征每个参与者在系统中是否处于正常状态也是困难的.但是如果一个参与者执行了发送动作, 系统中一定存在着对应这个动作的消息; 同时, 如果一个参与者对某条消息做出了响应, 一定可以说明它收到了对应的请求(如果没有做出响应, 并不能说明它没有收到请求, 因为它或者消息都可能遇到故障, 也可能它收到请求但是选择不参与投票).所以我们在系统中设置了一个全局的消息通道, 通过检查消息通道的内容, 就能知道是否发生了发送或者响应动作, 以及消息流程也能在此处反映.

(3)  消息类型的统一处理.

Paxos分为两大阶段, 每个阶段又分为两个子过程, 每个过程的请求和响应内容都是不一样的, 所以整个系统中主要存在4种消息类型.如果分别定义这4种消息类型, 后续的验证过程中将变得非常复杂, 所以我们借助Coq的强类型检查机制, 将这4种消息类型进行统一处理, 极大地简化了验证过程.

(4)  对最大投票的标记.

Paxos实际运用中涉及3个重要的前提条件, 其中涉及的最后一个特定值条件非常的复杂, 我们通过设置全局的PromiseMaxBal, AcceptedMaxBal和AcceptedMaxVal来标记每个参与者参与的最大投票, 简化了对于最大投票的复杂计算, 使得验证过程易读并且精确.

本文第1节介绍分布式共识与Paxos.第2节简单介绍Coq, 然后给出基于Coq的BasicPaxos算法的形式化建模与验证.第3节对文章进行总结以及对将来的工作方向进行展望.

1 分布式共识与Paxos

我们假设一个分布式系统中有一系列进程能够单独地提出待投票的值, 并且每个进程之间能够通过消息传递机制相互沟通.其中, 进程以任意速度运行, 可能因停止而失败, 并且可能重新启动; 消息传递可能需要任意长的时间, 可以复制, 也可以丢失, 但它们没有被损坏, 即不会发生拜占庭错误^[20].基本共识问题^[12], 称为单值共识, 是确保从进程提出的值中最多选择一个单值.达成共识的安全要求是:

   ●   只能选择已提出的值;

   ●   只有一个值被选择;

   ●   除非一个值真正地被选择, 进程才会去学习这个值.

我们暂不考虑共识问题的具体解决方案, 则可以给出安全要求的抽象定义如下:

$ \begin{array}{*{35}{l}} Consistency=\forall {{v}_{1}}, {{v}_{2}}\in \mathcal{V}:\varphi ({{v}_{1}})\wedge \varphi ({{v}_{2}})\Rightarrow {{v}_{1}}={{v}_{2}} \\ \end{array} $

(1)

其中, $\mathcal{V}$是所有已经被提出的值集合.给出一个值v, 当且仅当v是算法选中的值, 谓词ϕ为真.

Paxos解决了共识问题, 算法的两个主要角色由两种进程执行.

   ●   Proposer:这些进程提出被选择的特定值.集合$\mathcal{P}$表示所有此类进程的集合;

   ●   Acceptor:这些进程对被提出的值进行投票.当有足够的投票时, 这个特定值将被选择.集合$\mathcal{A}$表示所有此类角色的集合.

集合$\mathcal{Q}$表示集合$\mathcal{A}$幂集的子集, 即$\mathcal{Q}\subseteq {{2}^{\mathcal{A}}}$.它必须满足如下两个性质.

   ●   集合$\mathcal{Q}$的并集等于集合$\mathcal{A}$, 即$\bigcup\nolimits_{Q\in \mathcal{Q}}{Q}=\mathcal{A}$;

   ●   集合$\mathcal{Q}$的任意两个元素相交, 即∀Q₁, Q₂∈$\mathcal{Q}$:Q₁∩Q₂≠Ø

Basic Paxos解决了单一值的共识问题, 其对应谓词的定义为

$ \begin{array}{*{35}{l}} \phi (v)=\exists Q\in Q:\forall a\in Q:\exists n\in \mathcal{N}:sent(2b, n, v, a) \\ \end{array} $

(2)

其中, $\mathcal{N}$是提出协议编号的集合, 也称为Numbers; Q是一轮投票中所有Acceptors的集合, 称作议会系统; 集合$\mathcal{Q}$则为议会系统集合, 在下文有其详细的解释与性质说明.∃n∈$\mathcal{N}$:sent(“2b”, n, v, a)表示在投票轮次为n的投票中, 由Acceptora发出的一个消息, 其中消息类型为“2b”, 编号为b以及特定值为v.通过发送这种类型的消息, 代表着一个Acceptor进行了投票.

Basic Paxos算法的具体推导过程见文献[12], 这里只给出最终协议的大概流程.我们将Proposer和Acceptor的行为放在一起, 我们可以看到该算法在以下两个阶段中运行.

   ●   第1阶段:(a) Proposer选择一个编号N, 并向多数Acceptor发送一个编号N的Prepare请求; (b)如果Acceptor收到一个编号N并且N大于其已响应的任何Prepare请求的编号, 则Acceptor对该请求做出响应, 承诺不接受小于N的任何提案, 并以其接受的最大编号的提案(如有)的内容做出响应.

   ●   第2阶段:(a)如果Proposer收到多数Acceptor对其编号N的Prepare请求的响应, 则其向这些Acceptor发送一份编号为N、特定值为v的Acceptor请求, 其中, v是响应中编号最高的提案的特定值, 或是如果响应中没有任何信息则任意设置; (b)如果Acceptor收到编号N的Acceptor请求, 则其接受该提议并发送Accepted响应, 除非其已经对编号大于N的Prepare请求做出响应.

算法描述见表 1, 在经历若干轮次投票之后, 若存在一个议会系统的所有Acceptors发送Accepted请求, 整个系统就选出了的特定值, 所有进程可以开始获取并学习这个选举结果, 这个过程称为学习阶段, 并未在流程表中反映.

我们从流程中可以总结出Paxos的三大前提条件, 分别为编号条件、议会系统条件和特定值条件.

   ●   所有投票轮次的编号都不相同, 即编号条件;

   ●   所有投票轮次的议会系统交集不为空, 即议会系统条件;

   ●   每个投票轮次的特定值是组成其议会系统的所有参与者之前投票过的最大编号(最近)的投票轮次的特定值, 即特定值条件.

我们将在下面的章节形式化地建模Paxos, 包括抽象所有系统类型、系统行为以及三大前提条件, 并在此基础上验证Paxos的一致性.

2 基于Coq的形式化验证 2.1 Coq简介

在形式化研究领域, Coq是最受欢迎的交互式定理证明器之一^[21].它允许数学断言的表达式, 机械性地检查这些假设的证明, 帮助寻找形式化的证明, 并从构造性的证明中输出一个关于它的形式化规范的被证明有效的程序.Coq建立在归纳构建演算理论基础上, 可以概括为扩展了归纳和余归纳类型的λ演算, 以及一种描述数学定义和证明的语言^[1].两个方面实际上是相关的, 这要归功于著名的Curry-Howard De Bruijn同构, 它将命题映射到类型, 并将证明映射到函数化对象或强规范化程序.

我们用简单的对自然数的插入排序来说明一些概念.nat是最简单的归纳类型之一, 它有构造子O和S; nat有其自身的类型Set, 具体的数据结构如下.

Inductive nat: Type:=

   |O

   |S (n: nat).

nat的定义描述了集合nat中的表达式是如何构造的:O和S是构造子; 表达式O属于集合nat; 如果n是属于集合nat的表达式, 那么S n也是属于集合nat的表达式; 并且只有按照这两种方式构造的表达式才属于集合nat.接下来, 我们可以定义在参数类型为nat集合上的递归函数式程序.

Fixpoint insert (i: nat) (l: list nat):=

   match l with

   |nil⇒i::nil

   |h::t⇒if i≤? h

      then i::h::t else h::insert i t

   end

Fixpoint sort (l: list nat):=

   match l with

   |nil⇒nil

   |h::t⇒insert h (sort t)

   end

其中, i是nat类型的参数; l是list类型的参数, 表示的是自然数列表; insert函数是把i插入到l的合适位置中; sort函数是递归地对列表里的每一项进行insert.很显然, sort函数实现了对l的排序, 但是如何去证明经过sort函数作用之后l确实是有序的, 即我们要证明如下引理:

$ Lemmasort\_sorted:forall\text{ }l, sorted(sort\text{ }l). $

其中, sorted是我们要规范说明的有序概念, 也可称作谓词.我们要证明sort算法是正确的, 也就是要证明对于任意一个列表l, 对它进行sort后产生的列表是有序的.我们定义一下有序的概念.

Inductive sorted: list nat→Prop:=

   |sorted_nil:sorted nil

   |sorted_one:forall x, sorted (x::nil)

   |sorted_cons:forall x y l,

      x≤y→sorted (y::l)→sorted (x::y::l).

这种归纳定义的命题在Coq中很常见, 并且非常容易理解.上述简单的例子说明了Coq类型理论的一些重要特征.Coq为用户提供了用这些类型、具体对象以及基于这些对象的函数来精确描述数学定义, 然后以交互的方式进行证明.总之, Coq的特性允许我们在一个类型化的、精确的环境中形式化数学理论, 而且这种定义基本上是构造性的, 这种定义能够为证明提供更多的信息, 所以大多数Coq用户尽可能地不使用排中律.

2.2 准备工作

通过第1节对Basic Paxos算法的描述, 我们清楚地知道了算法的流程.为了便于形式化的建模以及证明, 我们需要将算法进行抽象.明显地, Paxos算法是一个基于消息传递机制的选举共识算法, 系统进程即算法参与者在每一轮次的投票环节分别对特定值进行投票.我们知道, 整个算法主要包括3个基础类型:参与者、轮次编号、被投票的特定值.依据文献[7], 参与者与被投票的特定值只需要可以进行区别即可; 轮次编号之间必须不同且可以比较大小, 即能够满足唯一性和全序性.为了简化建模过程, 并考虑到我们经常使用的自然数完美地满足这两个性质, 所以对于这3个类型, 我们都可以用自然数定义以满足Paxos的实际情况需求.因此, 我们将参与者、轮次编号、被投票的特定值分别定义为3个类型:priest、number、decree, 具体的形式化定义如下.

Inductive priest: Type:=

   |priestId:nat→priest.

Inductive decree: Type:=

   |decreeId:nat→decree.

Inductive number: Type:=

   |numberId:nat→number.

Definition blt_number (x1 x2: number):=

   match x1, x2 with

   |numberId n1, numberId n2⇒ltb n1 n2

   end

通过第1节对算法的描述, 我们涉及到了许多属于和包含的概念, 所以在建模的过程中, 不可避免地要处理有关有限集合的问题.我们在Coq标准库的基础上, 对有限集合的一些定义以及引理做了一些补充.因为算法中有关集合的处理都是对于priest的操作, 所以我们接下来应该都不考虑多态性, 直接以类型priest进行定义.

首先, 因为算法的前提条件中涉及到对于空集的描述, 所以我们必须在标准库的基础上对空集及其性质进行定义并证明, 例如定义了空集不包含任何元素的引理及其两个推论.然后, 我们定义了集合之间的包含subset与真包含sincl关系, 并且对这两种关系之间的性质做了一些证明.具体的形式化定义如下.

Lemma empty_spec: forall x, ~(set_In x (empty_set priest)).

Lemma empty_spec_iff: forall x, set_In x (empty_set priest)↔False.

Lemma empty_spec_mem: forall Q, (exists x, set_mem Aeq_dec x Q=true)→

   Q < > empty_set priest.

Lemma double_inclusion: forall u v, subset u v→subset v u→u=v.

2.3 投票行为和消息抽象

在每一轮的投票中, 参与者都是对这轮投票的唯一特定值进行投票, 并且选择投票或者放弃.为了将这一过程的所有信息集中在一起便于分析与证明, 我们在Coq中运用Record方法将一轮投票抽象为一个Ballot类型, 其包括dec, qrm, vot以及bal这4个信息, 分别表示此轮投票特定值、议会系统、最终投票者以及轮次编号.举个例子, 第8轮为特定值v投票, 共有参与者PA, PB, PC, 其中PC不投, PA和PB投票了, 则这一轮投票Ballot的编号bal为8, 特定值dec为v, 参与者qrm为集合[PA, PB, PC], 投票者vot为集合[PA, PB].

Record Ballot: Type:=mkBallot

{

   dec: decree;

   qrm: set priest;

   vot: set priest;

   bal: number;

}.

同时, 在Paxos算法中, 所有的信息都是以消息的形式在各个参与者之间进行传递, 所以对消息的抽象是十分重要的.通过分析第1节的表 1, 很明显地知道整个算法分为两大阶段, 每一次请求或者响应都是一次消息传递:第1阶段(a)的Prepare请求中包含了轮次编号; 第1阶段(b)的Promise响应中包含了轮次编号、参与者以及其已经参与过的最大轮次编号和特定值; 第2阶段(a)的Accept请求包含了轮次编号以及此次投票选出来的特定值; 第2阶段(b)的Accepted响应包含了响应者响应的轮次编号以及特定值.为了便于建模之后的分析, 我们利用Coq系统的强类型特征, 将4个消息全部定义为类型Message, 若某一阶段的消息不包含某一项, 设为缺省默认值即可, 具体的如下所注释.在之后的定义和证明中, 因为Coq的类型检查, 不会带来混乱.

Record Message: Type:=mkMessage

{

   typeM: nat; (*消息的类型.我们以1~4分别代表 4个小阶段的4种消息.*)

   balM: number; (*消息的轮次.*)

   maxBalM: number; (*消息的轮次.只有2-类型消息有此项.*)

   maxValM: decree; (*消息的特定值.2-类型表示其曾经参与的最大特定值, 3-类型和4-类型表示现阶段进行投票的特定值, 1-类型没有此项.*)

   accM: priest; (*消息的发送者.2-类型和4-类型的消息表示发送者身份, 1-类型和3-类型消息没有此项.*)

}.

2.4 系统状态和三大前提条件抽象

我们将可供所有的投票轮次选择的轮次编号、特定值分别定义为Numbers, Values.另外, 在整个系统初始状态时还没有任何投票轮次发生, 我们定义一个特殊的特定值None, 来满足表 1中Promise响应内容为null的要求.同时, 我们定义系统中所有的投票轮次为aBallots, 因为Paxos采用的是非拜占庭的故障模型, 所以所有存在的投票轮次的信息都是正确的.显然地, 系统中所有的参与者组成了集合Acceptors(文献[12]中还存在Client和Leaner角色, 但是对于算法验证不重要, 我们在这里省略其建模), 每一轮次投票的议会系统Quorum都是Acceptors一个子集, 而且必须满足议会系统条件; 所有轮次的议会系统组成了集合Quorums.具体的形式化定义如下.

Variables Numbers: list number.

Variables Acceptors: set priest.

Variables Values: set decree.

Variables None: decree.

Variables aBallots: set Ballot.

Variables Quorums: set (set priest).

对于编号条件, 我们将其形式化定义为Unique_Ballot, 显然地, 其说明系统中任何两个投票轮次的投票编号相等则其一定为相同的投票轮次, 反之亦成立.BasicPaxos算法另外一个非常重要的定义就是Quorum, 它表示在一轮投票中, 所有参与者的集合即priest集合, 而且其必须满足议会系统性质.简而言之, 就是每个Quorum集合的元素个数必须是Acceptors集合的元素个数的半数以上, 并且两个不同的Quorum集合之间必须有交集.这就是Paxos算法为了满足容错性而进行的规定, 具体的数学定义在第1节给出过.我们将所有Quorum集合组成的集合定义为Quorums, 我们规定在每一轮次的投票中, 所有参与者组成的集合都是Quorums的一个元素, 故其一定满足Paxos对于大多数参与者的要求.我们将其定义为QuorumsAssumption, 即系统中的任意两个议会系统的交集不为空.具体的形式化定义如下.

Hypothesis Unique_Ballot: forall x y: Ballot,

   In x aBallots→In y aBallots→x=y↔(bal x)=(bal y).

Hypothesis eq_dec_Ballot: forall x y: Ballot,

   {(bal x)=(bal y)}+{blt_number (bal x) (bal y)=true}.

Hypothesis QuorumsAssumption: forall Q1 Q2: set priest,

   In Q1 Quorums∧In Q2 Quorums→exists q,

      set_In q (set_inter priest_eq_dec Q1 Q2).

通过仔细分析特定值条件, 我们发现其表述的此轮投票轮次之前的所有投票轮次的相关信息.如果通过定义函数得到过往投票轮次的相关信息, 整个建模和验证将变得非常麻烦和困难.所以, 我们考虑在算法流程中实时地更新记录每个参与者的相关过往投票信息——PromisePromiseMaxBal, AcceptedPromiseMaxBal和AcceptedMaxVal这3个字段值的更新, 其中, PromisePromiseMaxBal表示的是某个参与者参与过的最大的投票轮次, 注意到Promise子过程也算作参与了, 所以其会在Promise阶段和Accepted阶段都更新; AcceptedPromiseMaxBal和AcceptedMaxVal可以当作一个整体, 表示某个参与者在某个投票轮次中进行了投票, 其中, AcceptedPromiseMaxBal, AcceptedMaxVal分别表示这个投票轮次的编号和特定值, 只会在Accepted阶段更新.具体的形式化定义如下:

Variables PromisePromiseMaxBal: priest→number.

Variables AcceptedPromiseMaxBal: priest→number.

Variables AcceptedMaxVal: priest→decree.

最后, 我们需要强调的是:Basic Paxos采用的是非拜占庭的故障模型, 即进程以任意速度运行, 可能因停止而失败, 并且可能重新启动; 消息传递可能需要任意长的时间, 可以复制, 也可以丢失, 但它们没有被损坏.所以, 上述定义过的系统状态相关的值, 只要存在, 则其所包含的信息一定是正确的.考虑到这个系统性质, 我们设置了一个全局消息通道来解决并简化发送响应动作的形式化定义.因为系统会发生故障, 所以如何去表征每个参与者在系统中是否处于正常状态也是困难的, 也就很难形式化地定义执行发送响应时参与者应该处于何种状态.但是, 如果一个参与者执行了发送动作, 系统中一定存在着对应这个动作的消息; 同时, 如果一个参与者对某条消息做出了响应, 一定可以说明它收到了对应的请求(如果没有做出响应, 并不能说明它没有收到请求, 因为它或者消息都可能遇到故障, 也可能它收到请求但是选择不参与投票).所以, 通过对全局消息通道的内容进行检查, 可以确定每个参与者在系统中是否执行了发送动作, 以及如果执行了发送动作, 我们也能确定其发送的内容.因此, 形式化定义(2)时, 我们通过检查全局消息通道来定义, 从而不考虑发送动作并简化之后的证明.全局消息通道的形式化定义如下.

Variables msgsChannel: set Message.

2.5 Paxos实例

在准备工作和投票行为建模完成之后, 我们以文献[7]中的一个具体的算法例子来说明Paxos的实际情况和形式化定义之间的一致性.如表 2所示, 系统中包含5个参与者A, B, C, D和E, 并且一共进行了5个轮次的投票, 其中, quorum即议会系统是每个轮次中实际的参与者, 红色标记的是投票了的参与者, voters是quorum的子集.显然地, 5个投票轮次的编号都不一样, 并且议会系统都包含大多数的参与者, 保证其交集不会为空, 所以编号条件和议会系统条件都是满足的.接下来, 我们来具体地分析如何满足特定值条件.

   ●   编号2是最早的投票轮次, 所以其特定值条件是平凡的, 即可以为任何值.

   ●   编号5的投票轮次, 其议会系统中的参与者没有在之前的投票轮次中投过票, 故其特定值也是平凡的.

   ●   编号14的投票轮次, 只有参与者D在编号2的投票轮次中投过票, 所以已经特定值条件, 编号14的投票轮次的特定值与编号2的投票轮次的特定值相等.

   ●   编号27的投票轮次, 其议会系统中的参与者A没有在之前投过票, 参与者C只在编号5的投票轮次中投过票, 参与者D只在编号2的投票轮次中投过票, 所以最大的是编号5的投票轮次, 依据特定值条件, 编号27的投票轮次与编号5的投票轮次的特定值相等.

   ●   编号29的投票轮次, 其议会系统中的参与者B只在编号14的投票轮次中投过票, 参与者C在编号5和编号27的投票轮次中投过票, 参与者D在编号2和编号27的投票轮次投过票, 所以最大的是编号27的投票轮次, 依据特定值条件, 编号29的投票轮次与编号27的投票轮次特定值相等.

所以经过投票行为和消息抽象之后, 我们确保了Paxos的实际情况与形式化定义的一致性.例如, 编号29的投票轮次可以抽象为一个Ballot, 其中, bal为29, qrm为B, C, D组成的参与者集合, vot为B组成的参与者集合; 在这一轮投票中, 每个参与者会在系统中产生对应的消息, 包含消息的类型, 此次消息对应的投票轮次, 最大投票轮次的编号和特定值信息以及参与者信息, 这些消息内容与形式化定义的Message是一一对应的; 最后, 我们通过系统中的消息内容, 可以确定编号29的投票轮次的特定值decree为β.

2.6 算法建模

在前面的工作中, 我们对算法涉及的基础类型、投票轮次、消息机制以及三大前提条件进行了形式化的抽象和定义, 我们将在此基础上, 对系统如何选定一个特定值即公式(2)以及消息流程进行形式化定义.

首先, 我们要精确地定义一个特定值在满足特定条件时才表示其被选择了.为了说明这一个过程, 我们将其拆解为3个定义.在对全局消息通道介绍的时候, 我们已经说明了可以通过形式化定义对全局消息通道的检查来代替形式化定义sent动作.通过对消息流程的分析, 一个参与者priest对一个特定值投票是发生在Accepted响应中, 所以在全局消息通道中, 必然存在一个消息类型为4的消息, 并且表明它对这一轮次投票的特定值投票了, VotedForIn就是对这一行为结果的形式化定义.

Inductive VotedForIn: priest→decree→number→Prop:=

   |cons_VotedForIn:forall a v b, In a Acceptors→In v Values→In b Numbers→

      (exists m, In m msgsChannel∧(typeM m)=4

         ∧(balM m)=b

         ∧(maxValM m)=v

         ∧(accM m)=a)→VotedForIn a v b.

VotedForIn只是说明了一个参与者投票了, 如果某一轮次的所有参与者都投票了, 则代表这是一次成功的投票, 是一个成功投票轮次的性质说明.如果在所有轮次的投票中, 存在一轮成功的投票, 则表示这一轮成功的投票的特定值被选择了, 这是系统真实存在这样一个成功投票轮次的说明.

Inductive SuccessfulIn: decree→number→Prop:=

   |cons_SuccessfulIn:forall v b, In v Values→In b Numbers→

      (exists Q, In Q Quorums→

         forall a, set_In a Q→VotedForIn a v b)→SuccessfulIn v b.

Inductive Chosen: decree→Prop:=

   |cons_Chosen:forall v, In v Values→

      (exists b, In b Numbers→SuccessfulIn v b)→Chosen v.

SuccessfulIn表示的是“成功的投票”这一性质, 即一次投票的全部参与者都对这一轮的特定值投票了. Chosen表示的是“成功的投票”这一性质的存在性, 即存在一轮投票, 其投票轮次为b, 满足这个性质.很显然地, 这3个重要的归纳定义是对公式(2)的拆分定义.而且根据系统消息的不可篡改性质, 全局消息通道中的消息内容一定是所有参与者发送的, 所以其保证了系统中最后选择的特定值一定是系统参与者发送的, 即满足共识性安全要求中的“只能选择已提出的值”.

在这里, 我们需要进一步分析从一次投票行为Ballot可以得到的结论.显然地, 任意一次投票行为Ballot的qrm集合和vot集合都是Acceptors集合的子集, 而且vot集合也是qrm集合的子集.同时, 根据vot集合的定义, 它包含的所有参与者都在一轮投票行为中投票, 所以在系统消息中, 一定存在一条对应其投票行为的4-类型消息.系统中任意两个不同的投票行为Ballot的bal是不同的, 并且bal, dec分别是Number, Value的元素.这些平凡性质不属于附加前提, 都可以将其形式化定义, 并且在证明中是可以直接引用的, 用来说明存在性和合理性, 我们将其形式化定义为trivial, 因为比较简单, 我们不在论文中列出.

另外, 我们在前面提到过, 对于所有参与者其只能选择投票或者不投票, 我们定义参与者没有在某一轮次投票, 即VotedForIn的否定形式, 并且以后也不会在这一轮次投票, 即其PromiseMaxBal一定是大于这个投票轮次的轮次编号的, 我们将此性质形式化定义为WontVoteIn.同时, 如果某一投票轮次进行到Accept阶段, 对于这个投票轮次有一个安全状态, 即在这一轮次编号为N的投票过程中, 对于特定值V是安全的表示在任何轮次编号小于N的投票轮次中, 除了V以外, 没有别的特定值被选择, 或者永远不会被选择.这个定义其实就是对系统中所有priest行为的一个规范, 我们将此性质形式化定义为SafeAt.WontVoteIn和SafeAt具体定义如下.

Inductive WontVoteIn: priest→number→Prop:=

   | cons_WontVoteIn:forall a b, In a Acceptors→In b Numbers→

         (forall v, In v Values→~VotedForIn a v b)

      ∧blt_number b (PromiseMaxBal a)=true→WontVoteIn a b.

Inductive SafeAt: decree→number→Prop:=

   | cons_SafeAt:forall v b, In v Values→In b Numbers→

      (forall c, In c Numbers→blt_number c b=true→

      ((exists Q,

      (forall ballot, trivial ballot→In ballot aBallots→(c=(bal ballot))→

      Q=(qrm ballot)∧(forall a, In a Q→VotedForIn a v c∨WontVoteIn a c)

      ))))→SafeAt v b.

通过第1节对Paxos的介绍, 我们知道算法一共分为两大阶段, 每个阶段细分为两个子过程.同时, Paxos是一个基于消息传递机制的选举共识算法, 涉及到消息的发送与接收.但是我们可以通过检查整个系统中存在的消息, 去判断是否发生的消息的传递.例如, 如果消息通道中存在一个1-类型的消息, 我们一定可以推断出系统中某个参与者发出了Prepare请求; 同时, 因为系统中可能存在各种延时、宕机等, 有些参与者是无法收到消息或者发送消息的, 所以我们无法去良好地定义接收行为.但是我们可以依据消息通道中是否存在2-类型的消息去判断一个参与者对一轮投票进行参与, 因为只有在参与者接收到Prepare请求时才会发送Promise请求; 类似地, 我们也可以根据全局消息通道中是否存在4-类型的消息去判断一个参与者是否对某一轮次投票的特定值进行了投票, 因为参与者只有收到Accept请求之后才会发送Accepted响应.通过这个全局消息机制, 我们解决了形式化定义消息发送与接收的困难点, 不用去复杂地定义系统客观存在的故障和异常, 还成功地体现了Paxos实际运用中会遇到的各种消息问题, 并且保证了形式化定义的合理性和准确性, 所以这个形式化定义更加形式化和构造性.我们根据算法描述定义系统中的所有消息性质, 我们先给出其归纳定义然后进行说明.

Inductive MsgInv: Prop:=

   |cons_MsgInv: (forall m, In m msgsChannel→

      ((typeM m)=1→True)

   ∧((typeM m)=2→less_or_equal_number (balM m) (PromiseMaxBal (accM m))

         ∧(In (maxValM m) Values∧In (maxVBalM m) Numbers

               ∧VotedForIn m (accM m) (maxValM m) (maxVBalM m)

       ∨((maxValM m)=None∧(maxVBalM m)=numberId 0)))

∧((typeM m)=3→(SafeAt m (maxValM m) (balM m)

         ∧forall ma, set_In ma msgsChannel→(typeM m)=3→

               (balM m)=(balM ma)→(maxValM ma)=(maxValM m)))

∧((typeM m)=4→(less_or_equal_number (balM m) (maxVBal (accM m))

         ∧forall ma, set_In ma msgsChannel→(typeM ma)=3

            ∧(balM ma)=(balM m)

            ∧(maxValM ma)=(maxValM m))))→MsgInv.

通过观察上面对MsgInv的归纳定义, 很明显地看出我们是根据消息类型对其进行归纳定义, 所有在全局通道中的消息行为都必须满足MsgInv规范.因为1-类型消息是每个轮次的发起阶段, 系统中的每个参与者都可以随时发起Prepare请求, 请求的轮次编号可以是任意的number类型值, 故系统中的所有1-类型的消息都是合理的.某个参与者发出了2-类型的消息, 则其必须满足此轮次投票的编号大于其曾经参与过的投票的最大轮次编号, 并且发送最大轮次编号及其特定值, 若没有则发送默认值, 即特定值为None, 编号为0的默认消息; 如果不满足2-类型的消息发送要求, 则全局消息通道中一定不会出现对应的2-类型消息.若发出了3-类型的消息, 则其处于一种安全状态, 并且对于整个系统中所有3-类型的消息, 如果其编号相等, 则消息里的特定值一定是相同的, 因为根据编号条件, 相同编号的投票轮次一定是同一个投票轮次, 故其特定值一定是相同的.若某个参与者发出了4-类型的消息, 则这个消息发送者的最大特定值不小于此消息的特定值, 并且在系统所有的消息中, 一定存在3-类型的消息, 并且与此消息的轮次编号和特定值相同, 因为4-类型消息是对3-类型消息的响应, 参与者不可能主动发送4-类型消息.

通过上面的分析, 我们确保并坚信对Paxos的形式化建模与Paxos的实际情况之间的一致性.我们要证明Paxos的一致性, 就需要在上述形式化建模的基础上验证公式(1)的正确性.

2.7 算法验证

在这一节, 我们将在前面建模的结果中, 描述一些对一致性定理比较重要的引理及一致性定理的证明.

首先, 我们从消息传递的角度来看待算法, 在系统中的任意两个参与者, 分别发送了两条消息, 其中一条消息表示其中一个参与者为轮次编号b的特定值v1投票, 另一条消息表示另一个参与者同样为相同轮次编号的特定值v2投票了, 根据MsgInv和VotedForIn的定义, 我们可以推断出这两个特定值v1和v2是相等的, 我们将此性质形式化定义为引理VotedOnce.我们描述这个推论过程:根据VotedForIn的定义, 我们知道在系统的消息中存在着两条4-类型消息, 又根据MsgInv的定义, 存在4-类型的消息则系统中一定存在着对应的3-类型消息, 并且对于所有的3-类型消息, 如果轮次编号相同, 则消息相同即消息包含的特定值是相同的.其实通过对Ballot的定义, 我们能够更简单地意识到这个问题:根据编号条件, 任意两个投票行为Ballot的投票轮次bal是唯一的, 所以如果两个参与者的轮次编号一致, 则代表他们肯定是在同一轮进行的投票, 同一轮的特定值肯定是相同的.通过上面的推论分析, 我们也能够很快地以同样的方式可以推断得到引理VotedInv.

Lemma VotedOnce: forall a1 a2 b v1 v2,

   MsgInv→In a1 Acceptors→In a2 Acceptors→

   In b Numbers→In v1 Values→In v2 Values→

   VotedForIn a1 v1 b∧VotedForIn a2 v2 b→(v1=v2).

Lemma VotedInv: forall a v b,

   MsgInv→In a Acceptors∧In v Values∧In b Numbers

   →VotedForIn a v b→less_or_equal_number b (AcceptedMaxBal a)∧SafeAt v b.

介绍完两个最重要的引理之后, 我们来定义一致性定理Consistent:对于系统中的任意两个轮次的投票行为Ballot, 我们最直接地能够看到每个Ballot的各个组成部分的内容, 如果Ballot所属的议会系统qrm是vot的子集(更直观地说, qrm集合和vot集合是相等的), 可以推论出qrm的所有参与者都参与了投票, 即满足第1节公式(2)的定义, 这轮的投票行为都成功地选择了一个特定值, 所以这个条件与公式(2)是等价的, 我们将这种性质定义为引理SuccToChosen, 具体的形式化定义如下.为了与投票行为的抽象保持一致, 我们将公式(1)中的抽象定义具体定义为一致性定理Consistent.如果两个Ballot所属的qrm都是vot的子集, 即这两轮的投票行为都成功地选择了一个特定值, 则这两个轮次的特定值是相等的.对于一致性定理, 我们可以将其以两个Ballot是否是同一个投票行为为依据分为两个引理进行证明, 两个引理分别为ConsistentOfEqual和ConsistentOfNotEqual.对于引理ConsistentOfEqual的证明很容易, 因为两轮次投票行为的编号是相同的, 根据前面的分析, 能够确定就是同一轮投票, 故其特定值一定是相等的.接下来给出投票轮次不相等证明的大概思路.

Lemma SuccToChosen: forall b a,

   trivial b→set_In b aBallots→set_In a (qrm b)→subset (qrm b) (vot b)→

   Chosen (dec b).

Lemma ConsistentOfEqual: forall b1 b2, trivial b1→trivial b2→

   subset (qrm b1) (vot b1)→subset (qrm b2) (vot b2)→

   (bal b1)=(bal b2)→(dec b1)=(dec b2).

Lemma ConsistentOfNotEqual: forall b1 b2, MsgInv→trivial b1→trivial b2→

   subset (qrm b1) (vot b1)→subset (qrm b2) (vot b2)→

   blt_number (bal b1) (bal b2)=true→(dec b1)=(dec b2).

Theorem Consistent: forall b1 b2, MsgInv→trivial b1→trivial b2→

   subset (qrm b1) (vot b1)→subset (qrm b2) (vot b2)→

   (dec b1)=(dec b2).

对于定理前提谓语条件即系统中所有成功的投票轮次, 其议会系统都是投票者的子集, 又依据投票轮次的平凡性质比如其投票的人一定是议会系统的子集, 根据集合性质, 很容易知道成功投票轮次的议会系统和投票者其实是相等的, 即所有参与者在这一轮次投票行为中全部投票了, 这也很符合SuccessfulIn的定义.根据这个议会系统全部投票了的推论进而能得出很多结论.比如, 我们可以确定很多存在性, 即在系统中, 成功的投票轮次都满足Chosen的规范, 以及在所有的消息中, 肯定也存在成功轮次相关4-类型的VotedForIn消息等.在这些初步的推论中, 结合上述的VotedForIn引理, 就能够推论出SafeAt规范.仔细分析SafeAt规范, 我们发现其涉及到两个投票轮次之间编号的大小比较, 所以由此我们很容易确认将一致性定理分为两部分进行证明的思路是正确的.同时, 根据SafeAt和VotedForIn得到的相关结果进行分析, 结合我们已经证明过的引理VotedOnce, 就能够得到两轮成功投票行为的特定值是一致的.最后, 根据投票行为的平凡性质, 我们就能通过这两个引理最终得到一致性定理证明的完整过程.我们需要强调的是:所有的平凡性质虽然简单但都是必须的, 它反映了Paxos非拜占庭故障模型一系列的基础规范, 比如轮次编号和特定值都是类型准确的、投票消息一定会在全局消息通道中真实反映等.

通过上述的规范的数学定义之后, 我们对BasicPaxos算法所涉及的类型、消息通道以及性质有了一个完整并且严格的形式化定义, 并且最终成功地证明了算法的一致性定理, 即在整个系统中, 两轮成功投票的值一定是相等的.

3 总结

在整个建模和验证过程中, 我们在Coq中用1 092行代码一共证明了13个重要引理以及最终的共识性定理, 完整的Coq脚本可以在https://github.com/Liyanan0410/BPOfCoq中查看并使用.通过对Basic Paxos算法的建模与验证, 我们进一步理解了分布式共识问题, 以及确信Paxos算法能够解决问题并且是正确的.通过这次研究, 我们确定并坚信在分布式领域, 运用形式化方法是能够取得进步的.将来我们还可以对算法模型进一步优化, 以及增加一些特定的符号说明来改善证明的可阅读性.同时, 因为Paxos算法具有很多的变种^{[22, 23]}, 我们将进一步地对这些算法变种进行研究, 对整个Paxos算法家族做一个整体地建模与验证, 以增强算法在实际应用中的信心.