论文分享06_01

       本周我们分享一篇发表于PLDI’18上的关于利用模块化保持演绎验证的可判定性及其在验证分布式系统的应用的文章:Modularity for Decidability of Deductive Verification with Applications to Distributed Systems,文章一作是以色列特拉维夫大学的Marcelo Taube。

       验证复杂系统是一项长期的研究课题,近年来在验证编译器,操作系统和分布式系统方面有一系列成功的案例。目前这个方向主要有两种方法,一是交互式的定理证明,如Coq和Isabelle/HOL,二是基于自动定理证明器的演绎验证。证明自动化可以显着提高复杂系统形式验证的生产力,然而,自动定理证明器在处理量化公式时的不可预测性成为了这些工具可用性的主要障碍。为了解决这一难题,本文作者没有对证明器进行改进,而是使用了一种模块化的证明方式,它能够生成可判定的验证条件(Verification Conditions,VC)。可判定性可以极大地提高自动化证明的可预测性,从而使验证方法更加实际可行。作者使用该方法验证了多个分布式协议的实现,展示了该方法的有效性。

在这篇文章中,作者提出的新验证方法可判定分解(Decidable Decomposition),其核心思想是以模块化方式构建正确性证明,从而可以使用一阶逻辑的可判定片段来证明每个组件。重要的是,每个组件的验证条件可以使用不同的可判定片段(fragment)。例如,这允许一个组件使用算术(arithmetic),而另一个组件使用分层量词(stratified quantifier)和未解释的关系(uninterpreted relation)。它还允许每个组件使用自己的量词分层,即使组合不会分层。重要的是,即使全局验证条件不在于任何单个可判定片段中(例如,算术、未解释关系和量词的组合是不可判定的),也可以应用可判定分解。本工作中主要使用的两种一阶逻辑的可判定片段为EPR(Effectively Propositional Logic)和FAU(Finite Almost Uninterpreted Fragment),作者团队有数篇关于这两个片段的前期工作。

很多分布式协议中都有领导人选举部分,这里我们用一个简单的领导人选举流程为例介绍可判定分解是如何进行的。首先我们声明三个类型,包含了候选人和投票人的类型Citizen,集合类型Set,以及用于计算票数的自然数类型int。其次,我们用两个映射表示状态,分别是从Citizen到Set的映射voter和用Citizen到Boolean的映射lead,voter表示投票给该候选人的人的集合,而lead表示该候选人是否是领导人。我们设定得票超过半数的候选人被选为领导人,那么这个选举流程可以记作:

这里我们用requires标记precondition,vote_once指的是每个Citizen只能投一次票,good_count指的是成为领导人的Citizen得票数超过半数;用ensures标记postcondition,single_leader指的是至多只能有一个领导人;而用括号标记的部分是实现的伪代码,也是我们需要用可判定分解的部分。

伪代码中计算票数部分需要引入算术,而算术会导致不可判定,因此我们可以把算术放在一个新的模块Sets中,并提供两个对Main模块可见的映射isquorum和common_member以及一个性质intersect。实际上,我们在计算票数的时候并不需要复杂的数论,而只是用到了一个简单的抽屉/鸽巢原理,即全集的两个元素个数都超过半数的子集,一定存在共同元素。我们在Sets模块中用FAU证明这一性质,并将这一性质提供给Main模块,这样在Main模块中就不需要引入算术,而直接用isquorum表示给候选人投票的人的集合的元素个数超过一半。

除了算术,另一个经常出现的导致不可判定的情况就是函数循环。比如有f函数将T类型的元素映射到S类型,g函数将S类型映射到T类型,这样函数嵌套起来之后的搜索空间会变为无限。这里我们需要用EPR进行分解,避免出现函数的循环。

在之前的过程中,有voter将Citizen映射到Set,又有common_member将Set映射到Citizen,因此我们需要一个新的模块Votes,在Main和Votes模块中分别只能包含一个方向的映射。我们引入enough_votes直接判断候选人是否得到足够多的票数,把其具体实现放在Votes模块中不对Main可见的实现部分,并用ensures给出其postcondition。这样就把清点票数这一具体的动作抽象为enough_votes,用votersof替换voter,使得Votes模块和Main模块都可以用EPR描述。

至此,我们将领导人选举这一流程拆分为三个模块,分别是Main,Sets和Votes,并且它们都可以用一阶逻辑的可判定片段EPR或FAU描述,从而实现了可判定分解。

在该文章中,作者还详细介绍了模块化证明语言MDL(Modular Decidable Language)的语义和证明规则,并使用工具Ivy验证了两个著名的分布式协议Raft和Multi-Paxos。