基于非交互式Petri网的异步程序验证模型和方法.pdf

资源描述

1、基于非交互式 Petri 网的异步程序验证模型和方法*吴志文,李国强(上海交通大学软件学院,上海200240)通信作者:李国强,E-mail:摘要:异步程序使用异步非阻塞调用方式来实现程序的并发,被广泛应用于并行与分布式系统中.验证异步程序复杂性很高,无论是安全性还是活性均达到 EXPSPACE 难.提出一个异步程序的程序模型系统,并在其上定义两个异步程序上的问题:等价性问题和可达性问题.通过将 3-CNF-SAT 规约到这两个问题,再将其规约至非交互式 Petri 网的可达性证明两个问题是 NP 完备的.案例表明,这两个问题可以解决异步程序上一系列的程序验证问题.关键词:异步程序;非交互式

2、Petri 网;可达性;等价性;可达性中图法分类号:TP311中文引用格式:吴志文,李国强.基于非交互式Petri网的异步程序验证模型和方法.软件学报,2023,34(8):36743685.http:/ and Method for Verifying Asynchronous Program Based on Communication-free Petri NetWUZhi-Wen,LIGuo-Qiang(SchoolofSoftware,ShanghaiJiaoTongUniversity,Shanghai200240,China)Abstract:Asynchronousprogra

3、msutilizeasynchronousnon-blockingcallstoachieveprogramconcurrency,andtheyarewidelyappliedinparallel and distributed systems.However,it is very complex to verify asynchronous programs,and the difficulty can be ranked asEXPSPACE in terms of both safety and liveness.This study proposes a program model

4、of asynchronous programs and defines twoproblems of asynchronous programs,namely,-equivalence and-reachability.In addition,the two problems can be proved to be NP-complete by reducing the 3-CNF-SAT to the problems and making them further reduced to the reachability of the communication-freePetrinet.

5、Thecaseshowsthatthetwoproblemscansolvetheverificationproblemsofasynchronousprograms.Key words:asynchronousprogram;communication-freePetrinet;-reachability;-equivalence;reachability 1 引言随着计算机多核系统与分布式系统的大规模发展,异步程序得到了前所未有的广泛应用.异步程序是一种普遍存在的系统编程风格,用于管理与环境的并发交互.异步程序使用异步非阻塞调用方式来实现程序的并发.这种调用不需要等待函数或者过程返回结果,

6、可以直接继续执行程序;而同步阻塞调用需要等待函数或者过程返回结果,然后才能继续执行程序.然而编写正确的异步程序也非易事,对异步程序的程序验证更是一类难题.由于一个具有多栈的程序模型是图灵完备的1,因此通常来说,异步程序上的验证问题是不可判定的.除此以外,不同线程*基金项目:国家自然科学基金(61872232,61732013)本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-09-03;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-03-24CNKI 网络首发时间:2023-02-24软件学报ISSN1000

7、-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):36743685doi:10.13328/ki.jos.006615http:/中国科学院软件研究所版权所有.Tel:+86-10-62562563之间以异步方式通讯,需要借助不同媒介,如队列(queue)、共享缓冲区(sharedbuffer,通常表示为多重集合)、邮箱(mailbox)等,也为验证带来了一定的困难2.因此学术界为了得到异步程序可判定的性质,通常采用近似或抽象等方法,对程序模型作出一定限制.即便如此,异步程序的程序验证依然困难3,4.在异步程序模型的研究中,Sen 等

8、人将异步通讯程序限定为拥有一个无限的程序栈,要求通讯时程序栈需为空,提出了多重集下推系统5,并将异步程序的安全性问题归约到 Petri 网6的可覆盖性问题上.Ganty 等人则在此基础之上,借助 Parikh 像将异步程序的活性问题归约到 Petri 网上的可达性问题上7.Atig 等人在多重下推系统上,通过禁止在同一个线程上执行的任务之间传输锁,证明了带有嵌套锁的多线程异步程序上的可达性问题的复杂度是 EXPSPACE-complete8.Emmi 等人提出面向事件驱动(如中断)的异步程序模型9,并通过数据 Petri 网这个Petri 网的扩展模型的可覆盖性问题来解决事件驱动异步程序的安全

9、性问题.众所周知,Petri 网是一种状态转移系统,可以用来描述异步、并发的计算机系统模型.Petri 网的可覆盖性问题的复杂度是 EXPSPACE 完备,Petri 网的可达性问题的复杂度则是 EXPSPACE 难.因而缺乏高效的 Petri 网验证工具,上述提到的研究都只是理论结果,并未有验证工具.此外,也有一些工作针对 Petri 网提出了不同的扩展,但也有相当高的复杂度1014.非交互式 Petri网作为 Petri 网的一个子类,其验证性质(可覆盖性、可达性等)的复杂度是 NP 完备15.本文提供了一个异步程序的抽象模型异步程序标签控制流图(asynchronousprogramla

10、bellingcontrolflowgraph,APG)系统,并提出了两种程序验证性质等价性问题和可达性问题,同时证明这两个问题是 NP 完备的.我们将 CNF-SAT 规约至这两个问题,证明其是 NP 难的;然后,将这两种性质归约到非交互式 Petri 网的可达性问题,从而证明它们的 NP 完备性问题.这两种程序验证性质可以对异步程序的安全性进行近似,同时验证一些更具体的应用,如:动态更新、缺陷定位等.通过实验室开发的非交互式 Petri 高效工具可以开发出高效的验证工具.本文第 2 节对用到的预备知识进行概述,包括 Petri 网、非交互式 Petri 网、上下文无关语法等.第 3 节给出

11、我们提出的异步程序抽象模型 APG 系统及其语义,并提出两种验证性质可达性和等价性.第 4 节引入一种计算模型并行下推系统,并证明了异步程序的这两种性质是 NP 完备.第 5 节案例分析,介绍 APG 如何表示程序以及验证性质如何刻画具体程序问题.第 6 节总结全文,并对未来工作进行探讨.2 预备知识 2.1 基础记号=v1,v2,.,vk给定一个有限字母表,符号和分别表示由生成的自由幺半群(freemonoid)和自由交换幺半群(freecommutativemonoid).通俗地说,即表示所有由中字母组成的字符串,而表示由生成的多重集合(multiset).NNkkP:Nkw Pw(ai)

12、aiwwP(w)=(Pw(a1),Pw(a2),.,Pw(ak)记为自然数集合,表示所有定义在自然数上的维向量集合.定义 Parikh 映射为.对每个单词,记为字母在单词中的出现次数.对每个单词,在字母表上的 Parikh 映射的象(Parikhimage)为.Parikh 映射是研究形式语言的一个重要工具.我们将在后文使用它来辅助证明本文模型中的验证问题.2.2 Petri 网(S,T,W,M0)定义 1.Petri 网.一个 Petri 网是一个四元组,其中,ST=(1)S 和 T 都是不相交的有穷集合,即,S 和 T 分别表示 Petri 网中的库所和迁移,一般在图中用圆形节点和方形节点

13、表示.Petri 网中的一个对象不会同时是库所和迁移.W:(S T)(T S)N(2)是一个权重函数,分配给每个弧一个非负的权重.M:S NM0(3)Petri 网的标记是一组从库所到自然数的映射,含义是每个库所分配的令牌个数.表示该Petri 网的初始标记.t Tts S|W(s,t)0ts S|W(t,s)0对一个迁移,将其前集(输入库所集)记为,即,将其后集(输出库所集)记为,即.吴志文等:基于非交互式 Petri 网的异步程序验证模型和方法3675tss tM(s)W(s,t)tM0Mt MM(s)=M(s)+W(t,s)W(s,t)T=t1t2.tn1tnM0M1,M2,.,Mn1如

14、果对一个迁移的前集中的任意库所,即,都满足,那么称这个迁移被标记 M 触发.迁移被触发后会转移到一个新标记,记为,其中新标记的令牌数由公式确定.给定一个若干个迁移组成的迁移序列,两个标记和 M,如果存在标记使得以下公式成立:M0t1 M1t2 M2t3.tn1 Mn1tn M,M0T MM0则将其记为,并称 T 为触发序列,同时称标记 M由标记可达.非交互式 Petri 网是一类特殊的 Petri 网,和另一种描述并发程序的模型基本并行进程(basicparallelprocess,BPP)是等价的.(S,T,W,M0)s S,t T,|t|=1W(s,t)1定义 2.非交互式 Petri

15、网.给定一个 Petri 网,若对于任意,且,则称该 Petri 网为非交互式 Petri 网.S=s1,s2,s3,s4,s5,s6T=t1,t2,t3,t4ti(1 i 4)图 1 是一个非交互式 Petri 网的例子,此处每条弧权重设为 1.表示库所集,表示迁移集.迁移恰好只有 1 个输入库所,因此构成非交互式 Petri 网.s1t1t4t2t3s2s5s4s3s6图1一个非交互式 Petri 网的例子(S,T,W,M0)M0问题 1.非交互式 Petri 的可达性问题.给定一个非交互式 Petri 网,和该 Petri 的一个标记 M.则非交互式 Petri 网的可达性问题定义为:

16、判定标记 M 是否由初始标记可达.针对非交互式 Petri 的可达性问题,文献 15给出以下结论.这一结论是本文工作的核心关注点,利用非交互式 Petri 网的可达性问题的可判定性,证明后文的相关问题.定理 1.文献 15,Theorem3.2.非交互式 Petri 网上可达性问题的复杂度是 NP 完备的.2.3 上下文无关文法G=(Non,Ter,A,P)定义 3.上下文无关文法.一个上下文无关文法(context-freegrammer,CFG)是一个四元组,其中,NonTer和是不相交的有穷集合,分别表示非终结符集和终结符集.A Non表示开始变量,用来表示整个句子(或程序).P Non

17、(NonTer)是一个有穷的集合,P 的成员称为文法的规则或产生式.由上下文无关文法产生的语言称为上下文无关语言.上下文无关语言的等价性问题是不可判定的.因此,我们介绍一类特殊的上下文无关文法:交换上下文无关文法.Gc=(Non,Ter,A,Pc)NonTerPc Non(NonTer)定义 4.交换上下文无关文法.一个交换上下文无关语法(commutativecontext-freegrammer,CCFG)是一个四元组,其中、A 和前文一致,而.,(NonTer)给定两个可交换词,如果由产生式,可以直接产生,则记为;如果经过了若干次3676软件学报2023 年第 34 卷第 8 期产生式的

18、使用,可以产生,则记为,其中表示的自反传递闭包.Gc=(Non,Ter,A,Pc)w TerAw问题 2.统一词问题(uniformwordproblem).给定一个交换上下文无关语法,和一个可交换词.统一词问题16定义为:判定是否成立.定理 2.文献 15,Theorem4.1.在交换上下文无关文法中,统一词问题的复杂度是 NP 完备的.wAwGVw LG(N)V证明的思路是将统一词问题归约到非交互式 Petri 网的可达性问题,即将上下文无关文法翻译为非交互式Petri 网,那么可交换词为该 Petri 网中的一个可达标记当且仅当成立.也就是说该文献表明,对于每个交换上下文无关文法,都存在

19、一个非交互式 Petri 网,使得对的成员资格查询可以通过对的可达性查询来回答.3 程序模型本节提出异步程序标签控制流图(APG)系统,以控制流分析方法来辅助刻画异步程序的特征.我们首先简要介绍一下如何使用控制流图来形式化表示异步程序.3.1 APG 系统(P,E,V)定义 5.APG 系统.APG 系统表示异步程序标签控制流图 G(asynchronousprogramlabellingcontrolflowgraph).G 可以用一个元组来表示,其中,P=p1,p2,.,pn(1)是一个有穷的过程(procedures)名称集,用于表示可以被调用的过程集合.V(2)是一个控制节点集,每个控

20、制节点代表程序的一个基本块(basicblock),即对应一段异步程序中最大顺序执行的代码序列.E V LV(3)是一个边集,其中 L 是一个标签集合,E 表示节点到节点的迁移或跳转关系.p P,pvspvep对于每个过程在控制节点集 V 中都有一个入口节点(start)和一个出口节点(end),分别表示程序在这过程 p 执行开始和结束的位置.过程 p 可以在任何时候被调用.VpVpVp VVpvspvep需要注意的是,我们定义的 APG 系统是良结构的.我们用表示控制节点集中属于过程的控制节点集合,则有.良结构的意思是说,中任意节点都能从入口节点出发可达,并且可到达出口节点.而标签集合 L

21、中的标签共有以下 3 种类型.u v Euv(1),标签为空标签,表示不存在过程调用,仅存在一些状态的迁移.控制流在过程内部执行,从控制节点直接转移到控制节点.ups v Epsuppv(2),标签为同步调用标签,表示控制节点同步(synchronous)调用了过程,并且在过程调用完成后控制流返回到控制节点.upa v Epauppv(3),标签为异步调用标签,表示控制节点异步(asynchronous)调用了过程,无需等待过程返回,控制流直接转移到控制节点.3.2 APG 系统的语义T:E D D,Td我们在 APG 系统中引入数据流分析方法,来分析异步程序的行为.令 D 表示一个数据流值的

22、有限集合,T 表示一个数据流转移函数,即将 APG 系统中边集一条边 e 和一个数据流值 d 映射到另一个数据流值上.现在我们给出 APG 系统的格局定义.(Pr,M,N)定义 6.APG 系统的格局.APG 系统的格局用一个三元组来表示,其中,Pr (V D)V)(1)是一个带有程序堆栈的抽象状态的多重集,抽象状态指控制节点和数据流值,栈符号则表示控制节点.M P(2),其中 M 表示处于 pending 状态的异步调用,即还在等待执行的调用.N PN(3),其中表示处于 returned 状态的异步调用,即执行结束后已经返回的调用.main在引入以上格局的记号后,若用记号表示程序入口,则对

23、一个异步程序来说,其对应的 APG 系统的初始吴志文等:基于非交互式 Petri 网的异步程序验证模型和方法3677格局集合为:(vsmain,d0main),),).mainvsmaind0main,此时,程序在过程入口节点开始执行,初始数据流值为表示程序栈为空,pending 和 returned调用也都为空集.定义 7.APG 系统的语义.针对一个异步程序的行为,我们将其分为以下几类,并定义 APG 系统的语义如下.(1)过程内部操作:e=v v(v,d),)Pr,M,N)(v,T(e)(d),)Pr,M,N).(v,d)(v,T(e)(d)此时程序的全局抽象状态被改变,由变为.由于只是

24、过程的内部操作,栈顶符号仍为,保持不变;M 和 N 也保持不变.(2)同步调用:e=vps v(v,d),)Pr,M,N)(vsp,T(e)(d),v)Pr,M,N).vspdT(e)(d)vv此时程序的全局抽象状态被改变,控制节点变为同步调用入口节点,数据流值由通过转移函数变为,栈顶符号发生变化,将压入栈,变为;由于是同步调用,因此 M 和 N 也不会发生变化.(3)同步返回:(vep,d),v)Pr,M,N)(v,T(e)(d),)Pr,M,N).vepvv此时程序的全局抽象状态被改变,控制节点从出口节点返回到,栈顶符号也发生变化,此时需要将从栈顶弹出,栈顶符号变为.(4)异步 post:

25、e=vpa v(v,d),)Pr,M,N)(v,T(e)(d),)Pr,pM,N).vspvp,N异步调用需要发送一个 post 请求,与同步调用类似,但异步调用不需要等待调用返回,而是让调用进入pending 状态,所以控制节点不会变为入口节点,而是直接变为,数据流转移则于同步调用类似,栈顶元素不会发生变化;M 中则加入一个处于 pending 状态的异步调用则不变.(5)异步调用 dispatch:(Pr,pM,N)(vsp,d0p),)Pr,M,N).vsppM异步调用中处于 pending 状态的调用 p 总会被某个线程执行,此时表现为异步调用分发(dispatch).程序全局状态发生

26、改变,控制节点变为入口节点,而 M 则需要减少一个正在 pending 状态的调用 p,由一开始的变为 M.(6)异步返回:(vep,d),)Pr,M,N)(Pr,M,pN).vepp异步返回表示该调用处于 returned 状态,控制节点从出口节点离开,程序全局抽象状态回到 Pr;M 不会改变,N 则加入一个处于 pending 状态的异步调用.至此,我们在 APG 系统上定义了异步程序的行为.3.3 安全性性质和验证问题真实世界中大多数实际运行的程序,都会由于语法、语义的出错导致出现与预期不符的异常行为.而异步程序由于其涉及多线程间通讯等并发要求,编写起来相当困难,也容易出现异常行为,更难

27、以进行软件测试.解决方案是通过形式化的方法,将程序转化为程序模型,使用模型检测等验证技术,找出程序模型的错误以及异常行为,可以从本质上为我们完成对程序的验证,以此保证程序的安全性.3678软件学报2023 年第 34 卷第 8 期异步程序的可达性问题以及等价性问题都是不可判定的.因此本文通过对模型作出一些限制,重点讨论以下两个问题:异步程序中的可达性问题以及等价性问题.而借助非交互式 Petri 网的可判定性以及相关高效的验证工具,可以来对程序的安全性性质进行验证.于是我们引入 APG 系统的可达性问题与等价性问题,以及第 4 节提及的并行下推系统,并将其最终归约至非交互式Petri 网的可达

28、性上.G=(P,E,V)(M,N)Ginit-reachable-reachableReach(G)=(M,N)|init(,M,N)定义 8.APG 系统的可达性问题.给定一个 APG 系统,一个格局,在中所有从初始状态经过若干次迁移能到达的格局集合称为集合.记迁移规则的自反传递闭包为.则集合可以写为.(M,N(M,N)Reach(G)(M,N)Reach(G)(M,NAPG 系统的可达性问题定义为:给定一个格局),判断格局是否在中.若格局在中,则称格局)可达.程序的可达性问题又被称为安全性问题,这是因为往往可以通过验证程序错误或异常状态的不可达来说明程序的安全性.G1=(P1,E1,V1)

29、,G2=(P2,E2,V2)定义 9.APG 系统的等价性问题.给定两个异步程序,其所对应的 APG 系统为.Reach(G1)Reach(G2)APG 系统的等价性问题定义为:判定这两个程序的可达集合是否相等,即是否等于,若二者相等,则这两个程序等价.等价性问题又称为安全等价性问题,例如,给定一个异步程序和一个截止日期,询问它是否可以在每种可能性上准时执行.对于异步程序中的可达性问题以及等价性问题来说,我们讨论其复杂度下界.因此我们给出以下引理.引理 1.异步程序的可达性问题的复杂度是 NP-hard 的.引理 2.异步程序的等价性问题的复杂度是 NP-hard 的.对于引理 1 和引理 2

30、,我们并不直接给出证明.我们将在第 4 节中证明更强的结论,即异步程序上的可达性问题和等价性问题的复杂度是 NP 完备的.证明的主要思路是通过引入并行下推系统,使用归约手段,将 3CNF-SAT 问题归约到并行下推系统的这两个问题.request_listmainreqsreqsrcclientclient在本节的最后,我们用一个较为简单的例子来说明如何使用 APG 系统来对异步程序进行验证.图 2 表示一个异步程序代码片段,用来模拟向客户端发送请求处理任务.r 是一个类型的全局指针,用于表示请求列表中的当前请求.程序入口在,这段程序首先初始化 r,然后异步调用函数,随后开始循环调度.函数用来

31、向远程客户端发送请求.其逻辑是,如果请求列表 r 为空,则异步调用其自身;否则为变量(表示远程客户端)分配一块内存,若无内存可分配,返回一个超出内存限制异常,否则异步调用函数,随后执行下一个请求列表中的下一个请求.函数用于处理请求相关任务.图2一个异步程序的代码片段P=pmain,preqs,pclient对于图 2 中的异步程序,我们可以将过程调用抽象成集合,程序中最大顺序执行的代码序列抽象成控制节点集 V,控制流的迁移关系抽象为边集 E.对 E 中边上的标签进行分类.针对调用的类型以及是否调用,将其分为异步调用和同步调用以及过程内不涉及调用,并将这 3 种类型抽象为控制流图中的 3 种不同

32、标签.最后通过以上方式得到一个异步程序标签控制流图(APG),来刻画这个异步程序.main在这个异步程序的 APG 系统中,每个 procedure 对应的控制流图如图 3 所示.函数为入口,因此在此省吴志文等:基于非交互式 Petri 网的异步程序验证模型和方法3679略其控制流图.APG 系统的可达性可以由其对应的并行下推系统归约至非交互式 Petri 网来回答,因此可以验证程序的安全性等性质.Reqss,891011papaps131415171819e,2022-2324-25e,26s,21Client图3图 2 中所有 procedure 对应的控制流图 4 并行下推系统我们引入计

33、算模型并行下推系统(parallelpushdownsystem,PPS),将 APG 系统上的可达性与等价性转为对应 PPS 上的验证性质.并行下推系统的语义可以看成是多个下推系统无通讯地并行执行,即:PPS=PDS|PDS|.|PDS.4.1 并行下推系统的语义为了转化 APG 系统上的可达性与等价性,我们首先给出并行下推系统的格局定义以及其语义.(Pr,M,N)Pr,M,N定义 10.并行下推系统的格局.并行下推系统的格局用一个三元组来表示,其中与前文APG 系统保持一致.(G=(P,V,E),main)PPSGPPSG=(Q,q0,Qf,P,init)定义 11.并行下推系统的语义.我

34、们可以通过重新定义全局抽象状态集合,并忽略 APG 系统中同步调用的标签,将一个程序所对应的 APG 系统转化成一个并行下推系统.,其中,Q=(V D)q0ppPqfppP(1)是状态的有穷集合.q0:P Qpq0(p)=q0p(2),对每个,有,表示起始状态.Qf:P P(Q)pQf(p)=qfp(3),对每个,有,表示最终被接收的状态的集合.P=P(4)是输入字母表集合.=v|vps v Efor somep P(5),表示栈字符集.init(6)表示并行下推系统的初始格局.(Q)P(Q)转移函数是满足以下条件的最小集合.e=v v Eu d D(1)令,对每个和,都有以下公式成立:(v,

35、d),u)(v,T(e)(d),u).e=vps v Eu d D(2)令,对每个和,都有以下公式成立:3680软件学报2023 年第 34 卷第 8 期(v,d),u)(vsp,T(e)(d),uv),(vep,d),v)(v,d),).e=vpa v Eu d D(3)令表示 APG 中一条异步调用的边,对每个和,都有以下公式成立:(v,d),u)p(v,T(e)(d),u).p P(4)对每个,都有以下公式成立:(q0p,)(vsp,d0p),).p Pd D(5)对每个和每个,都有以下公式成立:(vep,d),)(qfp,).PPSGps注意到,标签是表示异步调用的过程名称,并且栈字符

36、集保存的是同步调用返回后的控制节点.并行下推系统的迁移规则是继承其对应的 APG 系统的规则,并通过将同步调用标签视为标签后得到的.因此从APG 系统转化而来的并行下推系统也可以视为空栈限制,即其格局中的 Pr 为.4.2 并行下推系统可达性问题的复杂度下界PPSG异步程序的可达性问题被转化为在对应的系统的可达性问题.与 APG 系统可达性问题的定义相似,我们给出其对应并行下推系统可达性问题的定义.(M,N)(M,N)init定义 12.并行下推系统的可达性问题.给定一个格局,并行下推系统的可达性问题定义为:判断格局是否由初始格局可达.引理 3.并行下推系统(PPS)上可达性问题的复杂度是 N

37、P 难的.证明:我们从 3-CNF-SAT 问题可以归约到并行下推系统的可达性问题来证明引理 3.=ciC=c1,c2,.,cmU=u1,u2,.,unpuipcj给定一个 3-CNF 公式,是定义在有限布尔变量集上所有子句的集合.我们将过程构造为文字(literal),将过程构造为子句(clause).puiui=trueui=false过程有两条从起始节点出发的出边,分别代表和.ui=truevTvFui=trueui=falseCiuiuipuivTpuicjCipcj首先考虑的情况.令和分别为代表和的节点.令是所有包含的字句的集合.那么对于变量对应的过程,我们将其行为定义为:从出发,过

38、程顺序地异步调用变量对应的过程,然后转到出口节点.ui=falsecjpcjpmainpui(1 i m)对于的情况可以类似地定义.考虑变量对应的过程,将其行为定义为它异步调用自身到起始节点或者直接转到出口节点的过程.顺序地同步调用进程,然后转到出口节点.(M,N)M=ni=1pc1,pc2,.,pcmN=pmain现在我们考虑格局的可达性问题,此时有,并且.(M,N)因此根据以上构造方法,我们可以得到格局是可达的当且仅当公式是可满足的.并且构造在多项式时间内可以完成.综上,引理 3 得证.4.3 安全性性质和验证问题PPSG异步程序的等价性问题被转化为在对应的系统的交换上下文无关文法等价问题

39、.PPSGPPSG对于系统来说,其可识别的单词由其中下推系统接受的单词合并得到.而在系统的上下文语义中,单词指的是异步调用的序列.PPSG(M,N)(M,N)initw(,M,N)w1pi,w2pi,.,wnipiq0piqfpi(1 i|P|)引理 4.给定一个并行下推系统,一个格局.则格局由初始格局可达(即)当且仅当存在单词被初始状态为和最终状态为的下推自动机所接受,且满足以下条件.wwjpi1 j ni,1 i|P|由所有合并得到,其中.pi=mainPw(pi)=mi+ni1pi,mainPw(pi)=mi+ni对,有,对,有.吴志文等:基于非交互式 Petri 网的异步程序验证模型和

41、.同理对任意前缀以及,若,则有,反之亦有.=方向w1pi,w2pi,.,wnipiq0piqfpiMiMi=(Q,q0pi,z0,qfpi),(1 i|P|)(M,N)initwwinitw(,M,N)(M,N)“”.如果存在单词被初始状态为和最终状态为的下推自动机所识别,其中.那么只需要证明此时并行下推系统的格局由可达.将所有单词合并后得到.这个即表示异步调用的序列,一个迁移序列使得成立,即并行下推系统中的格局可达.综上,引理 4 得证.PPSG引理 5.存在一个多项式的归约方法,使得上的可达性问题可以归约到交换上下文无关进程的可达性问题.PPSGw1pi,w2pi,.,wnipiq0piq

42、fpiMi1 i|P|证明:由引理 4,中的可达性问题可以等价于存在单词被初始状态为和最终状态为的自动机所接受,其中.PPSGMi因此,我们只需要证明可以将中的下推自动机与一个交互上下文无关文法等价.而每一个下推自动机与一个上下文无关文法等价.根据定义 4,只需要证明其对应的上下文无关文法中的产生式右边的符号与顺序无关,是一个多重集.PPSG因此上的可达性问题可以归约到交换上下文无关进程的可达性问题.综上,引理 5 得证.定理 3.异步程序的可达性问题的复杂度是 NP 完备的.PPSGPPSG证明:由于异步程序的可达性问题被转化为在对应的系统的可达性问题.而由引理 5,存在一个多项式时间的归约

43、方法,使得上的可达性问题可以归约到交换上下文无关进程的可达性问题.又因为交换上下文无关文法和非交互式 Petri 网等价,因此异步程序的可达性问题是 NP 完备的.综上,定理 3 得证.对异步程序的安全等价性问题来说,我们考虑其可达集.非交互式 Petri 网的语言等价性是不可判定的,可达集等价问题也是困难的.我们使用形式语言理论中的 Parikh 引理17来证明我们关于异步程序等价性问题结论.Parikh 引理表述如下.LLParikh(L)=Parikh(L)引理 6.Parikh 引理.对任意上下文无关语言,存在一个高效的可计算正则语言,满足:.Parikh通常来说,这个正则语言的构建需

44、要指数时间 EXPTIME.但是在这个问题中,由于我们考虑的标签表示的是程序的同步调用,因此我们有比引理更简洁的表示.定理 4.异步程序的等价性问题的复杂度是 NP 完备的.证明:异步程序的等价性问题可以转化为求解其对应的可达集的等价性.又由引理 5 可知,其可达集是有上下文无关文法产生的上下文无关语言.因此根据 Parikh 引理,存在一个高效的可计算正则语言,使得二者的Parikh 映射的象相同.由于我们考虑将同步调用也视为标签,因此构建这个正则语言的复杂度可以进一步降为NP 完备.3682软件学报2023 年第 34 卷第 8 期综上,定理 4 得证.5 案例分析本节以一个具体实例来说明

45、如何借助异步程序可达性与等价性来验证程序安全性与活性,甚至动态更新、错误定位等性质.图 4 是一个带有 bug 的 server 程序例子.这个程序执行一个循环调度 server 函数,并等待外部客户端进行连接,且以异步方式读取数据.如果有一个客户端连接上了服务器,server 函数会分配一个 client 数据结构,以异步post 方式处理 client 的连接(process_client 函数),在结束后调用自身以等待下一次连接.process_client 函数根据client 的状态完成数据的读取或发送,如果为 TO_READ 则执行 read 函数,DONE_READ 则执行 se

46、nd 函数.如果发生某些错误(第 14 行),read 函数可以将连接断开,否则就读取数据.如果 read 函数读取数据时,client 的数据还没有完全读取,则将其赋为 TO_READ 状态,若完全读取,则赋为 DONE_READ 状态.在 read 函数执行到最后时,会以同步方式调用 process_client 函数.send 函数则仅当 client 状态为 DONE_READ 时被调用,最后调用disconnect 函数,将状态改为 CLOSED.图4一个带有 bug 的 server 程序例子这个程序的正确行为是通过断言(assert 函数)的方式确保 client 的状态处于正常

47、.例如在 send 函数的 assert肯定会满足,这是因为已经在第 36 行 process_client 函数中检查过.然而,这个例子在第 15 行有一个 bug,在disconnect 函数执行结束后,client 的状态被设为 CLOSED,此时程序由第 15 行跳到第 24 行执行,而在process_client 函数中,并没有针对 CLOSED 状态的检查,因此程序出现了未知行为.针对这一情况,我们可以借助可达性来验证这个异步程序的断言是否正确.核心思路是通过说明坏状态的不可达来确保程序的安全.在这个例子中,我们可以为这个异步程序构建一个 APG 系统.图 5 表示了这个异步程序

48、的 APG 系统中所有 procedure 对应的控制流图.paps图 5 中每个控制流图有一个入口节点 s 与出口节点 e,每条边上带有对应的标签或或.注意每个节点中的内容为代码的行号,表示其对应的一个基本块.而 p 则表示程序某个 procedure 的名称,例如 server 对应的控制流图中,节点 7-8 到节点 10 上的 p 指 process_client 函数,而节点 10 到节点 11 上的 p 指其自身 server 函数.吴志文等:基于非交互式 Petri 网的异步程序验证模型和方法3683ServerReadSendProcess_clientDisconnects,4

49、-5s,1167-8papa10s,13s,251415pspspsps18172124s,26s,292728s,31e,413233-3437-38papa3640s,43e,4644ps45图5APG 系统中所有 procedure 对应的控制流图(M,N)MN(M,N)(M,N)对于异步程序的安全性性质,我们可以先找到表示坏状态的格局,其中为程序从第 15 行执行到第 24 行时还处于 pending 状态的调用,表示那时已经返回的调用.我们可以借助其对应并行下推系统的可达性来回答是否在 APG 系统中格局可达.在这个例子中,是可达的,因此说明程序会到达一个坏状态,验证了其安全性.我们

50、提出模型上的两个问题可以验证一些异步程序性质,比如:我们可以借助等价性来判断程序在动态更新前后其可达集是否变化.在这个例子中,如果原程序运行时一个动态补丁发生效果,例如在第 15 行与第 16 行之间加入对客户端状态的断言以及 return 语句.则如果其可达集在动态更新之后,与原程序的可达集不等价,那么说明程序的安全性发生变化,即完成了对程序动态更新的安全性验证.这说明我们可以使用等价性来判断一个程序是否被正确的动态更新.6 总结及未来工作PPSGPPSG本文关注基于非交互式 Petri 网的异步程序验证,提出了用于刻画异步程序模型 APG 系统,引入计算模型并行下推系统,将异步程序的可达性

展开阅读全文