软件学报  2017, Vol. 28 Issue (4): 804-818   PDF    
基于通信Petri网的异步通信程序验证模型
杨启哲, 李国强     
上海交通大学 软件学院, 上海 200240
摘要: 由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.
关键词: 异步通信程序     通信Petri网     可覆盖性     程序验证     k-型    
Model on Asynchronous Communication Program Verification Based on Communicating Petri Nets
YANG Qi-Zhe, LI Guo-Qiang     
School of Software, Shanghai Jiaotong University, Shanghai 200240, China
Foundation item: National Natural Science Foundation of China (61672340, 61472238, 91318301)
Abstract: Since multi-stack models are generally Turing-complete, verification problems on general models for asynchronous communication programs are undecidable. This paper proposes a new model based Petri net, named communication Petri nets (C-Petri nets) to model asynchronous communication programs. Applying the k-shaped restriction on the input communications and the abstraction on each stack based on popping lemma of regular languages, the coverability problem of the restricted C-Petri net is decidable by encoding the model to data Petri nets.
Key words: asynchronous communication program     communication Petri net     coverability     program verification     k-shaped    

随着大规模复杂多核系统的广泛使用, 并发程序得到了越来越多的应用.但并发程序不同于顺序程序具有通用的程序验证模型 (下推系统), 即使将所有数据域抽象成有限域, 并发程序所对应的多栈模型也图灵等价, 其上最简单的验证, 如可达性不可判定[1].异步程序是并发程序中最常用的管理并发交互的一种方式, 该种程序不需要等待函数调用返回结果, 可以直接继续执行, 直到程序需要用到调用的返回结果时再去等待函数的调用结果; 同步程序则相反, 一个同步调用要求程序必须等待至函数调用完成返回结果之后, 程序才能继续执行下去.异步通信程序在异步调用之时, 允许不同线程之间通过中间存储方式进行通信.这样的程序语言包括Erlang, Scala等, 其程序行为更加复杂, 难以进行建模和验证.

在异步程序验证模型的研究上, Sen和Viswanathan提出了多重集下推系统[2], 只允许在栈空的时候发生通信, 并证明了该模型的可覆盖性可判定.这样的模型对于异步通信程序而言过于受到限制, 因为一般来说, 异步通信程序中的通信发生都不是在栈空的时候.Kochems和Ong提出了异步偏序通信下推系统[3], 并且对其进行k-型限制.该限制将栈与通信绑定在一起, 并且限定模型中栈上输入通信的数量不能超过k.在该模型中, 栈不再作为递归的标识, 因而很难对于程序进行直观建模, 并且对每个线程递归的深度限制得也比较严重.同时, 这种编码会引起栈元素呈指数级扩张, 使得模型很难找到可用于实现的高效算法.

本文基于Petri网, 提出了通信Petri网.在通信Petri网里, 一个线程被描述成在库所 (place) 里扩展的令牌 (token), 其中一个令牌是一个二维向量的形式, 而令牌在通信Petri网的轨迹则是一个进程的行为表示.由于整个信箱存放的信息是无序的, 因此消息的传递则是通过一个全局的向量来完成.同时, 每个进程会反映出它所进行的通信和栈的情况.

为了保证可判定性, 通信Petri网对于通信和栈的问题进行了分别的限制.对于通信, 通信Petri网将k-型限制转变为限制每个线程所能接受信息的最大数量为k, 也就是一个令牌的第2维向量的值不会超过k; 对于栈的部分, 我们根据正则语言的汞引理, 将栈抽象为一种等价关系.在上述两种方法的限制和抽象下, 通信Petri网可以编码到数据Petri网, 从而其覆盖性是可判定的.该方法在程序建模和验证中由于保持栈对于递归的刻画, 因而更为直观和清晰, 也更利于实现.

我们用一个例子来说明如何使用通信Petri网来验证异步通信程序.图 1图 2给出了一个用Erlang实现的简单的老师自动网上给学生分配一个作业的系统, 这个程序使用有限个信道来实现通信.

Fig. 1 An example of program (Ⅰ) 图 1 一个程序的例子 (Ⅰ)

Fig. 2 An example of program (Ⅱ) 图 2 一个程序的例子 (Ⅱ)

假设作业需要学生们合力完成, 并且共享一个资源, 每个学生只需完成自己要做的那一部分.程序一开始打开网络并且打开资源, 将有一个老师分配作业的系统, 他将所得到的作业重新分配给学生并且打印学生给出的答案.学生在收到一个作业后将会对作业逆行分析, 取出自己需要做的部分, 将剩余的部分交还给老师再进行分配.如此循环.在显示的程序里, 具体处理作业的程序被省略了.需要注意的是:由于解决作业的资源只有一个, 而学生在处理作业时需要使用这个资源, 因此会产生一系列有关是否互斥的问题.

注意到:在这样的程序里, 尽管在每个函数里都有不停的函数调用, 也会有着任意多的发送信息, 但是对于任何一个线程, 其接受消息的次数是有限的.也就是说, 在异步模式下, 可能停住的次数不是无限多次.并且在程序中栈的形式是没有记忆能力的, 也就是说, 这样的程序无法严格地分辨重复调用的不同.比如, reassign() 重复调用自己, 但程序并不会分辨reassign() 调用了自己2次或是3次这样的区别.

在这个例子中, 程序里一共有3个信道:toResource, toStudents和toTeacher, 发送的信息由于返回的答案和分配的作业是有限多个的, 不妨假设共k种, 因此可以用一个3×k维向量来模拟, 第k×i+j维对应第 (i+1) 个信道里信息j的数量.比如:当对toResource发送第1种信息的时候, 需要在第1维加1.同时, 从这一接受信息的时候开始则需要对第1维减1.将每一行程序和调用这一行程序的函数编码设为一个状态, 考虑程序中的reassign() 函数, 在整个程序中, 它会被主程序以及自己调用, 因此在编码至通信Petri网时, reassign() 函数的一行会被表示成两个库所:一个代表主程序调用的reassign() 里的语句, 另一个则代表自己调用自己里的语句.一个令牌则代表一个线程, 程序的执行可以用相应的转移来进行描述.同样, 考虑在reassign() 函数, 不妨仅考虑是自己调用自己的时候, 当收到重新分配作业的信息时, 一个令牌会从reassign() 里对应receive语句的库所转移至toStudent!Homework的语句, 同时将向量中表示对应信道对应信息的维数的值减1.而如果产生spawn操作, 令牌则会通过一个转移产生一个额外的令牌, 新的令牌就将用来模拟spawn出来的线程的运行, 那么这个程序便可以被一个通信Petri网编码, 程序的运行可以被限制下的通信Petri网进行模拟.

本文第1节介绍文中用到的一些基础知识, 包括基础记号、Petri网的概念和数据Petri网的概念.第2节介绍本文提出的模型通信Petri网的语法和语义.第3节形式化介绍异步通信程序如何编码至通信Petri网的模型上, 并且形式化地给出通信Petri网上的程序验证的安全性问题.第4节给出在k-型限制下的通信Petri网上可覆盖性问题的可判定性证明.第5节介绍关于该研究的一些相关工作.第6节总结全文.

1 预备知识

本节阐述全文用到的一些基础记号、Petri网的概念以及数据Petri网的概念.

1.1 基础记号

N是自然数集合, [d]代表{1, 2, …, d}的自然数集合.记Nd表示所有d维向量的集合, ∀aNd, 记a[i]表示向量a的第i维的值, a[i]∈N.记 (n, k) 为组合数, 其中, 如果k > n, 则 (n, k)=0.令U是一个集合, U*表示U里元素组成的字符串.此外, 令M[U]表示由U产生的一个多重集合 (multiset), 对于集合U里的一个元素ui, 定义函数ΠM[U](ui), 表示在该多重集合内ui出现的次数 (parikh image).特别地, 当多重集合不需要特别说明时, 简记函数为ΠM(ui).此外, 对于两个多重集合M[U1]和M'[U2], M[U1]+M'[U2]为两个多重集合的不相交并.

对于两个多重集合M[U1]和M'[U2], M[U1]≥M'[U2]当且仅当对于∀aU2满足${\mathit{\Pi} _{M[{U_1}]}}(a) \geqslant {\mathit{\Pi} _{M'[{U_2}]}}(a).$同样地, 对于两个元组 (p1, p2, …, pk) 和$({p'_1},{p'_2},...,{\text{ }}{p'_k}),$定义大小关系为$({p_1},{p_2},...,{\text{ }}{p_k}) \geqslant ({p'_1},{p'_2},...,{\text{ }}{p'_k})$当且仅当对于∀i∈ [k], 有${p_i} \geqslant {p'_i}$.这样就扩展了在元组上序的大小关系.

αA*A*上的一个元素, 称αA上元素产生的一个字.令m∈(Nk)*, 则m[i](j) 表示m里第ik维向量的第j位上的值.特别地, 如果m中每个向量的第j维都相同, 则简写为m(j).同时, 不妨简单令m(j) 的操作会对任意的iN, m[i](j) 都会进行相应的改变.

1.2 Petri网

Petri网[4]是由卡尔·亚当·佩特所发明的一种适合描述异步的并发的模型, 有如下定义.

定义1.2.一个Petri网是一个元组PN=(P, T, F), 其中, (1)P是有限的库所集合P={p1, p2, …, pk}; (2)T是有限的令牌集合T={t1, t2, …, tm}; (3) F⊂(P×T)∪(T×P) 是一段有向弧.

一个Petri网的标记是一个k维向量mNk, 其中, m[i]表示当前状态下第i个库所里令牌的数量; 又, Petri网里的一条转移t可以用两个k维向量fh来进行表示, 其中, f表示消耗令牌的数量, h则表示产生令牌的数量.那么, 一个标记m可以经过转移fm', 当且仅当m'=m-f+n.

1.3 数据Petri网

数据Petri网[5, 6]是在Petri网上扩展的一个模型.一个数据Petri网中存在一个全序的数据集合, 而数据Petri网中的每个令牌都被映射到了其中一个数据上.数据Petri网有如下的定义.

定义1.3.一个k维的数据Petri网是一个元组PDN=(P, T, F, H), 其中,

(1) P是有限的库所集合P={p1, p2, …, pk};

(2) T是有限的转移标记集合T={t1, t2, …, tm};

(3) $F = \bigcup\nolimits_{t \in T} {{F_t}} ,H = \bigcup\nolimits_{t \in T} {{H_t}} $, 其中, Ft, Ht∈(Nk)*; 并且对于每个tT, Ft, Ht都具有相同的长度n; 并且Ft(i), Ht(i)∈Nk, 其中, i∈[n].

一个数据Petri网的标记是由 (D×Nk)*的字组成的.在数据Petri网的任何一个状态, 数据Petri网只有有限多个令牌, 因此, 对应的数据都只有有限多个.同时, 因为整个数据集是全序的, 不妨设为d1, d2, …, dn, 并且有d1 < d2 < … < dn.一个数据Petri网的标记是 (d1, v1)(d2, v2)…(dn, vn), 其中, vi是一个k维向量, 用来表示对应数据为di的令牌在各个库所的数量.注意到, 只需要关注数据之间的大小关系, 因此可以再一步简化数据Petri网的标记为v1v2vn.令m=v1v2vn是数据Petri网的一个标记, 则m的一个0拓展是m'=u0v1u1v2un-1vnun, 其中, ui∈(Nk)*是一串Nk上的字.

mm'是数据Petri网的两个标记, t是数据Petri网的一个转移, 并且长度为n.如果有下列条件满足:

1) 存在m的一个拓展u0v1u1v2un-1vnun, 其中, ui∈(Nk)*;

2) viFt(i);

3) 存在m'的一个0拓展${u_0}{v'_1}{u_1}{v'_2}...{u_{n - 1}}{v'_n}{u_n}$, 使得${v'_i} = {v_i} - {F_t}(i) + {H_t}(i),$则称标记m可以触发转移tm', 并记为mtm'.同样地, 如果标记m经过一连串的转移序列t1t2tn, 使其到达标记m', 便记其为m*m'.

问题1.1 (数据Petri网的可覆盖性问题).给定一个数据Petri网PDN=(P, T, F, H), 一个初始标记mini=v1v2vn和标记$m' = {v'_1}{v'_2}...{v'_n}$, 则数据Petri网的可覆盖性问题是指是否存在一系列的转移序列t1t2tn, 使得mini*mm'.

对于该问题的研究, 在文献[6]中已经有了详细的结论, 这里将使用其中的结论来证明通信Petri网的可覆盖性的相关问题.

定理1.1 (文献[6], Theorem4.1.a).数据Petri网的可覆盖性问题和终止性问题是可判定的.

2 通信Petri网

通信Petri网的定义是在普通Petri网的基础上增加了相互通信的能力, 同时抽象了栈的概念.它通过赋予每个库所一个二维向量, 用以记录收发信息的信息.可以认为:在通信Petri网中, 每个令牌有一个二维向量的标示符, 而这个标示符的全集是一个N2全集.有如下的形式化定义.

定义2.1.一个通信Petri网是一个元组 (tuple):CPN=(P, T, H, In, Out, f, α), 其中,

(1) P是有限的库所集合P={p1, p2, …, pk};

(2) T是有限的令牌集合T={t1, t2, …, tm};

(3) f是一个TN2的映射函数;

(4) $In = \bigcup\nolimits_{t \in T} {I{n_t}} $, 其中, Int∈(P×N)*;

(5) $Out = \bigcup\nolimits_{t \in T} {Ou{t_t}} $, 其中, Outt∈(P×N)*;

(6) $H = \bigcup\nolimits_{t \in T} {(I{n_t},t,n,Ou{t_t})} ,$其中n∈[N0];

(7) $\alpha \in {N^{{N_0}}}$是一个N0维的向量.

对于T中的每个转移t, 定义了IntOutt两个集合用以表示令牌的消耗与产生.特别地, 集合T只是给出了转移的标示符, 通信Petri网的一条转移是 (Int, t, n, Outt) 这样的形式, 其中, n表示可能会对全局向量α有相应的操作.与普通Petri网不同, 通信Petri网里定义了一个有关转移的函数f, 将在通信Petri网里的转移区分成了若干不同的方式.

一个通信Petri网的标记 (c, α) 是一个库所与对应令牌的多重集合的元组串和全局向量的二元串.

(c, α)=((p1, M1[N2])(p2, M2[N2])…(pk, Mk[N2]), α).

在这个模型中, 每当有一个转移t被触发时, 会产生一些令牌的消耗和一些令牌的产生, 同时也会产生一个新的标记$(c',\alpha ')(({p'_1},{M'_1}[{N^2}])({p'_2},{M'_2}[{N^2}])...({p'_k},{M'_k}[{N^2}]),\alpha ')$, 并将其记为 (c, α)→t(c', α'), 对于不是单个的转移触发, 记 (c, α)→*(c', α'), 当且仅当存在一连串的转移序列t1t2tn, 使得:

$ (c,\alpha ){ \to _{{t_1}}}({c_1},{\alpha _1}){ \to _{{t_2}}}({c_2},{\alpha _2}){ \to _{{t_3}}} \cdots { \to _{{t_{n - 1}}}}({c_{n - 1}},{\alpha _{n - 1}}){ \to _{{t_n}}}(c',\alpha '). $

在通信Petri网中, 有一个映射转移t到一个二维向量上的函数f, 函数将转移分成了5类.

·有一类转移与普通的Petri网相同, 表示令牌在库所之间的转移;

·有两类则与全局向量α有关:其中一类需要对α开始做加法, 即会使α的某些分量增加, 见第1种规则; 另一类需要对α做减法, 即会使α的某些分量减少, 见第2种规则; 且整个模型中, 要保持α始终大于等于0;

·还有两类转移, 对参与转移消耗的令牌产生一些形式上的改变.

形式化地, 对于一个转移t, 如果:

1) 若f(t)=(a, 0), 其中, a > 0并且Int, OuttP×N, 则有:

$ \frac{{(I{n_t} = ({p_i},m),t,n,Ou{t_t} = ({p_j},m)) \in H}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中,

(1) 如果ki, j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}]$;

(2) 如果k=i, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}]$, 其中, M[Ek1]⊆Mk[Ek], M[Ek1]是Mk[Ek]的一个子集, 满足Ek1Ek并且|M[Ek1]|=m;

(3) 如果k=j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k1}}]$;

(4) 如果k=n, 则当α'[k]=α[k]+m×f(t)[1];kn时, α'[k]=α[k].

2) 若f(t)=(0, a), 其中, a > 0并且Int, OuttP×N, 则有:

$ \frac{{(I{n_t} = ({p_i},m),t,n,Ou{t_t} = ({p_j},m)) \in H \wedge \alpha [n] - m\& f(t)[2] \geqslant 0}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中,

(1) 如果ki, j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}]$;

(2) 如果k=i, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}]$, 其中, M[Ek1]⊆Mk[Ek], M[Ek1]是Mk[Ek]的一个子集, 满足Ek1Ek并且|M[Ek1]|=m;

(3) 如果k=j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k2}}]$, 其中, M[Ek2]={a|a[2]=a'[2]+f(t)[2], a'∈M[Ek1]};

(4) 如果k=n, 则当α'[k]=α[k]-m×f(t)[2];kn时, α'[k]=α[k].

3) 若f(t)=(0, 0), 并且Int, Outt⊆(P×N)*, 则有:

$ \frac{{(I{n_t},t,n,Ou{t_t}) \in H}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中,

(1) 如果 (p, _)∉Int, Outt, 则${M'_k}[{E'_k}] = {M_k}[{E_k}]$;

(2) 如果 (pk, m)∉Int, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}]$, 其中, M[Ek1]⊆Mk[Ek], M[Ek1]是Mk[Ek]的一个子集, 满足Ek1Ek, 并且|M[Ek1]|=m;

(3) 如果 (pk, m)∉Outt, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k2}}] + M[\{ a,0\} ]$, 其中, M[Ek2]⊆M[Ek1], M[Ek2]是M[Ek2]的一个子集, 满足Ek2Ek1, {(a, 0)}={(a, 0)|(a, _)∈M[Ek1]}, 并且两个多重集合满足|M[Ek2]|+|M[(a, 0)]|=m, 且M[Ek2]互不相交;

(4) α'=α.

4) f(t)=(a, b), 其中, a > b > 0并且Int, OuttP×N, 则有:

$ \frac{{(I{n_t} = ({p_i},m),t,n,Ou{t_t} = ({p_j},m)) \in H}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中,

(1) 如果ki, j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}]$;

(2) 如果k=i, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}]$, 其中, M[Ek1]⊆Mk[Ek], M[Ek1]是Mk[Ek]的一个子集, 满足Ek1Ek并且|M[Ek1]|=m;

(3) 如果k=j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k2}}]$, 其中, M[Ek2]={a|a[1]=a'[1]+f(t)[1], a'∈M[Ek1]};

(4) α'=α.

5) f(t)=(a, b), 其中, b > a > 0并且Int, OuttP×N, 则有:

$ \frac{{(I{n_t} = ({p_i},m),t,n,Ou{t_t} = ({p_j},m)) \in H}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中,

(1) 如果ki, j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}]$;

(2) 如果k=i, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}]$, 其中, M[Ek1]⊆Mk[Ek], M[Ek1]是Mk[Ek]的一个子集, 满足Ek1Ek并且|M[Ek1]|=m;

(3) 如果k=j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k2}}]$, 其中, M[Ek2]={a|a[1]=a'[1]+f(t)[1], a'∈M[Ek1]};

(4) α'=α.

直观而言, 第3种形式的转移与普通Petri网的转移是相同的, 都是把一些库所的令牌转移到另一些库所, 并且会在某些库所生成一些新的令牌, 某些令牌也会消失掉.只不过, 在通信Petri网这个模型里, 因为每个令牌是一个二维向量, 因此可能会有无限多种令牌, 因而需要用多重集合的方式来进行描述.

前两种形式的转移会对全局向量α:第1种形式下, 在通信Petri网上的转移会增加整个模型全局向量α的值; 而在第2种形式下, 转移的发生同时需要向量α保持一定的大小, 使得减小后的向量α'依旧是一个在${N^{{N_0}}}$的向量, 同时使得参与转移的令牌的第2维数值加1.而后两种转移则会对令牌的第1维数值产生影响:第4种转移会减少令牌的第1维向量, 而第5种转移则会增加令牌的第1维向量.

在关于转移的形式化定义里, 有意省略了一些除了第3种形式下的转移, 包括限制住了这些转移的IntOutt以及对于普通令牌迁移的情况.在上述定义中, 除了第3种转移以外, 其余4种转移每次相当于只能从一个库所里消耗令牌, 再在一个库所里产生新的令牌.第3种转移则并没有作这方面的限制, 并且我们可以假设令牌的转移和生成在第3种规则下是固定的, 即:对于第3类规则, 比如 ((p, 1), t, 1, (q, 1)(m, 2)), 我们在库所p中消耗掉一个 (1, 2) 的令牌, 可以假定这个令牌转移到了m库所里, 而在qm库所里则各自生成了一个 (1, 0) 的令牌.由于有第3种转移的能力, 因此这种省略并不会影响模型本身的能力, 并且有助于理解这个模型.事实上, 考虑一个夹杂了普通令牌迁移和多个IntOutt的转移t的情况, 只需要注意:由于一个通信Petri网里的转移 (Int, t, n, Outt) 只有有限多个, 因此可以定义出一个新的通信Petri网, 添加一些新的库所与转移, 可以将原来复杂的转移t分开来变成若干步线性的转移, 分别处理普遍令牌的迁移和IntOutt的转移, 使得这个新模型里所有的转移都符合上面所定义的转移.

特别地, 继续来限定一下模型, 即使令fT→{(0, 0), (1, 0), (0, 1), (2, 1), (1, 2)}, 所定义出来的模型也有着相同的能力.原因也很简单, 就是因为转移仅仅只有有限多个.对于初始的通信Petri网, 假设存在1个转移t使得f(t)= (m, 0), 便可以在新的通信Petri网上针对这个转移t构建m个辅助转移的转移t1, t2, …, tm与辅助的库所f(ti)=(1, 0), 使得原来的通信Petri网上转移t被触发当且仅当新构建的通信Petri网t1, t2, …, tm这一系列的转移.因此在接下来的讨论中, 要使得通信Petri网里映射转移的函数fT→{(0, 0), (1, 0), (0, 1), (2, 1), (1, 2)}.

3 通信Petri网与异步通信程序

现在来介绍通信Petri网与异步通信程序之间的联系.对于我们所研究的程序, 它有如下特点:(1) 函数存在没有记忆能力的函数调用; (2) 存在spawn操作, 也即开一个新的线程; (3) 程序之间存在异步通信, 并且用来通信的信道和信息类型都只有有限个.其中, 没有记忆能力的函数调用对于调用次数不敏感, 比如一个函数A自我调用, A调用k次和A调用m次在程序栈的表示上是没有区别的.这里, 我们以文前中给出的程序为例来加以说明.我们考虑student() 函数, 注意到, 其两个student() 进程里不会产生内部的联系, 因此最后一句student() 对自己的调用次数不会在程序栈上有不同的表示.在student() 函数里, 其对自己调用的次数并不敏感.注意到:因为每一个线程都有一个栈, 而多栈的系统图灵等价, 因此没有记忆能力的栈是对原来栈的一种抽象, 这样的抽象没有实现限定栈深度, 因而要比k-型更加一般化.

在通信Petri网中, 将每个库所视作程序中的某个状态, 而一个令牌代表了程序的一个线程, 令牌的转移则表示通过程序的执行, 每个线程会达到程序中的不同状态.这样, 新令牌的产生便能表示新开线程操作的产生, 而程序本身的运行便能体现在整个模型里面.比如在上例中, setup_network() 中第1行的spawn函数便可认为是在通信Petri网中新增加了一个令牌.还需要说明的是如何编码整个通信, 这一点我们通过通信Petri网的全局向量α来完成.在通信Petri网的转移中, 使得f(t)=(0, 1) 的转移则可以理解为一个程序接受一个消息, 收取信息的时候便会在第2维向量加1, 也就是一个令牌所对应的第2维向量存储了收取信息的数量.同样, 以文前的例子来进行说明.在本文开始部分, 我们已经假设共有k种信息, 图 1图 2中给出的程序一共有3个信道, 因此我们要用一个3k维的向量来进行模拟, 并且假设3个信道的顺序是toResource, toStudents和toTeacher, 则第i×k+j维上的数值就表示为第 (i+1) 个信道上第j种信息的数量.当student() 函数企图从toStudents上接受第1种信息的时候, 通信Petri网就可以检测第k+1维上的值是否为0以决定是否能够收到相关的信息.如果大于0, 则通过将这一维向量减1的方式表示该信息已被接受; 发送信息可以作类似的考虑.由于只需要在对应维度上做加法, 因此不会使得程序无法进行.此外, 注意到, 信道上的内容是全局的, 因此在通信Petri网中, 我们使用全局向量α来模拟.而对于每个令牌来说, 每当进行一次程序调用时, 自身的第1维向量便会加1进行存储, 结束调用时, 第1维向量减1.这里需要考虑如何模拟程序的运行, 我们将令牌视作一个线程, 而程序的模拟则通过令牌在库所间的游走来加以表示.这里, 为了考虑函数调用以及通信的能力, 我们在每个令牌里记录了调用层数与收取信息的数量.之前已经提到, 第2维记录了收取信息的数量, 而令牌的第1维则记录了调用的层数.在这样的编码下, 一个满足上述条件的程序便可以编码到通信Petri网上, 并且不妨限定每次只有一个消息的传送和接收.

形式化地来说, 对于一段异步通信程序, 假设一共有A1, A2, …, An个函数, 其中, 每个函数Ai共有ai行语句.接下来构造如下$\sum {n{a_i}} $个库所, 记为Aijk, 其中, i, j∈[n], k∈[aj].库所Aijk的意思是指, 函数Ai调用函数Aj进行至第k行语句的状态.其次, 假设程序共有k个信道和m种信息, 则添加一个k×m维的向量α, 用以表示信息在进程间的传递, 初始状态下, α为零向量.每当向第i个信道发送第j种信息时, 则α[(i-1)×m+j]加1;而需要从第i个信道接受第j种信息时, α[(i-1)×m+j]减1.在经过这样的编码后, 程序已将程序交互上信息的存储与控制流所能达到的状态编码到了通信Petri网上的状态和全局向量上.接下来将考虑程序的动作如何编码至转移上去.

令通信Petri网的转移根据之前的介绍分为规则1~规则5.对于原程序的一条语句, 如果产生了信息的发送, 则添加一条规则1, 令牌在转移的同时, 使全局向量的对应分量加1;如果需要接受信息, 则添加一条规则2, 令牌在能转移的同时, 使全局向量的对应分量减1, 并且使得转移的令牌的第2维值加1;当程序产生函数调用的时候, 添加一条规则4, 除了令牌的转移以外, 令转移的令牌的第1维值加1, 与状态一起模拟该线程的程序栈; 而程序结束函数调用的时候, 则添加一条规则5, 令转移的令牌的第1维值减1;每当需要产生一个新的线程的时候, 产生一条规则3, 使得产生一个新的第1维值相同, 第2维值为0的令牌; 其余情况只需要根据程序的正常执行产生对应令牌的相应转移即可.这样, 便把一个异步通信程序编码到了通信Petri网上, 并且模型上的一个令牌便代表了一个线程, 令牌在模型里的转移则代表了程序的控制流, 其中, 令牌的第1维和令牌所处的状态则刻画出一种受限制的程序栈, 也就是没有记忆能力的程序栈.

而对于异步通信程序的研究, 验证方法关注的兴趣在于是否存在一些不期望见到的程序运行状态.比如, 假设以行号来表示标记程序运行到的状态, 则是否会存在两个学生在调用分析作业的时候同时运行到行号20的状态产生, 也就是说, 是否会发生死锁的行为, 亦即一个不期望达到的状态, 验证方法便是去检验这样的状态是否会发生.对于这一点, 接下来会加以说明, 这个问题可以通过研究通信Petri网的可覆盖性问题来得到解决.

问题3.1.给定一个通信Petri网k-CPN=(P, T, H, In, Out, f, α) 和它的一个初始标记 (cini, αini)=((p1, M1[N2])(p2, M2[N2])…(pk, Mk[N2]), αini) 以及一个目标标记$(c,\alpha ) = (({p'_1},{M'_1}[{N^2}])({p'_2},{M'_2}[{N^2}])...({p'_k},{M'_k}[{N^2}]),\alpha ).$如果存在一个转移序列t1t2tn使得 (cini, αini)→*(c', α'), 其中满足c'≥c, 则称 (CPN, cini) 能覆盖住c.因此, 通信Petri网的可覆盖性问题便是是否存在这样一个满足要求的c', 使得 (cini, αini)→*(c', α'), 其中满足c'≥c.

事实上, 基于之前给出的异步通信程序到通信Petri网的编码不难发现:程序会达到某个不期望的“坏”状态, 当且仅当编码后的通信Petri网会达到一个状态可以覆盖掉这个不期望的“坏”状态的标记.

需要注意的是:在通信不受限制的情况下, 通信Petri网的可覆盖性问题是不可判定的.

接下来将在通信Petri网上增加一种比较自然的限制, 对于每个令牌来说, 它所代表的二维向量的第2维会被一个预先给定的固定常数k所绑定.这种限制对于这种模型来说是合理的, 因为考虑到在异步通信程序中, 很多程序尽管会有不受次数限制的消息发送与接收, 然而对于每个线程来说, 它接受信息的次数是被绑定的.比如, 在前文给出的程序中, 对于每个函数来说, 它只会接受有限多次信息, 因而这样的程序便满足了这个限制.

定义3.2.一个k-型限制下的通信Petri网是一个通信Petri网元组k-CPN=(P, T, H, In, Out, f, α), 设定由初始标记cini出发, 定义集合Reach={c|(cini, αini)→*(c', α')}, 使得Reach≥{(pi, (0, k))}不成立.

通信Petri网可以通过修改转移的语义来完成这一限制, 事实上, 只需要修改满足f(t)=(0, 1) 的转移t.

$ \frac{{(I{n_t} = ({p_i},m),t,n,Ou{t_t} = ({p_j},m)) \in H \wedge \alpha [n] - m\& f(t)[2] \geqslant 0}}{{(({p_1},{M_1}[{E_1}])...({p_k},{M_k}[{E_k}]),\alpha ) \to (({p_1},{{M'}_1}[{{E'}_1}])...({p_k},{{M'}_k}[{{E'}_k}]),\alpha ')}}, $

其中, (1) 若ki, j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}];$(2) 若k=i, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] - M[{E_{k1}}],$其中, M[Ek1]⊆Mk[Ek], |M[Ek1]|=m; 并且对于M[Ek1]中的任意一个元素a, a[2]≤k-1;(3) 若k=j, 则${M'_k}[{E'_k}] = {M_k}[{E_k}] + M[{E_{k2}}],$其中, M[Ek2]={a|a[2]=a'[2]+f(t)[2], a'∈M[Ek1]}, 并且a'[n]= a[n]-m×f(t)[2].

在本节的最后, 我们将用一个例子来简单阐述程序到模型的转换, 如图 3所示.

Fig. 3 An example transition 图 3 一个转换的例子

图 3中左边是一个简单的程序, AB两者的区别是, 一个是先发信息再接收信息, 另一个是先接收信息再发信息.图 3中右图则是通信Petri网的一个编码, 注意到, 只有C一个信道和ready一个信息, 该全局变量α是一维的.整个编码与程序的控制流是非常相似的.这里, 库所的名字与左边程序的行号直接挂钩.另外, 如果一个令牌在库所pi里, 则表示这个令牌所代表的进程运行到了第i行, 则这个程序能否return便取决于库所p2里是否能有令牌.

4 k-型限制下的通信Petri网到数据Petri网的编码

本节将给出k-型限制下的通信Petri网的可覆盖性可判定性的证明, 证明的核心思路是:通过说明在k-型限制下的通信Petri网中每个令牌所对应的一个二维向量可以认为是在全序集上的一个映射, 从而证明受限的通信Petri网的可覆盖性问题可以规约到数据Petri网的可覆盖性问题上, 而数据Petri网的可覆盖性问题可以通过规约至良序转移系统 (WSTS) 的可覆盖性问题上, 从而证明其是可判定的[6].

直观上来理解, 数据Petri网的拓展是将令牌直接绑定到了一个数据集上的一个数据, 而在每次转移的过程中, 令牌绑定的数据可能会发生变化, 但这个变化是由规则绑定的, 所以尽管有无穷多种令牌, 但是由于有限条规则的限制, 使得数据的变化是有限种.对于通信Petri网上性质的证明正是利用了这一点, 使得在k-型限制下的通信Petri网能够规约到数据Petri网的问题上.

给定一个k-型限制下的通信Petri网k-CPN=(P, T, H, In, Out, f, α) 和它的一个初始标记 (cini, αini)=((p1, M1[N2])(p2, M2[N2])…(pk, Mk[N2]), αini) 以及一个目标标记$(c,\alpha ) = (({p'_1},{M'_1}[{N^2}])({p'_2},{M'_2}[{N^2}])...({p'_k},{M'_k}[{N^2}]),\alpha ),$其转换为一个数据Petri网的可覆盖性问题说明如下.

第1步, 将k-CPN的全局向量α编码进库所里.额外地, 令d个库所pm1, pm2, …, pmd, 其中, d为向量α的维度, 每当存在一条需要对α做加法的转移t, 即 (Int, t, n, Outt), 则将在转移t出发后, 在pmn里产生一个向量为 (0, 0) 的令牌; 每当存在一条需要对α做减法的转移t, 即 (Int, t, n, Outt), 则将在转移t出发后, 在pmn里消耗一个向量为 (0, 0) 的令牌.在这些额外的d个库所中, 由于是被用来相当于当成信道存储程序发送的信息, 因此特别令在这些额外的d个库所中的令牌所代表的向量都是一样的.所以通过额外的d个库所的编码, 便将全局向量α编码进了库所.

第2步, 将每个令牌所代表的第2维向量编码进库所里.这一点由于有k-型限制, 可如下实现.

对于原先通信Petri网的每一个库所pi, 定义对应的k个库所pi1, pi2, …, pik, 其中, pij存储在原本通信Petri网的库所pi中存储的第2维向量j的令牌.在这样的情形下, 新的模型里的库所数量是原来通信Petri网的k倍.因为库所被分离了, 所以需要对现有的转移进行一些修改.下面根据原来的5类转移一一进行说明:第1、第3、第4和第5种转移是比较容易说明的, 事实上, 由于其不会修改里面库所中令牌第2维向量的值, 因此对于一个需要消耗在p1, p2, …, ps库所里的令牌并且在${p'_1},{p'_2},...,{p'_t}$库所里生成对应令牌的转移, 只需要添加类似的转移, 使得转移是需要消耗在${p_{1{i_1}}},{p_{2{i_2}}},...,{p_{s{i_s}}}$库所里的令牌并且在${p'_{1{i_1}}},{p'_{2{i_2}}},...,{p'_{t{i_t}}}$库所里生成对应令牌, 其中, im, jn∈[k].我们注意到:在这种情形下, 对于原先的一条转移, 由于第2维向量并没有发生变化, 因此为了在将第2维向量编码进状态的数据Petri网中模拟该转移, 我们需要考虑到所有的情况.简单来说, 比如:如果要消耗p1库所里的m1个令牌, 注意到, 这m1个令牌的第2维向量可能是0~k中的任一数字, 也就是说一共有${(k + 1)^{{m_1}}}$种情况, 对每个库所消耗的令牌进行考虑, 假设在pi库所里需要消耗mi个令牌, 则一共会有${(k + 1)^{\sum\limits_{i = 1}^s {{m_i}} }}$种不同的可能, 也就是说需要在数据Petri网中添加这么多种的转移.

现在来说明第2种转移的修改.注意到:这种类型的转移每次被触发时, 一个令牌的第2维向量只需要加1, 因此这种转移的添加也比较方便.对于属于第2种转移的t, 即 ((pi, m), t, (pj, m)) 这样一个转移, 只需要同样构造 ((pik, m), tk, (pj(k+1), m)) 的k条转移即可.图 4给出了一个在2-型下的通信Petri网的转移的修改方式.直观上来理解, 就是由于第2维向量是有限制的, 因此可以在状态里控制第2维向量.

图 4 一个2-型限制下的通信Petri网的转移修改

在对上述的转移进行修改以后, 编码已经将k-型限制下的通信Petri网的每一个令牌的第2维向量编码进库所里, 所以从现在开始, 将限定这里的每个令牌对应的只是一个自然数值.注意到, N是一个全序集, 因此可以采用数据Petri网使用的标记方法来表示现在一个通信Petri网下的标记.

最后将证明, 经过了如此变换的k-型限制下的通信Petri网是一个数据Petri网.事实上, 只需要说明每一个转移都可以表示成固定常数的一个Nk上的列即可.由于每次通信Petri网上的操作至多只需要对令牌所表示的向量完成+1, -1的操作, 也就是说, 每个通信Petri网下涉及到n个令牌的转移至多只需写成nNk上的列即可, 因此, 原本k-型限制下的通信Petri网已经被编码成了一个数据Petri网, 并且保证了两个模型所能产生的路径是相同的.现在来形式化整个过程.

定义4.1.给定一个k-型限制下的通信Petri网k-CPN=(P, T, H, In, Out, f, α), 其中,

1) P是一个有限的元素集合P={p1, p2, …, pm};

2) T是一个有限的元素集合T={t1, t2, …, tn};

3) αNd,

D(k-CPN) 所对应的一个k×m+d维的数据Petri网是一个元组PDN=(P', T', F, H), 其中,

1) P'={P11, P12, …, P1k, P21, …, Pm1, Pm2, Pmk, Pmsg1, Pmsg2, Pmsgd};

2) 对于k-CPN中的每个转移t:

ⅰ) 如果f(t)=(1, 0), (Int=(pi, 1), t, n, Outt=(pj, 1))∈H, 则{t1, t2, …, tk}⊆T', 并且Ftl, HtlNk×m+d, 其中, Ftl((i-1)×k+l)=1, 其余为0;Htl((j-1)×k+l)=1, Htl(m×k+n)=1, 其余为0.

ⅱ) 如果f(t)=(0, 1), (Int=(pi, 1), t, n, Outt=(pj, 1))∈H, 则{t1, t2, …, tk}⊆T', 并且Ftl, Htl∈(Nk×m+d)2, 其中, Ftl[1]((i-1)×k+l)=1, Htl[1](m×k+n)=1, 其余为0;Htl[2]((j-1)×k+l)=1, 其余为0.

ⅲ) 如果f(t)=(0, 0), 并且 (Int=(pi1, 1)(pi2, 1)…(pip, 1), t, n, Outt=(pj1, a1)(pj2, a2)…(pjq, aq))∈H, 则$\{ {t_{11}},...,{\text{ }}t_{12}^{p - 1},{t_{21}},...,t_{k2}^{p - 1}\} \in T',$并且对于$x \in [k],y \in \left[ {\sum\limits_{i = 0}^{n - 1} {(p,i)} ,\sum\limits_{i = 0}^n {(p,i)} } \right),{F_{txy}},{H_{txy}} \in {({N^{k \times m + d}})^n},$其中, pi1, pi2, …, pip重新记标号为P11, P12, …, P1b1, P2b2, …, Pnbn.其中, $\sum\limits_{i = 1}^n {{b_i}} = p,$Ftxy[c]((id-1)×k+x)=1, pid被重新记为pce, 其余为0;

Htxy[c]((jd-1)×k+x)=1, Htxy[c]((jd-1)×k+1)=ad-1, 其余为0.

ⅳ) 如果f(t)=(2, 1), (Int=(pi, 1), t, n, Outt=(pj, 1))∈H, 则{t1, t2, …, tk}⊆T', 并且Ftl, Htl∈(Nk×m+d)2, 其中, Ftl[2]((i-1)×k+l)=1, 其余为0;Htl[1]((j-1)×k+l)=1, 其余为0.

ⅴ) 如果f(t)=(1, 2), (Int=(pi, 1), t, n, Outt=(pj, 1))∈H, 则{t1, t2, …, tk}⊆T', 并且Ftl, Htl∈(Nk×m+d)2, 其中, Ftl[1]((i-1)×k+l)=1, 其余为0;Htl[2]((j-1)×k+l)=1, 其余为0.

ⅵ) Fd1, Hd1, Fd2, Hd2∈(Nk×m+d)2, 其中, Fd1[2](m×k+d)=1, 其余为0;Hd1[1](m×k+d)=1, 其余为0;Fd2[1](m×k+d)=1, 其余为0;Hd2[2](m×k+d)=1, 其余为0.

定义4.2.定义函数m:(P, M1[N2])*×Nd→(Nk×m+d) 和函数h:(P×M1[N2])*N, 其中,

1) $h(c) = \max {\text{ }}d,\prod\nolimits_{{M_i}} {(d,\_)} > 0$;

2) m(c, α)∈(Nm×k+d)k(c), 其中, m(c, α)[i](k×(a-1)+j)=d, 如果在c$\prod\nolimits_{{M_a}} {((i,j))} = d.$特别地,

$ \sum {m(c,\alpha )[i](k \times m + j)} = \alpha [j]. $

我们对这两个函数定义进行一定的说明.h函数实际上是一个作用在一个通信Petri网的标记上的函数, 返回在该通信Petri网当前标记下令牌中第1维向量的最大值.这个函数的作用在于服务接下来的m函数.实际上, m函数是一个通信Petri网标记转换成将令牌第2维编码进状态的数据Petri网标记的转换函数.也就是说, 如果 (c, α) 是k-型限制下的通信Petri网的一个标记, 则m(c, α) 是D(k-CPN) 上对应的一个标记.并且由m函数的定义, 我们不难定义出m函数的逆函数m-1:(Nk×m+d)*→(P, M1[N2])*×Nd.关于这两个函数, 我们有如下的性质.

命题4.1.对于函数h, m以及其逆函数m-1, 我们有如下性质.

1.对任意c, c'∈(P, M1[N2])*, 如果有cc', 我们有h(c)≥h(c');

2. (c, α) 是k-型限制下的通信Petri网的一个标记, 则m(c, α) 是D(k-CPN) 上对应的一个标记;

3.对任意d, d'∈(Nk×m+d), 并且m-1(d)=(c, α), m-1(d')=(c', α'), 若 (c, α)=(c', α'), 则对∀iN, ∀jN, 有: d[i](j)=d'[i](j);

4.对任意 (c, α), (c', α')∈(P, M1[N2])*×Nd, cc', 当且仅当m(c, α)[i](j)≥m(c', α')[i](j), 其中, i∈[h(c)], j∈[k×m].

证明:从函数h, m和函数m-1的定义不难得到.

1.由函数h的定义立即得出;

2.由函数m的定义及D(k-CPN) 的定义立即得出;

3.因为有m-1(d)=m-1(d'), 因此有c=c', 所以对于任意的i+k×j∈[k×m], $\prod\nolimits_{{M_i}} {((a,j))} = \prod\nolimits_{{{M'}_i}} {((a,j))} $对任意a均成立.因而有d[a][i×k+j]=d'[a][i×k+j];

4.由cc'可知:对于任意的 (i, j)∈N2, 有$\prod\nolimits_{{M_a}} {((i,j))} \geqslant \prod\nolimits_{{{M'}_a}} {((i,j))} $, 其中, a∈[m], j∈[k], 因此对于任意的i0∈[h(c)], j0∈[k×m], 有m(c, α)[i0](j0)≥m(c', α')[i0](j0); 反之, 同理.因而结论成立.

接下来将说明k-型限制下的通信Petri网k-CPN和一个对应的数据Petri网D(k-CPN) 之间的关系.

引理4.1.对于一个k-型限制下的通信Petri网k-CPN和一个对应的数据Petri网D(k-CPN) 以及k-CPN的两个标记 (c, α), (c', α'), (c, α)→(c', α') 当且仅当在D(k-CPN) 中m(c, α)→m(c', α').

证明:只需证明对于在k-CPN上 (c, α)→(c', α'), 当且仅当在D(k-CPN) 上dd', m(c, α)=d, m(c', α')=d'.

(⇒) 的证明:

假设 (c, α)→t(c', α'), 并且

$ \begin{align} & (c,\alpha )=(({{p}_{1}},{{M}_{1}}[{{N}^{2}}])({{p}_{2}},{{M}_{2}}[{{N}^{2}}])...({{p}_{k}},{{M}_{k}}[{{N}^{2}}]),\alpha ),({c}',{\alpha }')= \\ & (({{p}_{1}},{{{{M}'}}_{1}}[{{N}^{2}}])({{p}_{2}},{{{{M}'}}_{2}}[{{N}^{2}}])...({{p}_{k}},{{{{M}'}}_{k}}[{{N}^{2}}]),{\alpha }'). \\ \end{align} $

接下来将说明存在D(k-CPN) 的一条转移t', 使得m(c, α)→t'm(c, α)', 并且m(c, α)'=m(c', α').其中, m(c, α)'表示为m(c, α) 作转移t'后新的数据Petri网的标记.这里, 以第1类、第3类转移作为说明, 其余3类转移的说明是类似的, 这里不再重复.

1) 如果f(t)=(1, 0), (Int=(pi, 1), t, n, Outt=(pj, 1))∈H, 则存在一个大小为1的多重集合M[N2], 使得:

Mj'[N2]=Mj[N2]+M[N2], Mi'[N2]=Mi[N2]+M[N2], α'[n]=α[n]+1.

M[N2]={(b, e)}.由D(k-CPN) 的构造可知, 存在Ft', Ht'Nk×m+d, Ft'((i-1)×k+e)=1, Ht'((j-1)×k+e)=1, Ht'(m×k+n)= 1.在m(c, α) 中考察第b个向量m(c, α)[b], 注意到 (b, e)∈Mi[N2], 因此, 由m的规则, m(c, α)[b](k×(i-1)+e) > 0.因此, m(c, α) 可作该条转移t', 使得m(c, α)'满足:

$ \begin{gathered} m(c,\alpha )'[b](k \times (i - 1) + e) = m(c,\alpha )[b](k \times (i - 1) + e) - 1, \hfill \\ m(c,\alpha )'[b](k \times (j - 1) + e) = m(c,\alpha )[b](k \times (j - 1) + e) + 1, \hfill \\ m(c,\alpha )'[b](k \times m + n) = {\text{ }}m(c,\alpha )[b](k \times m + n) + 1. \hfill \\ \end{gathered} $

其余位置与m(c, α) 相等.

另一边, 由于$\alpha '[n] = \alpha [n] + 1,\prod\nolimits_{{{M'}_i}} {(b,e)} = \prod\nolimits_{{M_i}} {(b,e)} - 1,\prod\nolimits_{{{M'}_j}} {(b,e)} = \prod\nolimits_{{M_j}} {(b,e)} + 1,$因此, 由定义m(c', α'), 满足:

$ \begin{gathered} m(c',\alpha ')[b](k \times (i - 1) + e) = m(c,\alpha )[b](k \times (i - 1) + e) - 1, \hfill \\ m(c',\alpha ')[b](k \times (j - 1) + e) = {\text{ }}m(c,\alpha )[b](k \times (j - 1) + e) + 1, \hfill \\ m(c',\alpha ')[b](k \times m + n) = m(c,\alpha )[b](k \times m) + n) + 1. \hfill \\ \end{gathered} $

其余位置与m(c, α) 相等.因此有m(c, α)'=m(c', α').

2) 如果f(t)=(0, 0), 并且 (Int=(pi1, 1)…(pip, 1), t, n, Outt=(pj1, a1)…(pjq, aq))∈H, 则存在p个大小为1的多重集合Mu[N2].令Mu[N2]={(bu, eu)}, 使得Miu'[N2]=Miu[N2]-Mu[N2]Mjk'[N2]=Mjk[N2]+Mu[N2]+M[{(bu, 0)}], 并且|M[{(bu, 0)}]|=ak-1.不妨令bik个不同的值.由D(k-CPN) 的构造可知, 存在Ft, Ht∈(Nk×m+d)k, 使得Ft[g]((i-1)×k+e)=1, Ht[g]((z-1)×k+e)=1, Ht[g]((i-1)×k+1)=ai-1.其中, i, g满足bi在这p个值里排在第g小的位置, z=js.由于h(c)≥max bi, 因此在m(c, α) 中存在k个位置上的向量, 使得m(c, α)[xi]≥Ft[i], 于是, m(c, α) 可作该条转移t', 使m(c, α)'满足:

$ \begin{gathered} m(c,\alpha )'[{x_i}]((i - 1) \times k + {e_i}) = m(c,\alpha )[{x_i}]((i - 1) \times k + {e_i}) - 1, \hfill \\ m(c,\alpha )[{x_i}]({k_i} - 1) \times k + {e_i}) = m(c,\alpha )[{x_i}](({k_i} - 1) \times k + {e_i}) + 1, \hfill \\ m(c,\alpha )'[{x_i}](({k_i} - 1) \times k + 1) = m(c,\alpha )'[{x_i}](({k_i} - 1) \times k + {e_i}) + {\text{ }}{a_i} - 1. \hfill \\ \end{gathered} $

其余与m(c, α) 相等.

另一方面, 由Mjk'[N2]的变化及m函数的定义可知:

$ \begin{gathered} m(c',\alpha ')[{x_i}]((i - 1) \times k + {e_i}) = m(c,\alpha )[{x_i}]((i - 1) \times k + {e_i}) - 1, \hfill \\ m(c',\alpha ')[{x_i}](({k_i} - 1) \times k + {e_i}) = {\text{ }}m(c,\alpha )[{x_i}](({k_i} - 1) \times k + {e_i}) + 1, \hfill \\ m(c',\alpha ')[{x_i}](({k_i} - 1) \times k + 1 = m(c',\alpha ')[{x_i}](({k_i} - 1) \times k + {e_i}) + {\text{ }}{a_i} - 1. \hfill \\ \end{gathered} $

其余位置与m(c, α) 相等.

因此有m(c, α)'=m(c', α').因此由归纳假设, 结论成立.

(⇐) 的证明:

反过来的证明是相对比较容易的, 只要注意到:对于D(k-CPN) 的每个转移t, 都是由原先通信Petri网上的一个转移t生成而来.因此, 如果在D(k-CPN) 上有dd', 在k-CPN上即有m-1(d)→m-1(d').

因此, k-型下的通信Petri网可覆盖性问题规约到了数据Petri网的可覆盖性问题上去.由引理4.1、定理1.1, 便得到了下面的定理.

定理4.1. k-型限制下的通信Petri网的可覆盖性问题是可判定的.

5 相关工作

异步通信程序分析理论与方法是最近几年计算机理论和程序理论研究者关注的热点, 研究者们针对上述5个无限状态因素进行限制和抽象, 目前主要的研究分支和研究结果如下.

·限制递归.

即:每个进程不允许函数调用, 同时假设各个进程通过无界容量的无序缓存进行通信.这样的系统是异步通信系统, 其可覆盖性可通过规约至Petri网的可覆盖性, 因此是可判定的[7].基于该模型, 研究者们设计了一个Erlang语言的分析器Soter[8].文献[9]中, 研究者对递归进行了k-型的限制, 在这样的情况下, 同时对输入通信的次数进行有界限制, 系统的可覆盖性依然可判定, 且表达能力严格超过Petri网, 达到Tower完备[9].

·限制并发.

假设只有一个处理器执行程序, 且线程执行时不允许被挂起, 也即假设异步并发程序可以线性化.在这种限制下, 只有一个程序栈就足够了.即使这样的模型, 其表达能力依然很强, 是否是图灵完备目前仍然是一个开放问题.文献[2]在上述限制的同时, 对通信也进行了限制——只有在栈空的时候才能发生通信, 这样的程序模型的状态可达性 (EXPSPACE难)[2]和可覆盖性[10]是可判定的.

·限制通信.

最极端的限制方法是不允许不同线程间进行通信, 这样的程序也即异步程序.在这样的限制下, 模型的可覆盖性可以通过规约至Petri网的可覆盖性得到可判定的结论[11], 其活性 (liveness) 可以通过规约至Petri网的可达性, 因此也是可判定的[12].文献[13]详尽地列出了在不允许通信的情况下, 各种程序模型子集的判定性结论, 对应于不同的程序类型.对于这样的程序模型系统, 研究者开发了一个程序分析器原型[14].最新的研究扩展了不允许线程之间的通信, 得到了一个限制性比较强的可判定性结论[6].

还有一类型研究是为了对异步的Web程序进行分析, 假设系统有一个主线程以及无界数量个同类型的辅线程, 通信只发生在主辅线程之间, 辅线程之间没有通信.因此, 辅线程可以参数化.这样的模型叫做参数化异步通信系统.文献[15]首次提出了这样的系统, 并给出这一系统的可覆盖性的复杂性上界是EXPSPACE的.最后, 可覆盖性被确定为PSPACE完备[16].在最新的研究成果中, 该系统的活性上界被证明是NEXPTIME的[17].同时, 一些更为扩展的模型的可判定性结论也被提了出来[18].

此外, 计算机理论界的一些研究也对本研究具有很强的借鉴作用, 比如最新的关于下推向量加法系统 (pushdown vector addition system)[19], 其实际表达是单进程异步通信程序模型的一个超集, 它的可判定结论可以直接影响后者的判定性结论.目前的研究成果是下推向量加法系统在一维情况下可覆盖性可判定[20], 这一结论尚不能指导异步通信程序的理论模型 (因为程序模型不可能只有一维向量).良结构传递系统[21]及其扩展[10, 22]也可以对程序模型的判定性结论起到指导以及证明作用, 其优点是可得到通用的证明过程, 但不足之处是很难得到复杂性结论以及可实现的算法, 因此不太被程序语言理论界所认可.

由这些研究可知, 目前大多数的可判定性结论都是规约至Petri网的, 因此使得这一古老的模型重新焕发新机.最近, 很多Petri网的高效验证器[23, 24]被研究开发出来, 作为程序分析器的引擎.文献[25]在不完备的情况下, 基于通过SMT-solver实现了基于模式检测的Petri网可覆盖性验证.文献[11]将异步程序的进程间数据流分析形式化成了一个AIFDS问题, 并提出了相应的算法.其结论表示:尽管解决该问题是EXPSPACE难的, 但在实际中效率还是相当快的.

在20世纪末, 大量Petri网的扩展模型也开始应用于并发程序.文献[26]提出了颜色Petri网 (coloured Petri net), 对同步的通信进行了研究.文献[27, 28]则提出了对象Petri网 (object Petri net), 对面向对象的程序进行了建模研究.近些年, 一些更为具体的应用方面的研究也已经产生.文献[8]针对Erlang语言提出了一个叫做Soter的自动研究工具, 文献[14]也提出了一个针对异步程序开发的程序分析器原型.

此外, 除了基于Petri网的研究, 在应用中也有不少其他方式的探索.文献[29]对MHP问题, 也就是问两个活动能否在程序里并发地进行这一基础的问题进行了探索, 并且在基于类x10语言上提出了一种静态MHP分析的算法, 有着较快的效率.文献[30]则对异步程序进行了依靠/保证 (rely/guarantee) 的抽象, 即, 每个异步进程都需要满足这两个断言.这样, 整个程序的正确性就依赖于这些断言需要被满足, 文献[30]基于此给出一些C语言中的例子.文献[31]为了能够编程有效的异步程序, 定义了一种高可靠的程序语言P#, 通过静态数据竞争检测等手段来满足有效的要求.

但是, 基于这样的模型存在着一些问题, 比如:目前, 所有的程序模型通信都不考虑传值 (value-passing); 在文献[3]中提出的异步通信下推系统 (asynchronous communicating pushdown systems) 中, 便将消息限制在了有限种; 文献[6]在对基于事件同步的异步程序分析的过程中, 也将消息种类作了限定, 因此无法表达和分析像future和promise这样的语言特性.再比如:目前, 所有模型也无法表达某线程是否可以知道所接受的信息是某个特定线程所发, 等等.因此, 研究者们希望研究出表达能力更强的理论模型来描述和分析异步通信程序.与此同时, 研究者们也希望能基于此模型开发出高效的验证器来自动实现这些程序的程序分析.

6 总结以及未来的工作

本文针对异步通信程序给出了一个抽象的模型通信Petri网来编码, 证明了在k-型限制下的通信Petri网的可覆盖性问题是可判定的, 并且简单地给出了一个复杂性的下界.通信Petri网是将交互与程序调用合理地加以分离, 更方便直观理解和实现.

未来的工作包括:

·在理论上, 我们希望得到更为一般化的可判定模型来对异步通信程序进行建模和验证; 同时验证其他性质, 比如活性.此外, 我们希望能对其与其他类似的模型做出能力上的比较, 希望能严格证明其是当前最大的可判定模型;

·在实现上, 我们希望能够通过该模型提出有效使用的算法, 以此实现强大的通信Petri网的验证工具和从Erlang语言到该工具的自动转化程序, 从而得到自动化Erlang语言的验证工具.

参考文献
[1] Ramalingam G. Context-Sensitive synchronization-sensitive analysis is undecidable. ACM Trans. on Programming Languages and Systems (TOPLAS), 2000, 22(2): 416–430. [doi:10.1145/349214.349241]
[2] Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In:Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg:Springer-Verlag, 2006. 300-314.[doi:10.1007/11817963_29]
[3] Kochems J, Ong CHL. Safety verification of asynchronous pushdown systems with shaped stacks. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2013. 288-302.[doi:10.1007/978-3-642-40184-8_21]
[4] Petri CA. Kommunikation mit automaten[Ph.D. Thesis]. University of Bonn, 1962.
[5] Lazić R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J. Nets with tokens which carry data. Fundamenta Informaticae, 2008, 88(3): 251–274. https://www.researchgate.net/profile/A_Roscoe/publication/220444377_Nets_with_Tokens_Which_Carry_Data/links/00b49533ee85a5076e000000/Nets-with-Tokens-Which-Carry-Data.pdf
[6] Emmi M, Ganty P, Majumdar R, Rosa-Velardo F. Analysis of asynchronous programs with event-based synchronization. In:Proc. of the European Symp. on Programming Languages and Systems. Berlin, Heidelberg:Springer-Verlag, 2015. 535-559.[doi:10.1007/978-3-662-46669-8_22]
[7] D'Osualdo E, Kochems J, Ong CHL. Automatic verification of Erlang-style concurrency. In:Proc. of the Int'l Static Analysis Symp. Berlin, Heidelberg:Springer-Verlag, 2013. 454-476.[doi:10.1007/978-3-642-38856-9_24]
[8] D'Osualdo E, Kochems J, Ong L. Soter:An automatic safety verifier for Erlang. In:Proc. of the 2nd Edition on Programming Systems, Languages and Applications Based on Actors, Agents, and Decentralized Control Abstractions. ACM Press, 2012. 137-140.[doi:10.1145/2414639.2414658]
[9] Kochems J. Verification of asynchronous concurrency and the shaped stack constraint[Ph.D. Thesis]. University of Oxford, 2015.
[10] Cai X, Ogawa M. Well-Structured pushdown systems. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2013. 121-136.[doi:10.1007/978-3-642-40184-8_10]
[11] Jhala R, Majumdar R. Interprocedural analysis of asynchronous programs. ACM SIGPLAN Notices, 2007, 42(1): 339–350. [doi:10.1145/1190215.1190266]
[12] Ganty P, Majumdar R, Rybalchenko A. Verifying liveness for asynchronous programs. ACM SIGPLAN Notices, 2009, 44(1): 102–113. [doi:10.1145/1594834.1480895]
[13] Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems (TOPLAS), 2012, 34(1): 6. [doi:10.1145/2160910.2160915]
[14] Majumdar R, Wang Z. BBS:A phase-bounded model checker for asynchronous programs. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2015. 496-503.[doi:10.1007/978-3-319-21690-4_33]
[15] Hague M. Parameterised pushdown systems with non-atomic writes. In:Proc. of the 31st Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science. 2011. 457. http://arxiv.org/abs/1109.6264
[16] Esparza J, Ganty P, Majumdar R. Parameterized verification of asynchronous shared-memory systems. In:Proc. of the 25th Int'l Conf. on Computer Aided Verification (CAV 2013), Vol.8044. Saint Petersburg:Springer-Verlag, 2013. 124.[doi:10.1007/978-3-642-39799-8_8]
[17] Durand-Gasselin A, Esparza J, Ganty P, Majumdar R. Model checking parameterized asynchronous shared-memory systems. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2015. 67-84.[doi:10.1007/978-3-319-21690-4_5]
[18] La Torre S, Muscholl A, Walukiewicz I. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In:Proc. of the 26th Int'l Conf. on Concurrency Theory. 2015. 72. http://drops.dagstuhl.de/opus/volltexte/2015/5381
[19] Leroux J, Praveen M, Sutre G. Hyper-Ackermannian bounds for pushdown vector addition systems. In:Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). ACM Press, 2014. 63.[doi:10.1145/2603088.2603146]
[20] Leroux J, Sutre G, Totzke P. On the coverability problem for pushdown vector addition systems in one dimension. In:Proc. of the Int'l Colloquium on Automata, Languages, and Programming. Berlin, Heidelberg:Springer-Verlag, 2015. 324-336.[doi:10.1007/978-3-662-47666-6_26]
[21] Finkel A, Schnoebelen P. Well-Structured transition systems everywhere. Theoretical Computer Science, 2001, 256(1): 63–92. [doi:10.1016/S0304-3975(00)00102-X]
[22] Chadha R, Viswanathan M. Decidability results for well-structured transition systems with auxiliary storage. In:Proc. of the Int'l Conf. on Concurrency Theory. Berlin, Heidelberg:Springer-Verlag, 2007. 136-150.[doi:10.1007/978-3-540-74407-8_10]
[23] Rodríguez C. Verification Based on Unfoldings of Petri Nets with Read Arcs. École Normale Supérieure de Cachan, 2013.
[24] Siebert M, Flochová J. Pnets-The verification tool based on Petri nets. In:Proc. of the World Congress on Engineering. 2013. 1. http://www.iaeng.org/publication/WCE2013/WCE2013_pp369-373.pdf
[25] Esparza J, Ledesma-Garza R, Majumdar R, Meyer P, Niksic F. An SMT-based approach to coverability analysis. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer Int'l Publishing, 2014. 603-619.[doi:10.1007/978-3-319-08867-9_40]
[26] Christensen S, Hansen ND. Coloured Petri nets extended with channels for synchronous communication. In:Proc. of the 15th Int'l Conf. on the Application and Theory of Petri Nets. LNCS 815, Zaragoza:Springer-Verlag, 1994. 159-178.[doi:10.1007/3-540-58152-9_10]
[27] Lakos C. The consistent use of names and polymorphism in the definition of object Petri nets. In:Proc. of the 17th Int'l Conf. on the Application and Theory of Petri Nets. LNCS, Springer-Verlag, 1996. 380-399.[doi:10.1007/3-540-61363-3_21]
[28] Valk R. Petri nets as token objects? An introduction to elementary object nets. In:Proc. of the 19th Int'l Conf. on the Application and Theory of Petri Nets. LNCS 1420, Springer-Verlag, 1998.[doi:10.1007/3-540-69108-1_1]
[29] Lee JK, Palsberg J, Majumdar R, Hong H. Efficient may happen in parallel analysis for async-finish parallelism. In:Proc. of the Int'l Static Analysis Symp. Berlin, Heidelberg:Springer-Verlag, 2012. 5-23.[doi:10.1007/978-3-642-33125-1_4]
[30] Gavran I, Niksic F, Kanade A, Rupak M, Viktor V. Rely/Guarantee reasoning for asynchronous programs. In:Proc. of the LIPIcs-Leibniz Int'l Proceedings in Informatics. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. 42. http://drops.dagstuhl.de/opus/volltexte/2015/5390
[31] Deligiannis P, Donaldson AF, Ketema J, Lal A, Thomson P. Asynchronous programming, analysis and testing with state machines. ACM SIGPLAN Notices, 2015, 50(6): 154–164. [doi:10.1145/2813885.2737996]