基于k-定界的動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性分析

?

基于k-定界的動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性分析

引文格式： 徐力，錢(qián)俊彥.基于k-定界的動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性分析[J].桂林電子科技大學(xué)學(xué)報(bào),2016,36(1):48-51.

徐力，錢(qián)俊彥

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

摘要：為了保證含有遞歸、動(dòng)態(tài)創(chuàng)建線(xiàn)程并發(fā)系統(tǒng)的安全性，提出基于動(dòng)態(tài)下推網(wǎng)絡(luò)模型的形式化驗(yàn)證方法。該模型的可達(dá)性為不可判定，把動(dòng)態(tài)下推網(wǎng)絡(luò)轉(zhuǎn)換為在k-定界下可達(dá)性可判定的下推網(wǎng)絡(luò)，再將轉(zhuǎn)換后的下推網(wǎng)絡(luò)符號(hào)化。分析表明，該方法可使模型可達(dá)性成為可判定的，且緩解了模型狀態(tài)空間爆炸的狀態(tài)。

關(guān)鍵詞：動(dòng)態(tài)下推網(wǎng)絡(luò)；k-定界；可達(dá)性分析；符號(hào)化

隨著多核技術(shù)的發(fā)展以及內(nèi)存容量越來(lái)越大，基于充分利用資源的原則，Java語(yǔ)言引入Fork/Join并行模式，通過(guò)該模式，并發(fā)程序可把線(xiàn)程分解成更細(xì)粒度的子線(xiàn)程并行執(zhí)行[1]，且動(dòng)態(tài)創(chuàng)建新線(xiàn)程[2]對(duì)構(gòu)造系統(tǒng)組件具有重要意義，如在程序執(zhí)行過(guò)程中，可創(chuàng)建新線(xiàn)程，實(shí)現(xiàn)函數(shù)回調(diào)。但由于并發(fā)線(xiàn)程交錯(cuò)執(zhí)行，使得代碼中隱匿的漏洞和錯(cuò)誤難以檢測(cè)。

為保證帶動(dòng)態(tài)線(xiàn)程創(chuàng)建和含有遞歸的并發(fā)程序運(yùn)行安全，采用動(dòng)態(tài)下推網(wǎng)絡(luò)[3]對(duì)其進(jìn)行模型檢測(cè)。然而，動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性不可判定[4]，使得驗(yàn)證難以實(shí)現(xiàn)。Qadeer等[5]提出了k-定界可達(dá)算法，解決了多棧下推系統(tǒng)的上下文模型檢測(cè)，但無(wú)法解決帶動(dòng)態(tài)線(xiàn)程創(chuàng)建的可達(dá)性問(wèn)題。

鑒于此，基于k-定界技術(shù)，將動(dòng)態(tài)下推網(wǎng)絡(luò)模擬成可達(dá)性可判定[6]的下推網(wǎng)絡(luò)，并基于下推網(wǎng)絡(luò)提出一種符號(hào)下推網(wǎng)絡(luò)可達(dá)算法[7]，壓縮狀態(tài)空間來(lái)緩解爆炸問(wèn)題的狀態(tài)。

1相關(guān)知識(shí)

1.1并發(fā)程序并行模式

隨著大規(guī)模數(shù)據(jù)處理的與日俱增以及硬件價(jià)格的大幅下降，高性能多核并發(fā)計(jì)算得到廣泛應(yīng)用，基于多核技術(shù)的并行編程語(yǔ)言及編程模式被廣泛運(yùn)用。例如，Java在第7版中引入Fork/Join并行模式，以及被廣泛使用Map Reduce并行編程模式等。通常程序在運(yùn)行時(shí)，若其線(xiàn)程池中的一個(gè)線(xiàn)程正在執(zhí)行某個(gè)任務(wù)，由于資源不足或者其他原因，無(wú)法繼續(xù)執(zhí)行，則該線(xiàn)程會(huì)掛起處于等待中?；贔ork/Join并行框架的程序，若處理某個(gè)任務(wù)的線(xiàn)程無(wú)法執(zhí)行，該線(xiàn)程會(huì)主動(dòng)尋找其他尚未運(yùn)行的子問(wèn)題執(zhí)行，F(xiàn)ork/Join并行編程技術(shù)可減少線(xiàn)程等待時(shí)間，充分利用處理器資源，提高程序性能。

圖1中的父線(xiàn)程能否執(zhí)行，依賴(lài)于其子線(xiàn)程的執(zhí)行結(jié)果，只有當(dāng)其子線(xiàn)程執(zhí)行結(jié)束，調(diào)用線(xiàn)程才能獲得父線(xiàn)程返回結(jié)果。Fork/Join并行模式運(yùn)行的基本原理為：當(dāng)連接一個(gè)客戶(hù)時(shí)，使用Fork創(chuàng)建一個(gè)線(xiàn)程標(biāo)識(shí)符，存儲(chǔ)在一個(gè)變量中，該新線(xiàn)程標(biāo)識(shí)符會(huì)被拷貝到父線(xiàn)程的標(biāo)識(shí)符變量中，該新線(xiàn)程是原線(xiàn)程的副本，可與客戶(hù)完成通信。在該線(xiàn)程運(yùn)行結(jié)束，返回父線(xiàn)程繼續(xù)執(zhí)行的過(guò)程中，該變量包含的線(xiàn)程標(biāo)識(shí)符一直被Join操作監(jiān)視[8]。

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

1.2動(dòng)態(tài)下推網(wǎng)絡(luò)

動(dòng)態(tài)下推網(wǎng)絡(luò)M由一組動(dòng)態(tài)下推系統(tǒng)[9-10]

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

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

1)pia→pjωj，其中pjωj∈Pj×Γj*為動(dòng)態(tài)創(chuàng)建的新線(xiàn)程；

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

動(dòng)態(tài)下推網(wǎng)絡(luò)是一組下推系統(tǒng)，并行執(zhí)行各自順序序列的遷移系統(tǒng)。每個(gè)下推系統(tǒng)都可執(zhí)行下推操作，以及在網(wǎng)絡(luò)中動(dòng)態(tài)創(chuàng)建線(xiàn)程。假定G為全局變量集，動(dòng)態(tài)下推系統(tǒng)格局可表示為

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

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

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

以下給出了一個(gè)偽代碼程序，詳細(xì)闡述用動(dòng)態(tài)下推網(wǎng)絡(luò)建模的格局遷移。

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

1: call Initamend5: create Amend7: write data

2: write data6: return8: return

3: read data } }

4: return

}

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

其中φi∈Δ表示遷移路徑。設(shè)開(kāi)始格局集合為β1={p1a},目標(biāo)格局集合為β2={p8ap3a}，可知從格局集合β1到格局集合β2可達(dá)，其可達(dá)路徑集合為

1.3動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性問(wèn)題

2k-定界可達(dá)問(wèn)題描述及算法

假設(shè)一個(gè)遷移系統(tǒng)M和一個(gè)格局γ，如果格局γ在系統(tǒng)M中可達(dá)，當(dāng)且僅當(dāng)存在一條從初始格局γin到目標(biāo)格局γ的路徑，即γin→*Mγ。動(dòng)態(tài)下推網(wǎng)絡(luò)可達(dá)性問(wèn)題已被證明是不可判定的，但是，如果在分析可達(dá)性問(wèn)題時(shí)，對(duì)遷移中的上下文切換次數(shù)進(jìn)行限定，可使得該問(wèn)題變得可判定。對(duì)于給出的限制切換次數(shù)的正整數(shù)k，可遞歸定義的格局γ上的k-定界遷移關(guān)系：

其中：→i表示新的遷移關(guān)系；→*i表示該遷移關(guān)系的傳遞閉包。對(duì)于正整數(shù)k，因?yàn)槊恳粋€(gè)新遷移關(guān)系的閉包→*i都可能產(chǎn)生無(wú)限多種遷移，使得一個(gè)格局可遷移到無(wú)限多個(gè)不同的格局，所以，k-定界狀態(tài)空間和遷移序列可能是無(wú)界的。

Qadeer等[5]提出k-定界可達(dá)算法，主要為解決多棧下推系統(tǒng)的上下文模型檢測(cè)。該算法通過(guò)迭代增加執(zhí)行上下文數(shù)目，其中，在單個(gè)執(zhí)行上下文內(nèi)，當(dāng)前線(xiàn)程對(duì)于全局變量處于鎖定狀態(tài)，只有當(dāng)前線(xiàn)程才能訪(fǎng)問(wèn)全局狀態(tài)。只有執(zhí)行上下文切換時(shí)對(duì)該全局狀態(tài)進(jìn)行同步更新，這樣其他線(xiàn)程才能共享全局狀態(tài)信息。具體的k-定界可達(dá)算法如下：

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

輸出：Reach。

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

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

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

//包含N+1個(gè)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-定界可達(dá)算法中第1~3行分別表示對(duì)自動(dòng)機(jī)、工作線(xiàn)程及可達(dá)集合的初始化，從第4行開(kāi)始，針對(duì)工作線(xiàn)程WorkList，窮盡計(jì)算并發(fā)下推系統(tǒng)C中小于k-定界切換的格局。對(duì)于并發(fā)下推系統(tǒng)C=(G, Γ,Δ0,…,Δn, gin, ωin)和給定的正整數(shù)k，該算法是可終止的，其復(fù)雜度為O(k3(N|G|)k|P|5)。

3基于下推網(wǎng)絡(luò)符號(hào)化分析

3.1轉(zhuǎn)換為下推網(wǎng)絡(luò)

給定一個(gè)動(dòng)態(tài)下推網(wǎng)絡(luò)M=(G, P, Γ, Δ, gin,γin)和一個(gè)正整數(shù)k，可模擬一個(gè)對(duì)應(yīng)的下推網(wǎng)絡(luò)M。模擬轉(zhuǎn)換的基本思想為：對(duì)動(dòng)態(tài)下推網(wǎng)絡(luò)進(jìn)行k-定界上下文切換的限制，即執(zhí)行一步遷移最多有k個(gè)不同的線(xiàn)程。因此,下推網(wǎng)絡(luò)可使用標(biāo)識(shí)符為{0,1,…,k-1}的線(xiàn)程遷移遞歸地來(lái)模擬動(dòng)態(tài)下推網(wǎng)絡(luò)的遷移，約定標(biāo)識(shí)符為k的線(xiàn)程從不執(zhí)行遷移，用來(lái)模擬動(dòng)態(tài)下推網(wǎng)絡(luò)的剩余線(xiàn)程。最終通過(guò)轉(zhuǎn)換得到的下推網(wǎng)絡(luò)包含k+1個(gè)線(xiàn)程，其局部狀態(tài)表示為(p, n, a)。其中：p為局部變量；n為執(zhí)行遷移線(xiàn)程對(duì)應(yīng)最大線(xiàn)程標(biāo)識(shí)符；a為終止線(xiàn)程對(duì)應(yīng)線(xiàn)程標(biāo)識(shí)符。轉(zhuǎn)換算法如下：

輸入：動(dòng)態(tài)下推網(wǎng)絡(luò)M=(G, P,Γ, Δ, gin, ωin)；正整數(shù)k。

輸出：對(duì)于下推網(wǎng)絡(luò)M′。

1lett=0;//標(biāo)識(shí)符初始化為0

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

//包含N+1個(gè)Ain

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

//選擇一個(gè)線(xiàn)程為n的初始狀態(tài)，開(kāi)始構(gòu)造

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++;//下一個(gè)線(xiàn)程

轉(zhuǎn)換算法中第1~2行分別表示對(duì)標(biāo)識(shí)符和工作線(xiàn)程初始化，從第3行開(kāi)始，針對(duì)M的格局遷移關(guān)系，窮盡計(jì)算下推網(wǎng)絡(luò)M的遷移關(guān)系。由算法可知，當(dāng)標(biāo)識(shí)符t=k或無(wú)新的遷移規(guī)則時(shí)，執(zhí)行終止，該算法的時(shí)間復(fù)雜度與程序的大小呈指數(shù)關(guān)系，與多項(xiàng)式整數(shù)k呈線(xiàn)性關(guān)系。

3.2符號(hào)化分析

轉(zhuǎn)換后的下推網(wǎng)絡(luò)由一組不能進(jìn)行動(dòng)態(tài)創(chuàng)建線(xiàn)程的下推系統(tǒng)組成，為了描述方便，只描述單個(gè)下推系統(tǒng)進(jìn)行符號(hào)化的過(guò)程，下推網(wǎng)絡(luò)符號(hào)化與之類(lèi)似。

下推系統(tǒng)

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

符號(hào)下推系統(tǒng)

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

符號(hào)遷移函數(shù)

簡(jiǎn)化表示為

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

下推系統(tǒng)T和符號(hào)下推系統(tǒng)Ts對(duì)程序中賦值語(yǔ)句、函數(shù)調(diào)用以及返回語(yǔ)句的建模規(guī)則定義如下：

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

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

由遷移規(guī)則可知，符號(hào)下推系統(tǒng)Ts比下推系統(tǒng)T的表達(dá)更緊湊、簡(jiǎn)潔，且程序中的布爾變量和整數(shù)值都可用OBDD表示，可以指數(shù)性地壓縮狀態(tài)空間，以便節(jié)省大量搜索時(shí)間。

4結(jié)束語(yǔ)

針對(duì)Fork/Join并行性的并發(fā)程序，用動(dòng)態(tài)下推網(wǎng)絡(luò)進(jìn)行建模，并利用k-定界和符號(hào)技術(shù)緩解空間爆炸問(wèn)題的狀態(tài)，其算法效率有待改進(jìn)。下一步研究方向主要為：

1)針對(duì)Fork/Join并行性的實(shí)時(shí)并發(fā)系統(tǒng)，基于該模型引入能刻畫(huà)時(shí)間行為的時(shí)鐘，構(gòu)造時(shí)間動(dòng)態(tài)下推網(wǎng)絡(luò)，并基于時(shí)鐘模型提出相應(yīng)的可達(dá)搜索算法。

2)利用現(xiàn)有的模型驗(yàn)證工具(如Moped)，實(shí)現(xiàn)并發(fā)遞歸系統(tǒng)的抽象模型驗(yàn)證，解決位向量、語(yǔ)言決策等問(wèn)題。在現(xiàn)有工具的基礎(chǔ)上，利用相關(guān)求解算法,開(kāi)發(fā)相應(yīng)的實(shí)時(shí)并發(fā)程序的驗(yàn)證工具。

參考文獻(xiàn):

[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

中圖分類(lèi)號(hào)：TP301

文獻(xiàn)標(biāo)志碼：A

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

通信作者：錢(qián)俊彥(1973-)，男，浙江嵊縣人，教授，博士，研究方向?yàn)樾问交椒?、模型檢測(cè)。E-mail：junyanq@gmail.com

基金項(xiàng)目：國(guó)家自然科學(xué)基金(61262008)；廣西自然科學(xué)基金(2012GXNSFAA053220,2014GXNSFAA118365)

收稿日期：2015-04-06