Vol. 44 No. 3May  2020
第44卷第3期2020年5月江西师范大学学报(自然科学版)
Journal  of  Jiangxi  Normal  University ( Natural  Science)文章编号：1000-5862 (2020) 03-0301-06
—种基于Concurrent  Apla 语言的共享内存
并发分布式算法2层验证方法
王昌晶1，余小军1，沈德明S 罗海梅U  左正康1*
(1.江西师范大学计算机信息工程学院，江西南昌330022 ；2，江西科技师范大学通信与电子学院，江西南昌330013；3.江西师范大学物理与通信电子学院，江西南昌330022；4，江西师范大学江西省光电子与通信重点实验室，江西南昌330022)
摘要：形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一，尤其是在云计算、多核、
无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式 推导和验证方面的已有工作，以自定义泛型抽象顺序设计语言Apla 为基础，进一步研究并提出简明、高
抽象用于并发分布式计算的Concurrent  Apla 语言，使其既支持顺序算法的验证又能有效地验证并发分布 式算法.在依赖-卫式推理的基础上，提出一种新颖的2层并发分布式算法形式化验证方法，其中系统层
用于处理并发级验证，而组件层用于处理顺序级验证•最后，通过2个实例验证了该方法的有效性和可行性.
关键词：并发分布式计算；依赖-卫式推理;Concurrent  Apla；形式化验证
中图分类号:TP311 文献标志码：A  DOI ： 10.16357/j. cnki. issnlOOO-5862.2020.03.14
o 引言
形式化方法在软件验证的应用从串行程序验证 开始2]，随后运用到并发分布式系统⑶、云计算系
统曲]、反应式系统冏等.形式化方法采用数学和逻
辑的方法描述和验证软件•从描述上来讲，一方面是
关于系统或程序的描述，另一方面是关于性质的描
述•可以用1种或多种语言来进行描述，包括命题逻 辑、1阶谓词逻辑、高阶谓词逻辑、代数、状态机、
自 动机、线性时序逻辑、计算树逻辑、进程代数、77演
算、“演算、特殊的程序语言及其子集等•从验证方 法来讲，主要有2类方法：一类是以逻辑推理为基础 的演绎验证(Deductive  Verification) [7]，如定理证明 (Theorem  Proving )、自然演绎(Natural  Deduction )、
相继式演算(Sequent  Calculus)以及Hoare 逻辑等方
法；另一类是以穷尽搜索算法为基础的模型检测 (Model  Checking)⑻方法.
演绎验证不同于模型检测，它可以验证无限状
态系统，能够处理不同域(如整数、实数)上的程序, 以及线性、非线性数据结构(如栈、队列、树、图等)，
它甚至允许参数化程序的验证，如有任意数目相同
进程的程序；而模型检测自动化技术通常只能检验
有限状态系统，且只能检验这类程序的特定实例，如
检验全部含有1 ~7个进程的实例，不可判定的结果 表明通常不能自动化参数化程序的验证.除此以外,
模型检测还容易发生状态空间爆炸，这在较大程度
上限制了能被检验的并发程序的数目.
本文在抽象顺序设计语言Apla 中加入并发、通
讯和同步的语言成分，提出简明、高抽象度并发分布
式计算的Concurrent  Apla 语言，包括语法及结构化
操作语义；然后在依赖-卫式推理的基础上，提出一
种新颖的2层并发算法形式化验证方法，其中高层
系统层用于处理并行并发级验证，而低层组件层用 于处理顺序级验证；最后通过2个案例验证了方法
的有效性和可行性.
收稿日期：2020-03-19
基金项目：国家自然科学基金(61762049,11804133,61862033,61662035,61902162)，国家留学基金(202008360094)，江西
省科技厅课题(20181BAB206034)和江西省研究生创新基金(YC2019-S161)资助项目.
作者简介：王昌晶(1977-)，男，江西南昌人，教授，博士，博士生导师，主要从事可信软件、智能化软件与智能化教育的研
究.E-mail :wcj771006@ 163. com
通信作者：左正康(1980-)，男，江西抚州人，教授，博士，主要从事泛型程序设计和可信软件的研究.E-man ：kerrykaren@]26
302江西师范大学学报（自然科学版）2020年
1基于共享内存的并发分布式计算的Concurrent Apla语言
1.1Concurrency Apla语法
在抽象顺序设计语言Apla⑼中加入并发、通讯和同步的语言成分，构造并发分布式计算语言Con­currency Apla，其语法如下所示：
P：：=x=el P,；P2|if久
while6do P od|await b then P end|Pj||P2，其中x=e（赋值语句）、P[；P2（顺序语句）、if久—Pi…6”一fi（不确定选择语句）a while6do P od （循环语句）的语法来自Apla语言，与Dijkstra卫式命令语言类似.Concurrency Apla在Apla语言基础上扩展了await b then P end^Pj||P2这2个算子，使其既支持顺序算法的验证又能有效地验证并发分布式算法.同步使用await b then P end来描述.同步要求进程之间互相协调，实现统一性和一致性，当2个进程不同步时，可能导致其内存共享变量的读写错误，这时让不同步进程进行等待，使其满足条件6（即满足同步要求）再进行执行.并发使用P.||P2来描述，匕、“进程的原子行动交替执行从而实现其并发.通讯使用共享变量来描述，用共享变量来约定其读写步骤的进行.
1.2Concurrency Apla结构化操作语义
下面给出了Concurrency Apla语言的结构化操作语义，包括赋值语句（Assignment）、顺序语句（Sequence）、不确定选择语句（Conditional）、循环语句（Loop）、等待语句（Await）和并发语句（Parallel）的操作语义.其中顺序语句操作语义包含2种情况：第1种情况是在第1个程序执行过程中，程序顺利执行完成，此时转到第2个程序进行执行；第2种情况是第1个程序还没有执行完成，接下来继续执行•不确定选择语句和循环语句操作语义分别在选择条件和循环条件为真和假的2种情况下的语义•等待语句操作语义是程序进入了等待的状态，直到满足获得相关的资源条件等待终止•并发语句操作语义在满
足并发条件的情况下触发其中一个程序，此程序满足执行条件，从而使其程序可以正确地执行，当执行完后其程序的状态发生了改变，执行条件的状态也相应地进行了改变.
（i）赋值语句为
3=e,s）t（丄,fs）'
（ii）顺序语句为
「WC11（P1昇）T（丄，$'）
■（Pl；P2,S）T（P2,s'）'
:SEQ2]：（Pi，s「P,$）；
（iii）条件语句为
[CONDT]:（c^m；：sl®,s）
[condf]：丽乔加
（iv）循环语句为
[whib口：&皿6p,s)
s年b
—>(p；(while b p),5)〔whib F]：(while6p,s)_(.s)
(v)等待语句为
s e6(p,s)t(丄，s')
(await6p,s)—>(丄s')'
(vi)并发语句为
r(P,S)t(P',s')
「narallel2]-___(Q,s)―»(Q'’s')___
2基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法2.1依赖-卫式规约
并行并发算法的验证难点在于其线程的交错和变量的状态共享-C.B.Jones[10]提出了依赖-卫式（Rely-G
uarantee）推理方法，解决了可组合性问题.该方法在众多验证中⑴呵使用，应用范围较为广泛.Rely-Guarantee方法将并发任务间的接口抽象为Rely和Guarantee2种,Guarantee是对任务自身行为的抽象，用于描述自身行为的变化；而Rely则是对任务所能接受的环境行为的抽象，用于描述任务所能接受的环境行为所带来的干扰•在检查任务之间的无干扰性时，不需要逐行检查任务的代码，只要检查不同任务之间的Rely和Guarantee接口的匹配即可，要求每个任务的Rely被其他每一个任务的Guarantee蕴含（即Rely得到满足）.由于不再需要逐行检查所有任务的代码,Rely-Guarantee方法允许对单个任务进行独立验证，因此是一种具备可组合性的方法•这可以看作是一个组合的Owicki-Gries Method口4旳.
Rely-Guarantee方法是目前国际主流的并行分
第3期王昌晶，等：一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法303
布式算法验证方法.Rely-Guarantee规约是在Hoare 逻辑的基础上将断言的2元组(pre,post)的形式进行扩展，在中间过程引入R、G，使其规约扩展为4元组(pre,rely,guar,post)，因此Rely-Guarantee方法较好地兼容了Hoare逻辑方法庞].
2.22层共享内存并发算法验证方法
2层共享内存并发分布式算法验证方法思想来源于Rely-Guarantee方法，是一种可组合的推理方法，在
推理时不需要检查任务之间的无干扰性，只需检查不同任务之间的Rely和Guarantee接口的匹配，它允许对单个任务进行独立验证.因此，可以将基于共享内存的并发分布式算法的验证划分为系统层和组件层，其中系统层用于处理并行并发级，而组件层用于处理顺序级•在系统层中主要的难点是并发进程之间的共享变量的干扰性，使用Rely-Guarantee推理来形式化验证；在组件层中重点是带while循环的顺序程序，而难点是循环不变式的生成技术，使用Hoare逻辑来解决.因此，将共享内存并发分布式算法验证涉及的推理规则相应的设计为系统层推理规则和组件层推理规则2大类.
其中组件层推理规则包括Hoare逻辑的基本规贝!J：赋值规则(Assignment rule)、跳跃规则(Skip rule)、顺序规则(Sequence rule)、不确定选择规则(Conditional rule)、循环规则(Loop rule)等.具体说明如下.
(i)赋值规则为
pre[e/x]{%：=e\pre；
(ii)跳跃规则为
pre j skip[pre；
(iii)顺序规则为
pre{S]}尽，尽t$，人2{S2丨post
pre{Sj；S2}post'
(iv)不确定选择规则为
B A pre{S]}post B A pre j S2[post
pre j if B then S】else S2fi}post'
(v)循环规则为
P(x)/\P{S}P(%)
P(x)j while B do S od)-1B A P(x)'
而系统层推理规则主要包括基本规则(Basic rule)、并发规则(Parallel rule)、等待规则(Await rule)以及辅助变量规贝lj(Auxiliary variable rule).其中基本规则可以表示组件层的任一推理规则，它是系统层和组件层的接口 •具体说明如下：
(i)基本规则为
pre stable when rely
post stable when guar
\-{pre}C{post}
the effect of C is contained in guar
rely,guar\-{pre)C{post)；
(ii)并发规则为
Ri,Gi卜/MG}G；7?2,G2\-P2\c2\q2
7?=艮/\«2,G i V G2=G,G[\-R2,G2卜尽
R,G卜{匕A P2\c.II C2\Q.A Q2\;
(iii)等待规则为
pre stable when rely
post stable when guar
P sat(pre/\b/\y=坯,=y,true,guar[f0/y,
y/y']八post)
awedt b then P end sat(pre,rely,guar^post)；
(iv)辅助变量规则亦
3z.pre1(y,z,y0')
(y,z).(y‘,/),y0)
P sat(pre A pre1^rely A rely^,guar,post)
Q sat(pre,rely,guar^post).
这里简要介绍组件层推理规则Hoare逻辑的基本规则.
系统层Basic rule扩展了Hoare逻辑，只需要证明前置条件pre和后置条件post在rely的保证下能够平稳，以及自身的改变都写入到guar中，最后加上Hoare逻辑的证明规则，即可得出要证明的规则为rely,guar\~\pre]C{post)，也可写成4元组的形式C sat(pre,rely,guar,post).其中the effect of C is contained
in guar定义如下：\/a,a'P(a)A(a, a')e[[C]]=>G(a,a/)表示程序执行时的每一句的前状态和其程序执行后得到的后状态都被写进g“ar中，用以保证程序的正确执行.这里的难点在于需要仔细地分析程序以确保自身的改变都写入了guar中.程序自身的改变在程序运行时是复杂的，特别是并发算法程序，这就要求对要验证的算法步骤以及程序状态的自身改变有一个很好的认识和
在Parallel rule中淀义了如何使程序C并行的一些规则，它是对单个Basic rule的组合，使得程序满足Basic rule的同时能够通过自身的rely^guar以及并行全局的Rely,Guar来保障并行并发的正确执行.
在Await rule中，缓和了并行并发程序竞争共享资源的干扰，使其在通过Await rule时能够使并
304江西师范大学学报(自然科学版)2020年
行并发程序不出错的同时，不会因为共享资源的使用不当导致死锁或者饥饿的发生.
Auxiliary variable rule是在证明并发算法正确性的一个辅助规则，当在证明程序中引入了辅助变量时，使用此规则对此辅助变量进行消解，从而擦除辅助变量对关于程序的前后置条件的影响.
3案例研究
3.1并发执行小=乂+1
证明如下程序的正确性：
pre：{x：=0){%•=x+1)||{%•=x+1)post：!=2}.
字符串常量占ram(i)符号化表示为P"{Ci||C2) post,
(ii)引入辅助变量*=0；z：=0.
(iii)根据赋值规则构造变换前置条件
)x:=0)y：二0；z二0{光二y+z/\y=0/\ z二0}.
(iv)令P二\x=y+z[\y=0!\z=0)P 分解有
Pi：二y+z/\y=0)P2：{a；二y+z/\z=0}，则问题分解为
Q i II P2!c2}<?2;C1A Q2^post.
(v)在第1个程序中根据赋值规则有
P1t{x=y+z!\y=0((%：=a;+1；y：=1〉j%=y+A y=1),
可得p1\c1\g显然成立.p2\c2\q2也是同样的过程，同理可证.
运用基本规则通过分析血必(p】，&)；stabKQ^RJ以及程序可得
G1=y=Q/\y f=1/\x r=%+1/\z r=z,
C2=z=0A=1A x r=%+1A y r=y,
R、=G2；/?2三G].
对于R]{C]}Q]有
卜卩1{C]}G；stable(P1，尽)；stable(Q】,RJ.
(vi)通过深入分析理解程序以及定义：\/o, a f P(a)A(a,a)g[[C]]，可得
x=y+z f\y=0!\z=0/\x f=y f+z f A y r=1/\z f=z=>y=0A y z=1A=%+1A z r-z,
则有A(a,a)e[[C]]nG(g,c/).
可证R1G HP]{C]}g成立.同理可证有他，g2\-P2{C2}Q2成立.
(vii)由程序性质可知：共享变量在并行系统上而言，没有外界干扰，所以不需要依赖于外界条件，同理也不需要保证什么，所以可以设置人二False, G二True，则有下式成立：
False=y二0/\y'=1/\光'=x+1A z r-z A z=0A z'=1八％'=%+1Ay7=y,
(y=0A y7=1/\x r=%+l/\=z)V (z二0!\z r-1A x r=x+1A y'-y)^True.
可得R=«2；G i V G2=>G成立.
(viii)根据并发规则和辅助变量规则以及pre—>P；P= P］A P2^Q i A Q2—>post可得
\x=y+zf\y-^\/\{兀二y+z/\z=l}—>•二：2}.
3.2并发求最大公约数
已知pre：{%—>M,TV)用2个程序pre{C】||C2［post 求最大公约数并证明其程序的正确性得到的后置条件为
a z=GCD(M,N).
(i)引入辅助变量如』12：
$21=［兀+1］,$22=［兀］*
(ii)变换前置条件构造最大公约数函数
P=GCD(［幻，［光+1］)=GCD(M,N).
(iii)分解问题为2个子问题：
卩1{C］}Qi||P2\C2\Q2,Q x A Q2^post,
其中P=P X= P2.
(iv)构造求最大公约数程序C］:
力］］=［光］；力12=［光+1］；
while(如#t12)do j
if(i n>t12)i
=£口_勾2；
［光］—?!
fi
力12=［光+1］}•
od.
同理构造最大最大公约数程序C2:
力21=［光］；力22=［光+1］；
while(t21工t22)do{
if(=21><22)i
^21=hl~J22；
［光+1］二<21；丨
fi
力22=［光+1］；}*
od.
(v)证明程序G的正确性：
\GCD(［x］,［x+1］)二GCD(M,N)\,
如二［订
赋值规则：
GCD(［%］,［光+1］)二GCD(M^N)A t n=［光］,
第3期王昌晶，等：一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法305
t12=[x+1].
赋值规则和R,G：因为可能受程序C2的影响使得变量[%+1]减小，故对于变量如有
til=[%]A t12&[«+1]A[x~\n[%+1]=> t〔2=[%+1],
则
GCD(t n,t12)=GCD(M,N)A t n=[幻A t12&[%+1]A[x~\m[%+1]=^t12=[%+1]；
while(t n M t12)do{
GCD(如，勾2)=GCD(M,N)A t n=[幻A 巧2工[%+1]A[x~\3=[%+l]=>t12=[力+1];
if(> 址){
//不确定选择规则
GCD(t“,t(=GCD(M,N)A t u=[幻A tl2=[%+1]A ill>ti2；
如=-址；[%]=^n-
//赋值规则
GCD(t u,t12)=GCD(M,N)A f12=[^+1]A J11>J12；!■
i12=[x+1].
/
/赋值规则
GCD(如丿J=GCD(M,N)A f n W仏；丨.
//循环规则
GCD(tn,t12)=GCD(M,N)A t n=f12.
令Z=站=仏可得Z即为所求的最大公约数，可写为约束条件
3Z.x^Z,Z A z=GCD([%],[%+1]).
同理可证程序C2也成立.
(vi)通过分析程序G和stable
stable(Q1,R1)可得
G]三GCD([%'],[%'+1])=GCD(M,N)f\ [%+1]>[%'+1]A([%]>[%+1]=>[%]> [H]A<\_x+1]=>[%]=[%']).
通过分析程序C2和Cj,stable(P1,stable{Q x, RJ可得
G?三GCD([%'],[%'+1])=GCD(M,N)A [x~\>[a/]A([x+1]>+1]>[x r + 1]A[«+1]<[%]=>[«+1]=[x'+1]),
其中[%]表示变量％的前状态，[*]表示变量％的后状态.同时有三G2；R2三G[.
(vii)由程序分析以及规约Va,a'P(a,a')£[[C]]可得
GCD([*],[*+1])=GCD(M,N)A t n= [x~\A t2l>[x1+1]A([力+1]N[x1+1]A [x~\>[%+l]n[x]>[x'~\A[%]<[%+l]n [%]=[%'])，有V a,a'P(a,a')U[[C]]nG(a,a，).
综上所述证得FPJCJC p
重复上述证明过程同理可证
R2,G2\-p2iC1)q2.
(viii)由程序性质可知：对于共享变量的并行在并行系统上的全局的R,G而言，没有外界干扰，所以不需要依赖于外界条件，同理也不需要保证什么，所以可以设置R=False,G=True，则有7?= &KR2,G,V G2=G成立.
(ix)根据并发规则和辅助变量规则，同时对于程序C1;C2当运行结束时满足post-3Z.X^Z,Z K Z=GCD(M,N)，所以R,G\-{pre]C1||C2\post\成立.
4结束语
本文在抽象顺序设计语言Apla中加入并发、通讯和同步的语言成分，构造并发分布式计算语言Concurrency Apla语法及其结构化操作语义，给出了基于Concurrent Apla语言的共享内存并发分布式算法验证的组合验证规则.在依赖-卫式推理的基础上，提出一种新颖的2层并发算法形式化验证方法，其中高层系统层用于处理并行并发级，而低层组件层用于处理顺序级•最后，通过实例验证了方法的有效性和可行性.
本文的实例验证还在手工阶段，对于复杂的算法难免会因过程烦琐或者人为因素导致易出错等不足，为了弥补这种不足，同时提高验证并发算法的效率和正确性，下一步工作拟用Isabelle定理证明器对并发算法进行交互式验证.Isabelle不仅可以用于结构化程序M的证明，还可用于并发算法的证明，如在Isabelle里利用Owicki-Gries方法口刃和Rely-Guarantee方法少]等主流的并发程序验证方法对并发算法进行交互式验证，使得验证过程减少人为的干预•通过使用Isabelle对多种算法的交互式验证，也可形成定理证明库，以供使用Isabelle进行程序验证的其他研究人员学习和参考.
5参考文献
[1]王戟，詹乃军，冯新宇，等.形式化方法概貌[J].软件
学报,2019,30(1):33-61.
[2]贺飞，张立军.软件形式化验证专题前言[J].软件学
报,2019,30(7)：1901-1902.
[3]刘震伟，薛锦云，夏鲸，等.PAR平台中并发分布式事务
处理机制及其应用研究[J].江西师范大学学报：自然

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。