基于分离逻辑的云存储系统并发正确性验证

王子豪, 王捍贫

(广州大学 计算机科学与网络工程学院, 广东 广州 510006)

随着数据的快速增长，高性价比的海量存储系统已成为刚需，基于块的云存储系统又因其低成本、易扩展的特点而成为最经济可靠的选择[1]。市场研究报告表明，2020年我国云存储市场规模已达400亿元[2]。随着公共云平台的推广，依赖于云存储服务的应用日益增加，云存储故障可能会造成意想不到的负面影响。例如，2016年微软的云存储平台宕机以致部分用户在长达8天的时间内无法获得邮件服务[3]；2018年腾讯云存储发生故障，多重冗余失效，导致部分客户的数据灭失[4]。云存储系统的可靠性成为了研究热点。

验证云存储系统的正确性是提高系统可靠性的有效方法。形式化验证方法可以分析、证明程序的正确性，尽管代价略高，却能从逻辑角度保证程序中不存在特定的错误[5]。Reynolds[6]提出的分离逻辑是霍尔逻辑[7]的一种扩展，是描述和验证含地址操作和复杂数据结构的程序的有效工具[8]。文献[9]基于分离逻辑提出了块分离逻辑，用于描述云存储系统特有的存储结构和验证云存储管理程序的正确性，但需进一步考虑对系统并发正确性的验证方法。

并发程序的执行过程复杂,执行结果易受外界影响，其正确性验证一直是学界关注的热点。早在1976年Owicki等[10-11]便基于霍尔逻辑提出了“依赖-保障”方法，刻画共享内存冲突，验证并发程序的正确性。2007年，在分离逻辑出现后，O′Hearn[12]进一步提出并发分离逻辑(Concurrent Separation Logic, CSL)，认为并发正确性验证的难点在于不同线程共享存储区域所引起的冲突，同时给出了针对互不干扰的并发线程的正确性验证规则。在此基础上，CSL进一步提出了资源所有权假设和分离性假设，规定一般的存储单元不可共享、可共享的存储单元需满足特定性质。上述规定避免了并发冲突的产生，使得CSL成为基于分离逻辑的并发程序正确性验证的基础方法。

为提升并发程序正确性验证方法的可用性，研究人员在CSL的基础上引入了不同的辅助机制。例如：

(1)资源权限。在CSL中，所有权假设已经为资源引入了权限机制。Dinsdale-Young等[13]在此基础上提出了并发抽象谓词(Concurrent Abstract Predicate, CAP)，用于描述指定共享空间的性质及其所允许执行的动作，并预先完成小模块的验证。CAP细化了并发验证的粒度[14]。后续的改进包括TaDA[15]、HOCAP[16]等验证方案，为线程访问共享资源和线程间通信提供了更灵活的描述方式。另有针对存储单元本身的计数式权限模型，能更直观地反映存储资源的使用状态。如Bizjak等[17]提出的Iron验证方案,为存储资源赋予分数量化每个进程所使用的存储资源，通过分数变化的追踪实现对失控存储单元的识别，帮助验证者发现内存泄漏错误。

(2)协议机制。协议机制即消息传递机制，主要用于描述线程间的交互行为。在CSL中，线程间的交互动作通过资源完成，交互的具体动作受限于对应的资源不变式。协议机制倾向于详细追踪线程间的交互过程，为验证者提供了更为灵活的描述方法。例如，Lei等[18]提出了一种基于事件和通信代理的并发通信正确性验证模型，针对异步非阻塞通信程序给出了2组验证实例，证明了并发程序局部化、模块化验证的可行性。Hinrichsen等[19]提出的Actris验证方案更可描述消息所附带的存储关系、数量关系等性质，同时支持互斥体等并发规范，并提出了MapReduce框架下并发程序正确性验证的初步思路。上述方案在不同程度上支持对历史状态的描述和推理[20]。

(3)幽灵状态。幽灵状态是描述系统性质时有助于确定真实执行进度但不影响程序实际执行的辅助部分，一种典型的实现方法是在程序或断言中引入不参与运算的变量并在验证过程中持续跟进。在幽灵状态机制下，验证者可以直接描述一些存储单元难以直观反映的系统性质而不必关心是否有相应的命令执行过程，基于此提出的方法有Turon等[21]提出的GPS验证方案和Jung等[22]提出的高阶幽灵状态等。Clochard等[23]提出的幽灵状态监视机制则将程序正确性转化为执行程序过程中幽灵状态的正确性，验证者可以在不了解程序具体执行过程的情况下完成验证工作。幽灵状态机制能很好地与其他工具相结合，如前文提及的Iron验证方案中的权限分数便是幽灵状态的一种，Iris验证方案[24]也为包括幽灵状态在内的系统状态描述方式提供了数学基础。

云存储系统不仅是一个单纯的并发程序，它与本地机器一同构成了独特的并发执行环境。在逻辑上，以固定大小的数据块为基本存储单元所构成的“文件-块-数据”3层结构与分离逻辑所描述的“变量-可寻址内存”2层结构有显著差异；在执行上，3层存储架构的实现有赖于本地机器的2层存储架构。上述并发方案并未给出存储结构改变后的处理方式。为此，本文基于块分离逻辑提出一种云存储系统并发正确性验证方法，并给出相应的验证实例证明本文所提方法的有效性。

在存储资源控制上，本文通过扩展断言语言在块结构上实现了计数式权限机制，辅助验证者推理线程间竞争行为的性质。计数机制属于幽灵状态，能够直观反映可用存储空间的大小，可以更方便地描述云存储中“大小固定的数据块”以及本地机器上“不便扩展的内存资源”，实现2层结构与3层结构的统一。对块本身的计数限制并不影响块数量的扩增，云存储系统易扩展的特性和CSL原有的灵活程度不受减损。验证者也可以通过全局和局部资源计数的变化识别内存溢出和泄漏风险。

针对线程间交互，本文考虑异步通信环境和云存储系统对存储资源的管理需求，选择以信道作为描述进程间交互的工具，并相应地更新了建模语言、断言语言和状态更新规则。信道作为全局共享资源，同时支持数值信息的非阻塞传递以及存储资源使用权的显式转移。本文将使用权转移视为辅助验证的标记之一，允许验证者以更直观的方式追踪交互细节。

本文第1节介绍预备知识和相关工作；第2节提出云存储管理系统的并发建模语言，当中新增了与信道相关的命令并完善了对系统状态的描述；第3节提出基于块分离逻辑的断言语言，在块断言中引入了计数机制，新增信道断言分量以描述线程间通信的性质；第4节提出一组验证规则，给出了与新命令相关的公理以及与信道相关的状态更新规则；第5节给出一组验证实例；第6节总结全文。

1 预备知识

霍尔逻辑和分离逻辑的特征都是形如

{P}C{Q}

的霍尔三元组。在部分正确性假设下，三元组成立意指在满足前置断言P的情况下执行程序C，若能终止则得到的新状态必能满足后置断言Q。分离逻辑在逻辑上将存储器划分为2层：被称为堆(Heap)的可变存储区和被称为栈(Store)的不可变存储区。其中堆以地址为索引，用于实现寻址操作；栈以变量名为唯一访问依据，功能与霍尔逻辑一致。这种结构可以很直观地描述指针等与地址相关的操作。

分离逻辑中的“分离”指一个堆可以被划分为多个互不相交的部分，多个互不相交的小堆也可以合取为一个堆。分离合取以符号“*”表示。在此定义下，形如

p*p

的式子将因*号两侧的子堆拥有相同地址的单元恒为假，即在一个有效的断言中相同地址的存储单元只能出现一次。这个要求解决了可变存储区潜在的别名问题。

分离逻辑同时提出局部推理规则(Frame Rule)

局部推理规则使得验证者只需关注与命令直接相关的存储单元的局部状态，降低了验证复杂度。局部推理规则支持组合验证，为对局部状态的推理扩展至对全局状态的推理提供了路径。

1.1 基于分离逻辑的并发程序验证技术

并发分离逻辑(CSL)是基于分离逻辑的并发程序验证技术的重要基础，已衍生出大量并发程序验证工具[20,25]。

CSL首先就完全不共享存储单元的并发程序给出了推理规则，即互不干涉的并发推理规则，定义如下：

其中，线程1对线程2不构成干扰是指线程1的执行不影响线程2中任一命令的前置条件,不改变其自由变量。

互补干扰条件不足以描述并发程序的行为。CSL进一步提出资源所有权假设和分离性假设：一般存储单元只可被一个线程使用，可被复用的存储单元应归属于某一资源组；在任意时刻，一个资源组最多被一个线程使用，且系统的所有存储单元可被线程和资源组完整划分；资源组被使用前后均需使对应的资源不变式成立。在此限制下，线程间的交互由资源组实现，交互的结果及其影响范围由资源不变式提前给定。使用资源时的验证规则定义如下：

上述规则限制了进程间的交互，规避了并发执行可能带来的冲突。

锁式权限机制能够帮助控制并发冲突，分数式权限机制可以帮助验证者识别并发执行过程中资源分配不当的问题。例如，在Iorn方案[17]中存储资源获得的权限分数与线程无关,与资源大小无关，分数值仅取决于验证时执行分离和分离合取的次数。Iorn为系统初始堆的分数赋值为1，其后每次分离动作会将原堆的分数均分至划分所得的子堆上，而每次执行分离合取的所得的堆的分数为原子堆的分数和，即

empπempπ/2*empπ/2
empπ1*empπ2empπ1+π2

。

权限分数不影响程序分配、释放、读写等命令的执行，仅反映验证过程。若权限分数出现损失、全局分数和不等于1，则证明验证过程遗漏了对部分可变存储区的控制,可能存在内存泄漏风险。验证者可以追溯局部分数的变化定位出错的代码段。

1.2 基于分离逻辑的云存储系统验证技术

云平台为并发程序提供了特殊的运行环境，其本身也是一个计算机程序。保障平台本身的正确性是验证平台上各类并发程序正确性的基础之一。

云存储系统中的块结构有以下功能和特点：块内存储具体数据、分散存放，块与块结合组成文件；用户对数据的读写和系统对结构的维护以块为最小单元；系统通过块定位存储数据的具体机器乃至具体位置。块本身具备了可寻址、可扩展的特性，且块与数据之间也存在“地址-数据”的映射。王捍贫等[9,26-28]就块结构的描述、推理和验证做了一系列的研究工作。这些工作将分离逻辑原有的2层存储架构扩展为Store、HeapB和HeapV3层结构，分别代表不可变存储区、可变的块存储区和可变的本地存储区。HeapB和HeapV各自拥有堆所具备的分离属性，Store、HeapB和HeapV3者之间可构成“文件-数据块-数值”的3层体系，Store和HeapV两者之间可以构成“变量-数值”的传统2层体系。

文献[9]提出的验证方法由建模语言、断言语言和规范语言共同构成。在建模语言中，该方法引入了与文件和块结构相关的变量和命令，改善了存储架构并相应地扩展了论域。有关表达式的语法详列如下：

经扩增后的命令语法详列如下：

|ifbethenCelseC′|whilebedoC。

在断言语言部分，该方法沿用分离逻辑的断言语言描述与块无关的系统性质，引入块断言描述与块相关的系统性质，2个分量共同构成全局断言以完整描述系统状态。其中，块断言具体语法如下：

|β1→β2|bk==bk1…bkn|∀x.β

|∃x.β|∀b.β|∃b.β|∀f.β|∃f.β|empB

|bk

|b1b2|bk1==bk2。

在云存储环境下，并发程序之间不仅需要竞争云存储资源，还需要与本地机器上的其他线程竞争本地存储资源。即使将云存储资源视为可扩展资源，对于特定的数据或数据块的使用权却不可随意扩张，资源的竞争和调度受云存储管理系统控制。同时，本地内存资源有限、扩展不易，资源竞争带来的内存复用难以避免。现有工具对上述扩张限制的描述较为复杂，容易遗漏。

2 并发云存储管理系统建模语言

并发云存储管理系统的建模语言是MLBCSS[9]的扩展，新增的元素主要用于描述和支持信道等并发机制。

2.1 信道机制设计

信道机制用于满足线程间的交互需求，主要是平台管理程序与其他任务线程的通信需求，包括传输数值和存储资源使用权的上收下发。本文以信道模拟和描述两者的通信过程：每个信道都是缓存队列，信道内分别对数值信息和块权限采用先进先出的交互方式；为确保写入成功，信道容量不设限制；以非阻塞方式读取，目标信道无消息可读是不改变系统状态、执行下一命令。

对于线程的执行而言，在读取动作完成前不可得知信道的具体状态、不可利用信道内的数值信息或存储资源权限；在读取动作完成后，被读取的信息出队、被读取的块权限归线程所有。线程向信道输出数值时，需要额外在存储器中作写入，直至该数值被读取后对应的存储单元方可被释放，输出数值是一个明显改变内存状态的操作。在转移数据块使用权时，涉及的是数据块的使用权而并未改变数据块的内容或者数据块与分布式文件之间的关系，即未对系统状态作实质性的改变。综上，本文新增一函数StoreC，用于描述信道内的数值信息，定义如下：

StoresCCHVar→Values*Values*=

{(n1,…,nk)|ni∈Valurs,k∈}。

经信道转移的存储权限可用下式表示：

b.n.(l1,…,li)，

式中包含3个分量，分别是块表达式b，指代部分使用权被转移的块；一个不大于块b容量的整数n，指代被转移的存储单元数量；一个长度不大于n的地址序列(l1,…,li)、且序列中的本地地址应属于b，列明被转移权限的非空闲单元所存储的具体数据。

2.2 建模语言语法

在表达式部分，本文沿用MLBCSS所有的数值表达式、文件表达式、块表达式和布尔表达式，另新增一类信道表达式che。在命令部分，新增与信道相关的命令、修改与数据块容量相关的语句。其中信道相关命令根据2.1小节的说明给定，块命令则配合计数式权限机制作相应修改。增改后的语法详列如下：

|C:C′|ifbethenCelseC′|whilebedoC

|C1‖C2。

新增的信道变量包括空信道、数值信息、存储资源使用权3种元素以及他们的自由组合，用于描述信道的状态。存储资源使用权一式的涵义与2.1小节所述一致。

新增语句主要涉及信道操作，可满足管理线程与任务线程间的通信需求。另外，新增的块容量限制将影响原有的块命令。增改后的命令释义详列如下：

·allocated，分配新的数据块并给定容量上限；

·append，数据块追加写，受块容量限制；

·delete，删除数据块并释放对应的存储单元；

·remove，释放数据块内指定的存储单元；

·newch，开设新的信道；

·close，停用没有待收取消息的信道；

·send，向信道传出数值消息；

·tryre，尝试从信道内取出数值消息；

·pass，向信道内传出数据块使用权；

·get，尝试接收数据块使用权。

2.3 机器状态描述

系统的状态由7个函数组成，其中包括LRBCSS中使用的5个函数：由本地变量到本地存储地址的映射StoresV、由数据块变量到数据块地址的映射StoresB、由文件变量到一组数据块变量的映射StoresF、由已使用的本地存储地址最终指向数值的映射HeapsV、由已使用的数据块地址最终指向一组本地存储地址的映射HeapsB。新增的2个函数StoresC和Size分别表示信道的状态和数据块的容量上限。各个函数的具体定义如下：

Var≜{x,y,…} BKVar≜{b1,b2,…}

FVar≜{f1,f2,…} CHVar≜(ch1,ch2,…)

StoresV≜Var→Values

StoresB≜BKVar→BLoc

StoresF≜FVar→BLoc*

HeapsB≜BLoc→Loc*

HeapsV≜Loc→Values

StoresC≜CHVar→Values*

Size≜BLoc→。

为方便起见，各类数值都限于整数范围内，各类地址限于非负整数范围内，则表示不包含任何地址的nil可以被定义为-1。

根据2.1小节给出的信道机制，数值信息的读写操作将改变存储器的状态；块权限的转移在执行时不改变存储器内的映射关系，在验证时影响各线程可用的存储区。因此，StoresC是一个由信道变量指向数值队列的映射，而通过信道转移的数据块使用权仅用于辅助推理。

块的容量限制主要用于对云存储系统中块结构以及机器中有限内存资源的建模。在各类分布式存储系统中，数据块可以视为存储的基本单位，容量大多是固定的。如HDFS通常会将一个大文件划分为多个64 MB的数据块，TFS则会将多个小文件整合成为64 MB的数据块。在机器中，扩展内存资源通常需要停机后更新硬件才得以实现。模型中的数据块容量上限在数据块建立之初被指定，但在此后不可扩增，以表征云存储中固定大小的块结构和机器中内存不可增长的特性。在程序运行时，允许进程将自己所拥有的数据块作划分而不改变数据块的总容量，以支持对本地内存调度的建模。因此，Size是一个由已使用的数据块地址指向自然数的映射。

2.4 建模语言的指称语义

指称语义为语句和表达式在特定状态下的具体意义给出说明。机器的状态由一个七元组给定，但并非所有表达式或所有命令的释义都同时依赖于所有的状态函数。简便起见下文只列出释义所依赖的必不可缺的部分，给出本文新引入的表达式和语句的语义。

新增的信道表达式的语义给定如下：

ifche1(sC)=(loc1,…,loci)and

其中，n为数值信息，ch为信道变量。

新增的数值表达式$bk表征地址为bk的数据块的容量。原有的表达式#bk可以代表该数据块内已使用的空间，应不大于$bk。其语义分别如下：

wherehB(bkσ)=(loc1,…,locn)

andk<=$bk(sF)(sB)(sV)(hB)(Size)。

与数据块有关的命令中，追加写操作需受数据块容量的限制、删除块时需一并释放存储内容实际占用的内存空间，以确保验证过程的内存资源限制与执行状态一致；新增的remove操作是用于模拟内存和分布式文件的擦写过程。有关命令的语义给定如下：

hB[(loc1,…,loci)/bloc],[hV|loc1:e1σ,…,

loci:eiσ],Size[n/b])wherebloc∉dom(hB)

and(loc1,…,locn)∉dom(hV);

Size[0/bkσ]);

wherehB(bkσ)=(loc1,…,locm),thetermofsequence(loc1,…,locm)belongtodom(hV),theblockhadnotbeenfullm

andhB(bkσ)=(loc1,…,locm)(1≤i≤m),

otherwiseremove(bk,e)σ=(sF,sB,sV,sC,hB,hV,Size)wherethestatecannotbechangedlegally。

信道机制中，块权限的转移用于辅助验证，对内存状态不作实质性的修改，有关命令对系统的影响由3.2小节说明。信道命令的语义给定如下：

forpassingtherightwillnotchangethestate。

hB,Size)wherech∉dom(sC);

locm+1)/ch],[hV|locm+1:eσ],hB);

wheresV(chσ)=(loc1,…,locm)and

locm+1∈Loc-dom(hV);

sC[(n2,…,nm/ch)],hV,hB,Size)wheresC(ch)=(n1,…,nm)andm∈+,otherwise

wheresC(ch)=∅。

3 断言语言

断言语言可以用于描述某特定状态下系统所具备的性质。文献[9]提出的断言语言LRBCSS分别使用地址断言和块断言2个分离描述与块无关的系统特征以及愉快相关的系统特征。本文进一步描述存储资源所面临的限制，新增信道断言以描述线程间交互的性质，相应修改了全局断言。

3.1 块断言

与LRBCSS相比，块断言在语法上主要是为数据块引入下标以表示当前可用的空闲空间。新增的remove指令将块由只写不擦变为可擦写，块有可能完全空闲，需新增相应的语句描述。块断言的语法详列如下：

|β1→β2|bk1==bk2|∀x.β|∃x.β|∀b.β

|∃b.β|∀f.β|∃f.β|bk==bk1…bkn

|β1-*β2|fe=fe′|b1b2。

块断言在语义上增加了关于块容量的说明。增改的后语义给定如下：

-$σbk==bk1…bkniffbkσ=

andbkiσ⊥bkjσforallthei,j∈,

1≤i

-$σ{bkσ},

hB(bkσ)=(e1σ,…,ekσ),bkσ=

k+nandforall1≤i≤k,ekσ∈dom(hV);

-$σbkn(emp)iffdom(hB)={bkσ},

hB(bkσ)=∅,andbkσ=n。

上式未列出的bk1==bk2和fe=fe′语句在成立时可说明不同的块表达式指向同一块地址，不必强调两者容量相同；b1b2一式表示2块内容一致，其关注重点在于内容而非空间，语义不变。

通过显式的容量说明，验证者可以直观得知数据块或对应的内存区的容量能否满足程序运行所需、是否有溢出的可能。通过对各线程持有的存储单元数量求和，可以直观得知在验证过程当中是否有被遗漏的存储单元，避免内存泄露的风险。

带计数机制的块结构也可以描述本地机器上有限的内存资源。为满足其调度所需，块断言支持块的切分使用，即

bkn(emp)∃n1,n2,n1+n2=n∧

bkn1(emp)*bkn2(emp)。

通过上式，本地机器不必拘束于传统的2层结构，同时验证者可以使用信道机制描述本地机器的内存调度行为。

3.2 信道断言

信道断言主要包括表征信道内容的语句和基本的逻辑结构。对其他存储结构而言，由于同一时刻只能在一个线程中出现，期间不应出现2个相冲突的状态描述，在应用分离合取和分离析取时必然满足“互不相交”的要求。但对信道而言，通信内容至少有发送方和接收方2者可见，即同一时刻至少有2个不同线程的状态断言会包含同一信道的内容，应用分离合取和分离析取时可能会有冲突，需另外给出说明。由于涉及存储单元所有权的转移，这一部分断言同时依赖于不可变存储器Store以及可变存储器HeapV和HeapB的状态。信道断言的语法详列如下：

|γ1→γ2|cheche′|∀x.γ|∃x.γ|∀b.γ

|∃b.γ|∀f.γ|∃f.γ|empC|γ1*γ2|γ1-*γ2。

相应的语义给定如下：

-σtrueC;

-σ∀x.γiffsF,sB,sV(n/x),sC,hB,hV,Size

-σ∃b.γiffsF,sB(n/b),sV,sC,hB,hV,Size

-σ

-σγ1→γ2iffifσγ1thenσγ2;

-σcheche′iffcheσ=che′σand

theyarepassingrightofBlocksinthesameway;

-σempCiffdom(sC)=∅;

-σγ1*γ2iffthereexistwithsC=

需要注意的是，尽管信道中的内容可能因为不同线程执行进度的差异而无法保证在每次执行中都能保持一致，但对某一特定信道而言，在同一时刻向不同线程所展示的数据流应当是一致的。因此，在对信道断言执行分离合取操作时，相同的信道应当包含内容完全相同的信息流。

3.3 全局断言

全局断言的形式是地址断言、块断言和信道断言组成的三元组

α,β,γ。

其中，块断言、信道断言分别由3.1小节和3.2小节给出。地址断言沿用自LRBCSS，具体定义如下：

|α1→α2|e1=e2|e1≤e2|∀x.α|∃x.α

|∀b.α|∃b.α|∀f.α|∃f.α|empV

|ee′|α1*α2|α1-*α2。

全局断言并非3个分量的逻辑求和。例如，若某个块出现在信道断言中，可变数据块存储器HeapB的状态将由块断言和信道断言2者共同确定，简单地使用逻辑和联结2者并不能准确表示当中的划分关系，使用分离合取“*”联结也不能准确地描述当前数据块权限的归属。对机器状态而言，这个三元组是一个不可简单分割的整体。全局断言的语法详列如下：

|∃b.|∀f.|∃f.|∀ch.|∃ch.

|emp|1*2|1-*2。

相应的语义给定如下：

-σα,β,γiffσα,σβ,andσγ;

-σ

theypasstheonwershipofBlocks;

-$σ

topasstheonwershipofBlocks;

-σempiffdom(hV)=∅,dom(hB)=∅,and

dom(sC)=∅;

-$sF,sB,sV,sC,hB,hV,Size1*2iffthere

-$sF,sB,sV,sC,hB,hV,Size1-*2ifffor

anyheaph′Handcommunicationsstatus

s′C,ifhH#h′H,sC*s′Cexistsand

sF,sB,sV,s′C,h′B,h′V,Size1then

sF,sB,sV,sC*s′C,hB*h′B,hV*h′V,Size2。

4 证明系统

有效的霍尔三元组

{P}C{Q}

由前置条件P、程序指令序列C以及后置条件Q组成。其中，前置条件和后置条件均为全局断言，程序指令序列遵循2.2小节给出的语法。本文考虑部分正确性断言，即对一个成立的霍尔三元组，要求：

(1)程序指令序列中所读写的变量或存储单元，必须被包含在前置条件P中或是在程序C中以allocated等语句合法分配所得。即程序对出现在其前置条件内的存储单元拥有完整的权限、对新存储单元自分配成功时起拥有完整权限，直至有关存储单元被剔出成立的全局断言后权限灭失；

(2)对于任何能令前置条件P成立的状态σ，C,σ是安全的，即在状态σ下运行程序C不会出现导致程序意外退出的故障；

(3)在任何能令前置条件P成立的状态σ下运行程序C，若程序终止于一个新的状态σ‘，则状态σ’必须能令后置条件Q成立。

4.1 证明规则

本节主要为每一个语句给出一个基本的证明公理。这些公理仅依赖于语句本身，而与程序结构无关。不论涉及何种存储结构，公理都采用全局命题。第一部分是适用于原有命令的公理：

{p}skip{p}

(A1)

(A2)

(A3)

(A4)

(A5)

dispose(e){emp}

(A6)

(A7)

attach(f,bk1,…,bkn)

bkn[f′/f])/f],empC}

(A8)

delete(f)

(A9)

(A10)

(A11)

第二部分是与块命令相关的公理。由于本文引入了计数式机制，相关公理被改写如下：

(A12)

(A13)

(A14)

(A15)

信道相关操作主要依据先进先出的原则给出相应的公理，同时考虑消息读取失败时的情形。有关基本公理详列如下：

(A16)

{∃ch′.e=i,empB,chch′}send(ch,e)

{∃ch′.e=i,empB,chch′·i}

(A17)

(A18)

(A18a)

(A19)

(A20)

{∃ch′.empV,empB,ch∅}

get(ch)

{∃ch′.empV,empB,ch∅}

(A20a)

(A21)

4.2 基本推理规则

推理规则依赖于特定的程序结构而成立。下列基本推理规则沿用自霍尔逻辑[7]、分离逻辑[6]、并发分离逻辑[12]以及LRBCSS[9]。

(R1)

(R2)

(R3)

(R4)

(R5)

(R6)

上式中FV (p)为命题p中的自由变量集，ModifyS(C)涵盖被程序C修改过的除信道变量以外的存储单元集合。T (be)是将布尔表达式转换为全局断言的函数,定义如下：

T(e1=e2)=e1=e2,trueβ,trueγ;

T(e1≤e2)=e1≤e2,trueβ,trueγ;

T(bk1==bk2)=trueα,bk1==bk2,trueγ;

T(true)=true;T(false)=false;

T(be1∧be2)=T(be1)∧T(be2);

T(be1∨be2)=T(be1)∨T(be2)。

在并发规则中要求的“互不干涉”原本指可能被任一程序修改的存储空间不得被另一程序读写。本文允许以下例外：

(1)与信道相关的消息和权限传递。信道机制是在全局层面服务于线程间通信，如若受限则线程间再无交互的渠道；

(2)通过信道传递数据块使用权实现的复用。这部分复用对程序运行的影响可以通过对信道操作进行验证得以释明。

4.3 涉及信道的状态更新规则

在4.2节中，考虑到信道的内容可能会被多个线程知悉，且不要求线程关注所有信道的变化，本文对分离合取给出了新的限制。同理，在推理时验证者可以按需引入或剔除可能可用的信道。下述的推理规则给出了一些可以向语句的前后置条件引入新的信道状态的情景。

每个信道都可以传输数值和数据块使用权2种消息，2种消息均采用先进先出的队列模式，且2种消息是分别使用不同的命令完成出队入队操作。因此，在验证时只需保证同一种消息的时序能维持一致，而不必在所有消息队列上保证时序关系不变，即

(RC1)

循此操作多次变换，则对任意信道都可以表示为

ch

。

在线程间通信中，以接收信息后程序所执行的动作为标准，信道可作如下划分：

(1)单向传输消息，线程接收信息后不必根据该消息对外作出特定反应；

(2)双向响应消息，线程依据接收到的信息对外作出特定反应。

对于第一类行为，线程对外传出消息可能影响任何访问该信道的线程。尽管在读取消息前受信一方不知晓信道的具体状态，但对验证者而言，任一线程都有权获取该新消息。综上，对某一涉及信道操作语句的前置条件有：

(RC2)

对于第二类行为，若某一线程在接收一个特定信息a后，能在不访问其他信道的前提下传出另一组特定信息b，则可认为传出信息a的进程期望获取信息b。即对某一涉及发信操作语句的后置条件为

(RC3)

上式中的“▷”可用于信道操作的限制条件，表明在执行操作之前信道可能出现的状态，在有多个可能性时前后置条件可用下标区别各自的配对。出于限制信道混用带来的冲突考虑，在建模和验证期间可以限制线程对信道的读写权限，以维持“互不干涉”的状态。

在实际验证过程中，验证者可以主动区分不同信道的用途和使用者，以便追踪线程间通信行为对全局状态的影响。

5 程序验证实例

本节给出的实例由3个线程组成，分别为用户发出写请求、主节点分配任务和数据节点执行存储，为一个完整的写数据过程。本节首先给出实例及其说明：

(1)线程 1. 用户端

CHVar:appW,upD;

LocalVarList

BKVar:Btemp;

send(appW, 4);

whileBtemp==0do

endwhile;

send(upD,Btemp, 4, 3, 2, 1);

线程1有2次发信行为，分别为向主节点发送写请求和向数据节点提供具体数据，均为数值信息传递。另有一次等待主节点响应的收信过程，由于非阻塞条件下tryre命令不具备等待功能，需用循环语句辅助。

(2)线程 2. 主节点

CHVar:disW,disD;

LocalVarList

Var：i;

BKVar:Bpool;

whiletruedo

ifi>0then

send(disW,Bpool);

pass(disD,Bpool,i);

endif;

endwhile;

线程2有2次发信行为，向用户端反馈可用数据块地址时是传递“地址”这一数值信息，令数据节点开辟块空间则是存储资源使用权的转移。

(3)线程 3. 数据节点

LocalVarList

Var：len,j;

BKVar:Bdisk;

while#Bdisk=0do

endwhile;

whilej=0do

endwhile;

ifBdisk==jthen

whilelen<$Bdiskthen

endwhile;

endif;

线程3有2组信息接收行为：首先从主节点获得数据块权限；其后从用户端获得需写入的数据、核对写入地址后完成操作。

后续分3部分给出各自线程的验证过程。系统的初始状态与emp等价。

1)用户端线程验证过程

appW∅}(A16)

appW∅,upD∅}(A16)

appW∅,upD∅}(A11)

send(appW, 4);

appW4,upD∅}(A17)

appW0,disW∅,upD∅}1(,RC2)

⑧ {∃bd≠0.empV,Btemp0(emp)∧Btemp=0,appW0,disWbd,upD∅}2(-,RC3)

此处对信道状态的更新依赖于主节点的验证过程。验证式⑦由RC2推出，是其他线程对信道操作的影响在全局的体现。验证式⑧依赖于主节点的响应行为，在后续部分会详细列出对应的条件。由主节点的验证过程可知，验证式⑧的首次成立不会早于验证式⑦的首次成立。

此后为一循环，验证式⑦及⑧均可以成为循环体执行前成立的状态。现以验证式⑦为基础考虑第一次循环体执行，有：

appW0,disW∅,upD∅}1(⑦)

appW0,disW∅,upD∅}1(A18a)

由于信道内无消息可读，在非阻塞通信的要求下，读操作不改变任何系统状态。同时由于验证式⑨与验证式⑩等价，可以构成循环不变式。

再考虑以验证式⑧为前置条件的执行过程：

Btemp=0,appW0,disWbd,upD∅}2(⑧)

Btemp=bd,appW0,disW∅,upD∅}2(A18)

后续可有如下验证：

send(upD,Btemp, 4, 3, 2, 1);

2)主节点程验证过程

disW∅,disD∅}(A16)

Bpool=0,disW∅,disD∅}(A11)

Bpool=0,disW∅,disD∅}(A15)

Bpool=0,disW∅,disD∅,

appW∅}1(③,RC2)

Bpool=0,disW∅,disD∅,

appW4}2(⑥,RC2)

初始化各变量后，线程进入循环状态。参考用户端线程的验证过程，循环体内可有验证过程如下：

Bpool=-,disW∅,disD∅,

appW∅}1()

Bpool=-,disW∅,disD∅,

appW4}2()

Bpool=-,disW∅,disD∅,

appW∅}1(,A18a)

Bpool=-,disW∅,disD∅,

appW∅}2(,A18)

ifi>0then

Bpool=-,disW∅,disD∅,

appW∅}2(,TRUE)

Bpool=bd,disW∅,disD∅,

appW∅}2(A12)

send(disW,Bpool);

Bpool=bd,disWbd,disD∅,

appW∅}2(A17)

pass(disD,Bpool,i);

Bpool=bd,disWbd,disDbd.4.(φ),

appW∅}2(③,RC2)

Bpool=bd,disW∅,disD∅,

appW∅}2(,,RC2)

else

Bpool=-,disW∅,disD∅,

appW∅}1(,FACSE)

skip;

Bpool=-,disW∅,disD∅,

appW∅}1(A1)

endif;

Bpool=-,disW∅,disD∅,

appW∅}1()

Bpool=bd,disW∅,disD∅,

appW∅}2()

Bpool=-,disW∅,disD∅,

appW∅}1(,A2)

Bpool=bd,disW∅,disD∅,

appW∅}2(,A2)

Bpool=-,disW∅,disD∅,

appW∅}(,)

3)数据点程验证过程

*empB,empC}(Var)

∧Bdisk=0,empC}(A11)

∧Bdisk=0,empC}(A2)

∧Bdisk=0,empC}(A2)

Bdisk0(emp)

∧Bdisk=0,upDbd·4·3·2·1∧

disDbd.4.(∅)}(,,RC2)

初始化各变量后，数据节点进入循环，等待主节点的写权限分配。与其他线程的循环等待相似，有效的读信道行为对应下列验证过程：

(emp)∧Bdisk=0,upDbd·4·3·2·1∧

disDbd.4.(∅)}()

(emp)∧Bdisk=bd,upDbd·4·3·2·1∧

disD∅}(A20)

(emp)∧Bdisk=bd,upDbd·4·3·2·1∧

disD∅}(,R3)

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD∅}(A18)

用户端按时序提交了写入地址和4个待写入的数据共5条数值信息。在执行过程中，数据节点无法得知信道内尚未被读取的信息状态，但能在读取地址之后确认循环条件已不再成立。故验证式为循环执行后的最终结果。

后续的验证过程有：

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD∅}(,R3)

ifBdisk==jthen

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD∅}(,TRUE)

其后是一个以len为循环变量的循环体。为方便起见，对循环体验证前先对验证式进行等价变换，具体过程如下：

upD(elen+1,…,e4)∧disD∅}()

upD(el′+1,…,e4)∧disD∅}()

upD(el′+2,…,e4)∧disD∅}(A18)

upD(el′+2,…,e4)∧disD∅}(A13)

upD(el′+2,…,e4)∧disD∅}(A2)

upD(elen+1,…,e4)∧disD∅}()

∧Bdisk=bd,upD∅∧disD∅}(,R3)

endif;

∧Bdisk=bd,upD∅∧disD∅}(,,TRUE)

至此可知，用户端发起的写请求得到了响应，数据节点在主节点赋予的权限范围内执行写入，被写入的块的地址与主节点向用户端反馈的块地址相同，被写入的数据与用户端提交的数据一致，写功能正确。该实例涵盖了循环、通信的重要的验证环节，可以说明本文所提方法的有效性。

6 小 结

本文基于分离逻辑提出了一种适用于并发云存储系统正确性验证的系统方法，在建模语言中引入新的命令和表达式以描述线程间交互行为、扩展断言语言，以准确描述资源受限的执行环境，并基于此完善了推理规则。验证实例说明本文提出方法的可行性。

本文所提逻辑能直观描述存储容量的限制、信道机制能描述权限的转移过程，帮助验证者验证存储管理行为的正确性，识别潜在的溢出和泄漏风险，满足云存储系统的验证所需。本文扩展了块分离逻辑的验证范围，所提方法也可推广到云存储环境下的普通并发程序的正确性验证上，为实现MapReduce、Spark等并发框架下的程序验证提供了理论上的可能性。

未来的工作包括：①降低信道机制的复杂度，改变现有通过验证者主动规避冲突的状态，提升其对时序关系的描述精度；②完善所用幽灵状态的数理基础；③探究验证规则的可表达性、相对完备性；④扩展并发正确性验证的适用范围；⑤设计辅助验证工具和算法。