论文分享_08_09

Paxos Made EPR: Decidable Reasoning about Distributed Protocols

       本次分享的论文是发表于OOPSLA’17的Paxos Made EPR: Decidable Reasoning about Distributed Protocols，作者为来自以色列特拉维夫大学和美国UCLA的Oded Padon, Giuliano Losa, Mooly Sagiv和Sharon Shoham。

摘     要

    验证如Paxos的分布式协议是重要的，但在实际中也是困难的。检查这些协议的不变式通常是不可判定的，因为这需要对unbounded数量的节点和消息进行推理，而且协议的动作和不变式通常会包含不同量词和高阶逻辑概念，比如集合的势（元素数量）和算术等。这篇文章为了推进这些协议的自动验证，目标在于提出一种可以验证正确的协议且识别错误协议中的bug的技术。为此，作者提出了一种基于一阶逻辑的可判定片段EPR的演绎验证方法。该方法包括：用未解释的一阶逻辑对协议建模，系统性地转换该模型从而得到一个可以可判定地检查的模型和不变式。该转换的步骤都经过机器检查，保证了方法的可靠性。作者使用该方法对Paxos及多个Paxos的变种做了安全性验证。该工作是第一个对这些协议进行的可判定验证。

一、基础知识：使用EPR的验证

1、一阶逻辑中的迁移系统

        这里使用多类型一阶逻辑对迁移系统建模。我们使用的字母表Σ由带类型的常数，函数和关系符号组成。一个迁移系统就是一对（INIT, TR），其中INIT是初始状态，TR表示迁移关系。一个安全性性质可以由Σ上的公式P表示，如果一个系统的所有可达状态都满足P，那么这个系统就是安全的。Σ上的公式INV被称为证明迁移系统（INIT, TR）满足安全性性质P的归纳不变式，如果它满足：

2、EPR和Extended EPR

        EPR（Effectively Propositional Logic）是一阶逻辑的可判定片段，也被称为Bernays-Schönfinkel-Ramsey class，它是一类relational一阶逻辑公式，即字母表只包括常数和关系符号，没有函数符号，且满足量词前缀为∃∗∀∗的前束范式。EPR的可满足性问题是可判定的：NEXPTIME-complete。同时EPR满足有限模型性质，即其中的任一公式，要么是不可满足的，要么有一个有限的模型。由于EPR不允许函数出现，也不允许量词交替，因此我们需要对其进行扩展为分层（stratified）片段，即Extended EPR，其可判定性和有限模型性质都是保持的。分层公式的定义如下：如果一个公式的QA图是无环的，那么它可以称为是分层的。
后续文中的EPR都指的是Extended EPR。

二、演绎验证的方法

    这是使用EPR的验证方法的流程图，其中用户提供的输入用矩形表示，自动化程序用六边形表示，自动生成的输出用椭圆表示。

1、使用一阶逻辑建模

该验证方法的第一步需要用多类型未解释的一阶逻辑中迁移系统来描述协议。这一步涉及到抽象，因为通常协议中会使用一些不能直接用未解释的一阶逻辑表达的概念。

  • 将有解释的域公理化：如果需要描述一个有解释的域，如自然数，我们可以用一个类型来表达该域中的元素，用一个未解释的关系来表达有解释的关系（如二元关系≤）。一个很重要的例子就是在协议里使用自然数用于让某个集合的元素保持全序（比如序列号），那么我们可以直接定义二元关系≤，用全序的公理化（自反性，传递性，反对称性，完全性）来避免使用到自然数。
  • 通过一定的抽象来表达高阶逻辑：举例而言，协议中通常会涉及一些节点node和节点的集合nodeset，那么如果我们直接记node n∈ nodeset s，那么在对节点集合取量词的时候就会超出一阶逻辑。于是可以定义一个新的二元关系member(n:node, s:nodeset)，来表示元素与集合之间的属于关系。

2、使用派生的关系转换为 EPR

这个方法的第二步骤是将用一阶逻辑描述的模型转化为一个新的模型，并且得到一个归纳不变式使得验证状态（verification condition）都在EPR中，这样检查验证状态就是可判定的。这部分是需要手动完成的，但是按照这个步骤至少可以保证验证过程的可靠性（soundness）。其核心想法在于使用派生得到的关系来简化迁移系统中的迁移关系和相应的不变式。之前的流程图清晰地描述了整个转化过程，首先这一步的输入是已经用一阶逻辑建好的模型M=（INIT, TR）以及不变式INV，需要先做一个QA图，判断是否存在环，来决定是否要进入之后的转换步骤。具体来说，可以拆分为四个小步：

图片
  • 可靠性（Soundness）：以下定理总结了该方法的可靠性，如果用该方法得到的新模型和新不变式可以满足安全性性质p，那么原模型也满足p。
  • 不完备性（Incomleteness）：以上通过派生关系和重写等得到的是一个和原模型互模拟的迁移系统，但是对于EPR验证而言是不完备的。这种不完备性主要来源于：得到的新迁移系统可能是安全的，但是无法用EPR中的验证状态验证；过程中产生的重写条件可能无法在EPR中验证；一阶逻辑的表达能力不足等。

三、用EPR验证Paxos

       该文章中对Paxos及其多个变种（Multi-Paxos, Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos）进行了建模和EPR验证，这里指给出对Paxos验证的部分过程。在对Paxos用一阶逻辑进行建模后，作者检查发现其QA图发现是有环的，具体来说这个有向环来自于公理，不变式和assume命令中的三条公式：
        对QA图进行分析后可以发现，只需要去掉其中node-round和node-value两条有向边即可消除图中的有向环，于是可以找出需要替换掉的对应公式，并定义派生关系left_round和joined_round来描述并替换。
          按照步骤进行转换后，将新模型的验证状态，重写条件和辅助不变式用Z3检查，通过和semi-bounded verification比较的实验数据可以表明EPR验证方法在实际中也是效率很高的。
         附注：EPR的可满足性证明和复杂度分析可以参考Harry R. Lewis. 1980. Complexity results for classes of quantificational formulas. J. Comput. System Sci. 和Leonid Libkin的Elements of Finite Model Theory书中第14章1节。