[發明專利]基于上下文定界的隊列通信并發遞歸程序驗證方法

有效

• 申請號: 201210450761.8
• 申請日: 2012-11-12
• 公開（公告）號: CN102929781A
• 公開（公告）日: 2013-02-13
• 發明（設計）人: 錢俊彥;賈書貴;趙嶺忠;蔡國永;郭云川
• 申請（專利權）人: 桂林電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京思海天達知識產權代理有限公司 11203
• 代理人: 樓艮基

1.基于上下文定界的消息隊列通信并發遞歸程序的驗證方法，其特征在于：是一種基于良序消息隊列通信的并發遞歸程序RQCP上下文切換定界的可達性辨識之上的程序驗證方法，所述良序消息隊里是僅當進程的局部棧為空時，進程才能從隊列中讀取消息中途不允許被中斷，直至執行結束時才處理下一個任務，所述的并發遞歸程序，以下簡稱RQCP，用R表示，是在一臺多核處理器中依次按以下步驟實現驗證的，

步驟（1）、依次按以下步驟把所述的R轉換為一個多棧下推系統，用表示，以便把上下文(p,q)切換定界可達性問題轉換為多棧下推系統的階定界可達性問題，其中k次上下文切換對應于3k+1個階，其目的在于把基于良序消息隊列通信的并發遞歸程序R轉換為一個等價的用于模擬R執行的多棧下推系統，該多棧下推系統的執行對應于所述R所包含的動作或行為，步驟如下：

步驟（1.1）、構建R的抽象模型

給定一個體系結構A=(P,Q,Sender,Receiver)，P是有限進程集合，Q是有限隊列集合，Sender:Q→P和Receiver:Q→P是兩個指派函數，分別為每個隊列q∈Q唯一指派的發送進程和接收進程，并規定每個隊列的發送進程和接收進程是不同的：即對于q∈Q，Sender(q)≠Receiver(q)，

設：Π表示有限的消息字母表，m∈Π表示消息，p∈P表示一個進程，q∈Q表示一個隊列；

Act_p表示一個進程p的動作集合，Act=∪_p∈PAct_p表示所有進程的動作集合；

Calls表示所有進程的調用動作的集合，表述為{p:call|p∈P}，p:call為描述過程調用的局部棧動作；

Rets表示所有進程的返回動作的集合，表述為{p:ret|p∈P}，p:ret為描述過程返回的局部棧動作；其中：

p:call相當于進程p的局部過程調用，進程p把至少包括地址、局部變量的賦值在內的數據送到局部棧的棧頂，并遷移到新狀態；

p:ret相當于進程p中過程調用的返回，彈出局部棧的內容并遷移到另一個新狀態，所述另一個新狀態依賴于進程p的當前狀態及所述的局部棧中彈出的數據；

動作p:send(q,m)表示進程p向接收隊列q中寫入消息m；

動作p:recv(q,m)表示進程p從所述接收隊列q中讀取消息m；

動作p:int表示進程p的對隊列不處理的一個內部動作；

給定一個體系結構A=(P,Q,Sender,Receiver)，在所述體系結構A運行的上的遞歸隊列并發程序是一個五元組R，R=(S,s₀,∏，Γ，{T_p}_p∈P)，其中S是有限的狀態集合，s₀∈S是初始狀態，Π是所述的有限的消息字母表，Γ是有限的局部棧字母表，T_p是進程p的遷移關系集合，表示如下：

Tp⊆(S×(Actp/{p:call,p:ret})×S)∪(S×{p:call}×S×Γ)∪(S×{p:ret)×Γ×S),]]>

其中進程p的動作的形式如下：

1)p:send(q,m)，其中m∈Π，q∈Q，且Sender(q)=p；

2)p:recv(q,m)，其中m∈Π，q∈Q，且Receiver(q)=p；

3)p:int，或者p:call或者p:ret；

步驟（1.2）、R的操作語義描述

給定遞歸隊列并發程序R=(S,s₀,∏，Γ，{T_p}_p∈P)，其中：

{T_p}_p∈P是所有進程p的遷移關系集合；

其格局是一個三元組(s,{σ_p}_p∈P,{μ_q}_q∈Q)，其中s∈S是狀態；

符號{σ_p}∈Γ^*是進程p的進程局部棧的內容，表示為σ_p∈Γ^*，Γ^*是所述進程局部棧字母上的閉包；

符號{μ_q}∈Π^*是隊列q的內容，表示為μ_q∈Π^*，Π^*是所述消息字母上的閉包；

假設進程p的棧頂內容位于σ_p的最左端，棧底內容位于σ_p的最右端；

隊列q的隊尾消息位于μ_q的最左端，隊頭消息位于μ_q的最右端；

使用以下操作語義描述格局之間的遷移關系：

操作[Internal]act=p:int(s,p:int,s′)∈Tp(s,{σp}p∈P,{μq}q∈Q)→sct(s′,{σp}p∈P,{μq}q∈Q)]]>為內部動作，表示：執行動作p:int，使R的狀態由但{σ_p}、{μ_q}的內容沒有改變；

操作[Send]act=p:send(q,m)(s,p:send(q,m),s′)∈TpSender(q)=p(s,{σp}p∈P,{μq′}q′∈(Q/{q})∪{μq})→act(s′,{σp}p∈P,{μq′}q′∈(Q/{q})∪{m.μq})]]>為寫入，表示：執行動作p:send(q,m)，寫入進程為p，使R的狀態由使隊列的內容{μ_q′}中除了{μ_q}外還寫入了消息m；

操作[Receive]act=p:recv(q,m)(s,p:recv(q,m),s′)∈TpReceiver(q)=p(s,{σp}p∈P,{μq′}q′∈(Q/{q})∪{μq′.m})→act(s′,{σp}p∈P,{μq′}q′∈(Q/{q})∪{μq′})]]>為接受，表示執行動作p:recv(q,m)，讀取方是p，從s狀態下的隊列{μ′_q.m}中讀取消息m，使R的狀態由使隊列q的內容{μ′_q}中被讀取了消息m，寫入時的{μ_q}不一定等于讀取時的{μ′_q}；

操作[Call]act=p:call(s,p:call,s′,γ)∈Tp(s,{σp}∪{σp′}p′∈(P/{p}),{μq}q∈Q)→act(s′,{γσp}∪{σp′}p′∈(P/{p}),{μq}q∈Q)]]>為調用，表示：執行動作p:call，在s狀態下進程p根據規則γ調用至少包括地址、局部變量的賦值在內的數據送到對應于進程p的局部棧的內容{σ_p′}的最左端，使得狀態由{σ_p′}添加為{γσ_p′}；

操作[Return]act=p:ret(s,p:ret,γ,s′)∈Tp(s,{γσ′p}∪{σp′}p′∈(P/{p}),{μq}q∈Q)→act(s′,{σ′p}∪{σp′}p′∈(P/{p}),{μq}q∈Q)]]>為返回，表示：執行動作p:ret，在s狀態下，根據規則γ，彈出進程p的進程局部棧的內容{γσ′_p}中按規則γ調用的至少包括地址、局部變量的賦值在內的數據，剩下原先的內容{σ′_p}，使狀態狀態，所述調用的{γσ′_p}與返回的{σ′_p}不一定相同；

步驟（1.3）、用一個多棧下推系統模擬良序消息隊列的并發遞歸程序的執行

給定：良序消息隊列的并發遞歸程序R=(S,s₀,∏，Γ，{T_p}_p∈P)，

構造一個模擬所述良序消息隊列的并發遞歸程序R的k-上下文切換定界執行的多棧下推系統其中：

S是有限的狀態集合，s₀∈S是初始狀態；

St是局部棧集合，包括工作局部棧st_w，進程p對應的局部棧st_p，隊列q∈Q對應的局部棧st_q，St表示為St={st_w∪{st_p}_p∈P∪{st_q}_q∈Q}，各局部棧初始化為空；

是字母表，包括隊列對應的局部棧字母表，與進程對應的局部棧的字母表，表示為

Δ是遷移關系集合，包括：

Δ_int內部遷移關系集合，

Δ_push寫入遷移關系集合，包括push_q和push_p，其中：push_q與進程p的寫入隊列操作相關的遷移關系，push_p與進程p的入棧操作相關的遷移關系，

Δ_pop讀取遷移關系集合，包括pop_q和pop_p，其中：pop_q與進程p的讀取隊列操作相關的遷移關系，pop_p與進程p的出棧操作相關的遷移關系，

從而得到遷移關系集合Δ的表達式為：

Δ=Δ_int∪Δ_pop∪Δ_push，

在上下文（p,q）內，所述上下文定義為：某個進程任意長度的連續執行序列，進程p僅能從一個隊列中讀取消息，但可向所有輸出消息的任一隊列q寫入消息，所述進程p能執行的遷移關系定義如下：

規則[internal](s,p:int,s′)∈Tp(s,p:int,s′)∈Δint,]]>

規則[pushq](s,p:send(q,m),s′)∈TpSender(q)=p(s,p:send(q,m),s′)∈Δpush,]]>

規則[pushp](s,p:call,s′,γ)∈Tp(s,p:call,s′,γ)∈Δpush,]]>

規則[popq](s,p:recv(p,m),s′)∈TpReceiver(q)=p(s,p:recv(q,m),s′)∈Δpop,]]>

規則[popp](s,p:ret,γ,s′)∈Tp(s,p:ret,γ,s′)∈Δpop,]]>

規則表示把所述的R內隊列操作相關的遷移關系添加到所述的多棧下推系統中對應的遷移關系集合中去，

根據以上轉換方法構造的多棧下推系統能模擬良序排隊的遞歸隊列并發程序R的執行，并且的3k+1階定界可達問題相當于R的k上下文切換定界可達問題；

步驟（2）、按如下步驟執行基于可達算法Post^*的可達格局集合Reach計算

步驟（2.1）、初始化多棧下推系統

設立多棧下推系統和上下文切換次數K，0≤k≤K，其中：多棧下推系統是下推系統的自然擴展，包含多個棧結構；K是一個正整數，也是Post^*算法的迭代次數；其中：

S是有限的狀態集合，s₀∈S是初始狀態；

St={st_w∪{st_p}_p∈P∪{st_q}_q∈Q}，初始時，各棧st∈St的棧內容σ_st為空，表示為σ_st=ε；

其中：Π是隊列對應的局部棧字母表，Γ是進程對應的局部棧的字母表，總稱字母表；

Δ是遷移關系集合，Δ=Δ_int∪Δ_pop∪Δ_push；

定義：輸出可達格局集合Reach，集合Reach中存儲的是在至多k次上下文切換執行內正向可達的格局，用c表示，c=<s₀,{σ_st}_st∈St>，σ_st表示棧st∈St的內容；多棧下推系統的初始格局是c_in=<s₀,{σ_st}_st∈St>，以及對應的切換次數k，以格局項(c,k)的形式存儲在所述可達格局Reach的工作列表WL上，初始時的初始格局是c_in=<s₀,{σ_st}_st∈St>，內容σ_st為空，

給定的目標格局狀態集合T，所述目標狀態集合T定義為一種錯誤狀態集合，表示為是一種在所述并發遞歸程序不可能出現的錯誤狀態的集合，

步驟（2.2）、建立工作列表WL

按照所述并發遞歸程序的執行順序把所述上下文(p,q)轉換為依次銜接的格局項(c,k)，0≤k≤K的編號存儲于工作列表內，并初始化所述初始格為c_in，

步驟（2.3）、初始上下文(p,q)選擇

定義二元組（p,q）是所述并發遞歸程序的一個執行上下文，其中p是進程，q是進程間通信的隊列，并且隨機或指定某個上下文（p,q）為初始上下文，并對各棧st初始化：根據隊列q和進程p對應的遷移關系集合Δ，把隊列q對應棧st_q的內容壓入工作棧st_w的底部，將進程p對應的棧st_p內容壓入工作棧st_w的頂部，

假定是上下文（p,q）下進程p的下推系統，建立接受上下文(p,q)的初始格局的下推自動機A_p=(Q,Г，→₀,P,F)，對應算法5中的自動機A，其中：Q是自動機的控制位置集合，對應算法5中自動機A的狀態集合；Γ是自動機接受的字母表，對應算法5中自動機A接受的字母表；→₀是自動機的轉移函數，P是初始控制位置集合，對應算法5中自動機A的初始狀態集合；F是終止控制位置集合，對應算法5中自動機A的終止狀態集合，

對于下推自動機A_p，存在接受其正向可達格局集合的下推自動機A′_p=post^*(A_p)，給定初始格局為<s₀,σ_st>的下推系統及其對應的遷移關系集合Δ，可以計算接受下推系統正向可達格局集合為語言的下推自動機

步驟（2.4）、按以下步驟從所述初始上下文(p,q)開始，對所述工作隊列表WL中各個格局項編號中的內容進行上下文切換可達性計算

步驟（2.4.1）、從工作列表WL中取出一個編號對應于初始上下文(p,q)的格局項，并分別存儲在進程局部棧st_p和隊列局部棧st_q中：進程p逆序地存儲存儲在st_p和中，棧底存儲隊尾指向的內容，棧頂存儲隊頭指向的內容，隊列q是順序存儲在棧st_q中：棧頂存儲隊尾指向的內容，棧底存儲隊頭指向的內容，

步驟（2.4.2）、再把棧st_q的內容存儲在工作棧st_w的底部，棧st_p的內容存儲在工作棧st_w的頂部，

步驟（2.4.3）、使另一個進程局部棧棧st_p和隊列棧st_q初始化為空，在把初始上下文(p,q)切換為上下文(p′,q′)時，此時迭代次數k≤K,對工作棧st_w的頂部和底部進行出棧操作，把讀取的內容分別存儲到棧st_p和st_q中，

步驟（2.4.4）、按以下步驟計算進程中的初始格局是否屬于正向可達格局集合的初始格局：

步驟（2.4.4.1）、若所述多棧下推系統中對應于初始上下文(p,q)的遷移關系集合是寫入遷移關系集合Δ_push，δ=(s,st_q′,a,s′)∈Δ_push，a是消息，且格局<s?′σ′_p>，σ′_p=aσ_p，σ_p是棧st_p的內容，則向棧st_q′中入棧消息a，

步驟（2.4.4.2）、若所述多棧下推系統中對應于初始上下文(p,q)的遷移關系集合是讀取遷移關系集合Δ_pop，δ=(s,st_q,a,s′)，且格局為<s′,ε>，則彈出棧st_q內的消息a，局部棧為空，

步驟（2.4.4.3）、修改狀態s′的可達格局賦值為x，把格局項(x,i+1)添加到工作列表WL中，

步驟（2.4.4.4）、在繼續從初始上下文(p,q)開始向下執行上下文切換之后，按步驟（2.5）所述進行可達格局集合Reach計算，

步驟（2.5）、根據Post^*算法計算接受上下文（p,q）正向可達格局集合的下推自動機A′_p=Post^*(A_p)，A_p是接受進程p初始格局的下推自動機，修改A′_p的狀態，修改后的格局添加到工作列表WL，以及可達格局集合Reach，

步驟（2.5.1）、對于s′∈S(A′_p)，如果下推自動機A_p∈{P/p}的初始狀態與狀態s相同，使用rename(A_p∈{P/p},s′)修改A_p∈{P/p}的初始狀態為s′，避免自動機A′_p的初始狀態與自動機A_p中的狀態重名而產生沖突，

步驟（2.5.2）、使用函數update(A′_p,s′)重命名A′_p中除s′之外的其他狀態，并更新S不包含的狀態，即修改格局的賦值為x=<s′,update(A′_p,s′),rename(A_p∈{P/p},s′),update(σ_st/{p∈P})>，

步驟（2.5.3）、最后修改后的可達格局賦值為x，將格局項(x,k+1)添加到工作列表WL，并將格局x添加到集合Reach，

步驟（3）、目標可達性的判定分析

根據正向可達格局集合Reach(k)和給定的目標狀態集合T，目標狀態集合T視為R中不可能出現的狀態的集合，也稱錯誤狀態集合，進而計算集合Reach和集合的交集是否為空，上下文切換次數k的值從0不斷增大，直至可用計算資源被耗盡，

步驟（3.1）、若Reach∩T非空，則經過k次上下文切換的運行，某個目標狀態s∈S是可達的，則存在一個起始于初始格局的執行路徑能夠到達該錯誤狀態，進而根據進程在各個狀態的局部棧的內容和消息隊列的內容，嘗試查找產生錯誤的原因，

步驟（3.2）、若Reach∩T為空，則經過k次上下文切換的運行，目標狀態s∈S是不可達的，狀態s不可達的判斷步驟如下：

a)經過k次上下文切換的運行，搜索的狀態空間覆蓋度不足以覆蓋目標狀態，此時可以增大k的值并繼續求解，直至耗盡所有可用的計算資源；

b)若根據步驟a)仍不能判定目標狀態是可達的，則得出結論：在現有計算能力下目標狀態是不可能出現的。