Paxos Made EPR: Decidable Reasoning about Distributed Protocols
摘 要
一、基础知识:使用EPR的验证
1、一阶逻辑中的迁移系统
这里使用多类型一阶逻辑对迁移系统建模。我们使用的字母表Σ由带类型的常数,函数和关系符号组成。一个迁移系统就是一对(INIT, TR),其中INIT是初始状态,TR表示迁移关系。一个安全性性质可以由Σ上的公式P表示,如果一个系统的所有可达状态都满足P,那么这个系统就是安全的。Σ上的公式INV被称为证明迁移系统(INIT, TR)满足安全性性质P的归纳不变式,如果它满足:

2、EPR和Extended 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


