基于k-定界的動態下推網絡可達性分析

?

基于k-定界的動態下推網絡可達性分析

引文格式： 徐力，錢俊彥.基于k-定界的動態下推網絡可達性分析[J].桂林電子科技大學學報,2016,36(1):48-51.

徐力，錢俊彥

(桂林電子科技大學 計算機科學與工程學院，廣西 桂林541004)

摘要：為了保證含有遞歸、動態創建線程并發系統的安全性，提出基于動態下推網絡模型的形式化驗證方法。該模型的可達性為不可判定，把動態下推網絡轉換為在k-定界下可達性可判定的下推網絡，再將轉換后的下推網絡符號化。分析表明，該方法可使模型可達性成為可判定的，且緩解了模型狀態空間爆炸的狀態。

關鍵詞：動態下推網絡；k-定界；可達性分析；符號化

隨著多核技術的發展以及內存容量越來越大，基于充分利用資源的原則，Java語言引入Fork/Join并行模式，通過該模式，并發程序可把線程分解成更細粒度的子線程并行執行[1]，且動態創建新線程[2]對構造系統組件具有重要意義，如在程序執行過程中，可創建新線程，實現函數回調。但由于并發線程交錯執行，使得代碼中隱匿的漏洞和錯誤難以檢測。

為保證帶動態線程創建和含有遞歸的并發程序運行安全，采用動態下推網絡[3]對其進行模型檢測。然而，動態下推網絡可達性不可判定[4]，使得驗證難以實現。Qadeer等[5]提出了k-定界可達算法，解決了多棧下推系統的上下文模型檢測，但無法解決帶動態線程創建的可達性問題。

鑒于此，基于k-定界技術，將動態下推網絡模擬成可達性可判定[6]的下推網絡，并基于下推網絡提出一種符號下推網絡可達算法[7]，壓縮狀態空間來緩解爆炸問題的狀態。

1相關知識

1.1并發程序并行模式

隨著大規模數據處理的與日俱增以及硬件價格的大幅下降，高性能多核并發計算得到廣泛應用，基于多核技術的并行編程語言及編程模式被廣泛運用。例如，Java在第7版中引入Fork/Join并行模式，以及被廣泛使用Map Reduce并行編程模式等。通常程序在運行時，若其線程池中的一個線程正在執行某個任務，由于資源不足或者其他原因，無法繼續執行，則該線程會掛起處于等待中。基于Fork/Join并行框架的程序，若處理某個任務的線程無法執行，該線程會主動尋找其他尚未運行的子問題執行，Fork/Join并行編程技術可減少線程等待時間，充分利用處理器資源，提高程序性能。

圖1中的父線程能否執行，依賴于其子線程的執行結果，只有當其子線程執行結束，調用線程才能獲得父線程返回結果。Fork/Join并行模式運行的基本原理為：當連接一個客戶時，使用Fork創建一個線程標識符，存儲在一個變量中，該新線程標識符會被拷貝到父線程的標識符變量中，該新線程是原線程的副本，可與客戶完成通信。在該線程運行結束，返回父線程繼續執行的過程中，該變量包含的線程標識符一直被Join操作監視[8]。

圖1　Fork/Join并行模式Fig.1　Fork/Join model

1.2動態下推網絡

動態下推網絡M由一組動態下推系統[9-10]

{D1,…,Di,…,Dn} s.t.i1≤i≤n

組成。其中：Di=(Pi,Γi,Δi)為一個動態下推系統；Pi為狀態集；Γi為棧字符集；Δi為遷移規則集合，具有以下形式：

1)pia→pjωj，其中pjωj∈Pj×Γj*為動態創建的新線程；

2)pia→piωi?pjωj， s.t.pi,pi∈Pi,a∈Γi,ωi∈Γi*。

動態下推網絡是一組下推系統，并行執行各自順序序列的遷移系統。每個下推系統都可執行下推操作，以及在網絡中動態創建線程。假定G為全局變量集，動態下推系統格局可表示為

(g,p,ω)∈G×(P×Γ*)，

其中g∈G為全局變量，元組p,ω=p1,ω1,…,pi,ωi,…,pn,ωn，每個子項pi,ωi∈P×Γ*表示一個下推線程的局部格局。

定義1一個動態下推網絡可表示為一個六元組M=(G,P,Γ,Δ,gin,γin)。其中：G為所有全局變量賦值的集；P為所有局部控制狀態集合；Γ為所有棧字符集合；Δ為任意線程遷移關系集合；gin為初始全局狀態；γin為初始局部狀態(棧內容)。

以下給出了一個偽代碼程序，詳細闡述用動態下推網絡建模的格局遷移。

Main() {Initamend(){ Amend(){

1: call Initamend5: create Amend7: write data

2: write data6: return8: return

3: read data } }

4: return

}

用pi表示第i行代碼的程序狀態，a表示棧頂字符，其中pi∈P,a∈Γ。遷移關系集合為:

其中φi∈Δ表示遷移路徑。設開始格局集合為β1={p1a},目標格局集合為β2={p8ap3a}，可知從格局集合β1到格局集合β2可達，其可達路徑集合為

1.3動態下推網絡可達性問題

2k-定界可達問題描述及算法

假設一個遷移系統M和一個格局γ，如果格局γ在系統M中可達，當且僅當存在一條從初始格局γin到目標格局γ的路徑，即γin→*Mγ。動態下推網絡可達性問題已被證明是不可判定的，但是，如果在分析可達性問題時，對遷移中的上下文切換次數進行限定，可使得該問題變得可判定。對于給出的限制切換次數的正整數k，可遞歸定義的格局γ上的k-定界遷移關系：

其中：→i表示新的遷移關系；→*i表示該遷移關系的傳遞閉包。對于正整數k，因為每一個新遷移關系的閉包→*i都可能產生無限多種遷移，使得一個格局可遷移到無限多個不同的格局，所以，k-定界狀態空間和遷移序列可能是無界的。

Qadeer等[5]提出k-定界可達算法，主要為解決多棧下推系統的上下文模型檢測。該算法通過迭代增加執行上下文數目，其中，在單個執行上下文內，當前線程對于全局變量處于鎖定狀態，只有當前線程才能訪問全局狀態。只有執行上下文切換時對該全局狀態進行同步更新，這樣其他線程才能共享全局狀態信息。具體的k-定界可達算法如下：

輸入：并發下推系統C=(G,Γ,Δ0,…,Δn,gin,ωin)；正整數k。

輸出：Reach。

1letAin=(Q,G,d, {gin},F)

//其中L(Ain)={gin, ωin}

2WorkList∶={(g,Ain,…,Ain, 0)};

//包含N+1個Ain

3Reach∶={g,Ain,…,Ain};

4while(!WorkList)

5let(g,Ain,…,Ain,i)=REMOVE(WorkList)in

6if(i

7forall(j=0,…,N)

11ADD(WorkList, (x,i+1));

12Reach:=Reach∪{x};

13}

k-定界可達算法中第1~3行分別表示對自動機、工作線程及可達集合的初始化，從第4行開始，針對工作線程WorkList，窮盡計算并發下推系統C中小于k-定界切換的格局。對于并發下推系統C=(G, Γ,Δ0,…,Δn, gin, ωin)和給定的正整數k，該算法是可終止的，其復雜度為O(k3(N|G|)k|P|5)。

3基于下推網絡符號化分析

3.1轉換為下推網絡

給定一個動態下推網絡M=(G, P, Γ, Δ, gin,γin)和一個正整數k，可模擬一個對應的下推網絡M。模擬轉換的基本思想為：對動態下推網絡進行k-定界上下文切換的限制，即執行一步遷移最多有k個不同的線程。因此,下推網絡可使用標識符為{0,1,…,k-1}的線程遷移遞歸地來模擬動態下推網絡的遷移，約定標識符為k的線程從不執行遷移，用來模擬動態下推網絡的剩余線程。最終通過轉換得到的下推網絡包含k+1個線程，其局部狀態表示為(p, n, a)。其中：p為局部變量；n為執行遷移線程對應最大線程標識符；a為終止線程對應線程標識符。轉換算法如下：

輸入：動態下推網絡M=(G, P,Γ, Δ, gin, ωin)；正整數k。

輸出：對于下推網絡M′。

1lett=0;//標識符初始化為0

2WorkList∶=g,(p, 0,a),γ;

//包含N+1個Ain

3forall(p, 0,a),γ∈WorkListdo

//選擇一個線程為n的初始狀態，開始構造

4if(0<=t<=n&&n

5forallΔ

6switch(Δ)

7begin

8casep,γ→p′,γ′∈Δ;

9Move(p,n,a),γ→(p′,n,a),γ′

intoΔ′;break;

10caseg,p,γ→g′,p′,γ′∈Δ;

11Moveg,(p,n,a),γ→g′,(p′,n,a),γ′intoΔ′;break;

12casep,γ→p′,γ′p″,γ″∈Δ;

13Move(p,n,a),γ→(p′,n,a),γ′

intoΔ′;break;

14WorkList∶=(p″, ++n,a),γ″;break;

15caseg,p,γ→g′,p′,γ′p″,γ″∈Δ;

16Moveg,(p,n,a),γ→g′,(p′,n,a),γ′intoΔ′;break;

17WorkList∶=(p″, ++n,a),γ″;break;

18casep,γ→$;

19Move(p,n,a),γ→(p′,n,a∪{t}),$intoΔ′;break;

20endswitch；

20t++;//下一個線程

轉換算法中第1~2行分別表示對標識符和工作線程初始化，從第3行開始，針對M的格局遷移關系，窮盡計算下推網絡M的遷移關系。由算法可知，當標識符t=k或無新的遷移規則時，執行終止，該算法的時間復雜度與程序的大小呈指數關系，與多項式整數k呈線性關系。

3.2符號化分析

轉換后的下推網絡由一組不能進行動態創建線程的下推系統組成，為了描述方便，只描述單個下推系統進行符號化的過程，下推網絡符號化與之類似。

下推系統

其中：P為控制位集；Γ為棧字符集；Δ?(P×Γ)×(P×Γ*)為遷移關系集。

符號下推系統

其中G和L為整數{0,1}集合。

符號遷移函數

簡化表示為

其中：R?(G×L)×(G×Ln)；(g, l, g, l1, l2,…,ln)∈R。

下推系統T和符號下推系統Ts對程序中賦值語句、函數調用以及返回語句的建模規則定義如下：

2)程序調用。T的遷移規則為g, (n1,l)→g, (n3,l) (n2,l)，Ts的遷移規則為p,n1p,n3n2。

3)返回語句。T的遷移規則為g, (n1,l)→g,ε，Ts的遷移規則為p,n1p,ε。

由遷移規則可知，符號下推系統Ts比下推系統T的表達更緊湊、簡潔，且程序中的布爾變量和整數值都可用OBDD表示，可以指數性地壓縮狀態空間，以便節省大量搜索時間。

4結束語

針對Fork/Join并行性的并發程序，用動態下推網絡進行建模，并利用k-定界和符號技術緩解空間爆炸問題的狀態，其算法效率有待改進。下一步研究方向主要為：

1)針對Fork/Join并行性的實時并發系統，基于該模型引入能刻畫時間行為的時鐘，構造時間動態下推網絡，并基于時鐘模型提出相應的可達搜索算法。

2)利用現有的模型驗證工具(如Moped)，實現并發遞歸系統的抽象模型驗證，解決位向量、語言決策等問題。在現有工具的基礎上，利用相關求解算法,開發相應的實時并發程序的驗證工具。

參考文獻:

[1]TAUBENFELD G.A closer look at concurrent data structures and algorithms[J].Bulletin of the European Association for Theoretical Computer Science,2015,115:61-82.

[2]SONGF,TOUILIT.Modelcheckingdynamicpushdownnetworks[C]//SHANCC.Proceedingsofthe11thAsianSymposiumonProgrammingLanguagesandSystems:8301Melbourme,Australia,2013:33-49.

[3]ATIGM,BOUAJJANIA,QADEERS.Context-boundedanalysisforconcurrentprogramswithdynamiccreationofthreads[C]//Proceedingsofthe15thInternationalConferenceonTACASLNCS5505,UnivYork,EuropeanAssoc,2009:107-123.

[4]RAMALIANGAMG.Contextsensitivesynchronizationsensitiveanalysisisundecidable[J].OnProgrammingLanguagesandSystems,2000,22:416-430.

[5]QADEERS,REHOFJ.Context-boundedmodelcheckingofconcurrentsoftware[C]//HALBWACHSN,ZUCKLD.11thInternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems:3440.Edinburgh:Springer,2005:93-107.

[6]MCLEAND,RYBAKOVV.Multi-agenttemporarylogicTS4(Kn)(U)basedatnon-lineartimeandimitatinguncertaintyviaagents'interaction[C]//RUTKOWSKIL.LectureNotesinArtificialIntelligence.LNCS8052.Zakopane,POLAND,2013:375-384.

[7]ESPARZAJ,SCHWOONS.ABDD-basedmodelcheckerforrecursiveprograms[C]//BERRYG,COMONH,FINKELA.13thTnternationalConferenceonComputerAidedVerification:2102.Heidelberg:Springer,2005:93-107.

[8]BOLLIGB,KUSKED,MENNICKER.Thecomplexityofmodelcheckingmulti-stacksystems[C]//Proceedingsofthe28thAnnualACM/IEEESymposiumonLogicinComputerScience,NewOrleans,LA,USA,2013:163-72.

[9]LAMMICHP,OLMM,SEIDLH.Contextuallockingfordynamicpushdownnetworks[C]//Proceedingsofthe20thInternationalSymposiumonStaticAnalysis,Seattle,WA,USA,2013:47-98.

[10]CAOXiaojuan,MIZUHITOD.Well-structuredpushdownsystems[C]//MELGRATTIH.LecturenotesinArtificialIntelligence.LNCS8052,Berlin,Heidelberg:Springer,2013:121-136.

編輯：梁王歡

Research onk-delimited accessibility analysis for dynamic pushdown network

XU Li， QIAN Junyan

(School of Computer Science and Engineering, Guilin University of Electronic Technology, Guilin 541004, China)

Abstract：In order to ensure the security of concurrent system which contains recursion and dynamic creating threads, the formal verification method based on dynamic pushdown network model is proposed. The accessibility of this model is undecidable. The dynamic pushdown network is transformed into the accessibility which can be decidable under the k-delimited condition. And then the transformed pushdown network is symbolized. The analysis shows that the method makes the accessibility of the model decidable and greatly optimizes the problem of model state space explosion.

Key words：dynamic pushdown network; k-delimited; accessibility analysis; symbolic

中圖分類號：TP301

文獻標志碼：A

文章編號：1673-808X(2016)01-0048-04

通信作者：錢俊彥(1973-)，男，浙江嵊縣人，教授，博士，研究方向為形式化方法、模型檢測。E-mail：junyanq@gmail.com

基金項目：國家自然科學基金(61262008)；廣西自然科學基金(2012GXNSFAA053220,2014GXNSFAA118365)

收稿日期：2015-04-06