錢俊彥,賈書(shū)貴,蔡國(guó)永,趙嶺忠
(1.桂林電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院,廣西 桂林 541004);2.并行與分布處理國(guó)家重點(diǎn)實(shí)驗(yàn)室,湖南 長(zhǎng)沙 410073)
無(wú)論從理論,還是實(shí)踐角度來(lái)看,并發(fā)程序驗(yàn)證都是極具挑戰(zhàn)性的問(wèn)題。隨著多核技術(shù)日益發(fā)展,通過(guò)引入Fork/Join并行性,并發(fā)程序?qū)⑷蝿?wù)分解為更細(xì)粒度的子任務(wù)并行執(zhí)行,從而充分利用多核處理器提供的計(jì)算性能[1]。但是,多個(gè)線程之間的交錯(cuò)執(zhí)行可能會(huì)產(chǎn)生隱匿的錯(cuò)誤和漏洞,故保證并發(fā)程序的正確性具有十分重要的意義[2]。近些年提出的上下文定界方法是一種適合并發(fā)程序的分析技術(shù),其思想是僅考慮有限次上下文切換(控制權(quán)從一個(gè)線程切換到另一個(gè)線程)之內(nèi)程序執(zhí)行的計(jì)算。由于在有限次上下文切換之內(nèi)可發(fā)現(xiàn)許多并發(fā)相關(guān)的錯(cuò)誤,上下文定界思想有助于程序分析。在程序中存在遞歸和過(guò)程調(diào)用的情況下,雖然被搜索的狀態(tài)空間是無(wú)界的,但上下文定界可達(dá)問(wèn)題是可判定的[3]。
針對(duì)Fork/Join并行性的并發(fā)程序進(jìn)行可達(dá)性分析,主要基于以下考慮:Fork/Join 并行性涉及到動(dòng)態(tài)線程創(chuàng)建,而動(dòng)態(tài)線程創(chuàng)建對(duì)于構(gòu)建操作系統(tǒng)的組件是非常重要的[4]。例如:(1)文件系統(tǒng)、設(shè)備驅(qū)動(dòng)、無(wú)封裝數(shù)據(jù)結(jié)構(gòu)等軟件模塊的無(wú)界并發(fā)執(zhí)行;(2)異步行為的生成:例如創(chuàng)建一個(gè)線程、回調(diào)函數(shù)等;(3)實(shí)現(xiàn)應(yīng)用軟件的并行化執(zhí)行,充分利用多核體系結(jié)構(gòu)的強(qiáng)大性能。
Qadeer提出的上下文定界模型檢驗(yàn)算法假設(shè)全局狀態(tài)集合G 是有限的。算法執(zhí)行過(guò)程中迭代地增加執(zhí)行上下文的數(shù)目,在一個(gè)執(zhí)行上下文內(nèi),全局狀態(tài)對(duì)于當(dāng)前線程是局部的,只有該線程可以訪問(wèn)全局狀態(tài)。上下文切換時(shí)同步該全局狀態(tài),使得其他線程共享全局狀態(tài)。對(duì)于給定正整數(shù)k,該算法可以搜索并發(fā)下推系統(tǒng)在k 次上下文切換執(zhí)行所有可達(dá)的格局集合。k-定界可達(dá)算法如下所示:
算法1k-定界可達(dá)算法
對(duì)于并發(fā)下推系統(tǒng)P=(G,Γ,Δ0,…,ΔN,gin,win)和正整數(shù)k,該算法是可終止的,并且判定該問(wèn)題的復(fù)雜度為O(k3(N|G|)k|P|5)。
隨著多核處理器逐漸成為主流,并發(fā)程序通過(guò)引入Fork/Join并行任務(wù)調(diào)度模式,將一個(gè)規(guī)模較大的任務(wù)分解為更細(xì)粒度的子任務(wù)(線程)并行執(zhí)行,從而充分利用多核處理器的計(jì)算能力。由于任務(wù)可以用線程的執(zhí)行模擬,因此下文中用線程的概念來(lái)表示任務(wù)。
Fork/Join并行模式是獲取更高并行性能的最簡(jiǎn)單和高效的設(shè)計(jì)技術(shù)。Fork操作創(chuàng)建一個(gè)新的并行執(zhí)行子線程,Join操作使得當(dāng)前線程等待執(zhí)行,直到新創(chuàng)建的子線程執(zhí)行結(jié)束。圖1給出了一個(gè)Fork/Join模式的示意圖,位于圖上部的線程依賴于位于其下的子線程的執(zhí)行,只有當(dāng)所有的子線程都執(zhí)行結(jié)束之后,調(diào)用者才能獲得線程0的返回結(jié)果。
允許Fork/Join并行模式的并發(fā)程序的線程標(biāo)識(shí)符的使用是有限制的,因此對(duì)存儲(chǔ)線程標(biāo)識(shí)符的變量的使用也是有限制的。Fork操作創(chuàng)建一個(gè)線程標(biāo)識(shí)符,存儲(chǔ)在一個(gè)變量中。隨后,該線程標(biāo)識(shí)符被拷貝存儲(chǔ)到其父線程的線程標(biāo)識(shí)符變量中。最后,Join操作監(jiān)視該變量中包含的線程標(biāo)識(shí)符,該線程執(zhí)行結(jié)束后返回父線程繼續(xù)執(zhí)行。
Figure 1 Fork/Join model圖1 Fork/Join 模式示意圖
本節(jié)定義Fork/Join并行性的并發(fā)程序的抽象模型——?jiǎng)討B(tài)并發(fā)下推系統(tǒng)。在并發(fā)程序中,各個(gè)線程模型可用新線程的下推系統(tǒng)來(lái)創(chuàng)建。線程包含局部變量并可訪問(wèn)全局(共享)變量。使用棧字母表Γ 模擬局部變量值,G 中的狀態(tài)模擬全局變量的值。為了支持動(dòng)態(tài)的Fork/Join并行模式,需使用存儲(chǔ)線程標(biāo)識(shí)符的程序變量對(duì)線程標(biāo)識(shí)符進(jìn)行存儲(chǔ)。線程標(biāo)識(shí)符取值于集合Tid={0,1,2,…}。新創(chuàng)建的線程標(biāo)識(shí)符存儲(chǔ)在其父線程的標(biāo)識(shí)符變量中,父線程可對(duì)該變量中包含的線程標(biāo)識(shí)符對(duì)應(yīng)的子線程執(zhí)行Join操作。
4.2.1 語(yǔ)法
一個(gè)動(dòng)態(tài)并發(fā)下推系統(tǒng)可表示為一個(gè)七元組(G,Γ,Δ,ΔF,ΔJ,gin,γin)。其中:
(1)G 是所有全局變量賦值的(無(wú)限)集合,由包含布爾值的全局變量集合GBV 和包含線程標(biāo)識(shí)符的全局變量集合GTV 組成。
(2)Γ 是所有局部變量賦值的(無(wú)限)集合,由包含布爾值的局部變量集合LBV 和包含線程標(biāo)識(shí)符的局部變量集合LTV 組成。
(3)Δ?(G×Γ)×(G×Γ*)是描述任意線程單個(gè)步驟的遷移集合。
(4)ΔF?Tid×(G×Γ)×(G×Γ*)是Fork遷移關(guān)系。如果(t,〈g,γ〉,〈g′,w〉)∈ΔF,那么在全局狀態(tài)g 下,棧頂符號(hào)為γ的線程創(chuàng)建一個(gè)標(biāo)識(shí)符為t的線程,并修改全局狀態(tài)為g′,棧頂符號(hào)γ 替換為w。
(5)ΔJ?LTV×(G×Γ)×(G×Γ*)是Join遷移關(guān)系。如果(x,〈g,γ〉,〈g′,w〉)∈ΔJ,那么在全局狀態(tài)g 下,棧頂符號(hào)為γ 的線程阻塞,直至標(biāo)識(shí)符為γ(x)的線程執(zhí)行完畢。一旦等待線程執(zhí)行完畢,修改全局狀態(tài)為g′,并將棧頂符號(hào)γ 替換為w。
(6)gin是初始全局狀態(tài),對(duì)于所有的x∈GTV,gin(x)=0成立。
(7)γin是初始局部狀態(tài)(棧內(nèi)容),對(duì)于所有的x∈LTV,γin(x)=0成立。
4.2.2 語(yǔ)義
定義1ss∈Stacks=Tid →(?!龋纾蔷€程標(biāo)識(shí)符對(duì)應(yīng)的棧內(nèi)容,C=G×Tid×Stacks是動(dòng)態(tài)并發(fā)下推系統(tǒng)的格局集合,?C×C 是動(dòng)態(tài)并發(fā)下推系統(tǒng)格局上的遷移關(guān)系。
每個(gè)動(dòng)態(tài)并發(fā)下推系統(tǒng)使用一個(gè)特殊符號(hào)$?Γ 來(lái)標(biāo)記每個(gè)線程的棧底。動(dòng)態(tài)并發(fā)下推系統(tǒng)的一個(gè)格局是一個(gè)元組〈g,n,ss〉,其中g(shù) 是全局狀態(tài),n是最后被創(chuàng)建的線程的標(biāo)識(shí)符,ss(t)是線程t∈Tid 的棧。動(dòng)態(tài)并發(fā)下推系統(tǒng)的執(zhí)行從格局〈gin,0,ss0〉開(kāi)始,其中對(duì)于所有的t∈Tid,ss0(t)=γin$。
以下規(guī)則定義了從格局〈gin,0,ss0〉開(kāi)始線程t可以執(zhí)行的遷移:
所有的規(guī)則都包含條件t≤n,表明線程t必須已經(jīng)被創(chuàng)建。因此,只有線程0可以從初始格局〈gin,0,ss0〉開(kāi)始執(zhí)行。規(guī)則(I)允許線程t執(zhí)行遷移關(guān)系Δ 中的一個(gè)遷移。規(guī)則(II)表示線程t終止執(zhí)行,即當(dāng)線程t的棧頂符號(hào)是$時(shí),線程t從棧中彈出符號(hào)$,不改變?nèi)譅顟B(tài),從而線程t終止執(zhí)行。規(guī)則(III)模擬線程的Fork操作,即線程t根據(jù)一個(gè)Fork遷移關(guān)系創(chuàng)建一個(gè)標(biāo)識(shí)符為n+1的新線程。規(guī)則(IV)模擬線程的Join操作,線程t等待標(biāo)識(shí)符為γ(x)的線程執(zhí)行結(jié)束之后,線程t繼續(xù)執(zhí)行下一個(gè)遷移,其中γ 是線程t 的棧頂符號(hào)。使用一個(gè)空棧來(lái)表示線程終止。
本節(jié)說(shuō)明如何將一個(gè)動(dòng)態(tài)并發(fā)下推系統(tǒng)的k-定界可達(dá)問(wèn)題轉(zhuǎn)換為包含k+1個(gè)線程的并發(fā)下推系統(tǒng)的k-定界可達(dá)問(wèn)題。給定動(dòng)態(tài)并發(fā)系統(tǒng)P 和正整數(shù)k,可以從中提取一個(gè)包含k+1個(gè)線程的并發(fā)下推系統(tǒng)Pk,這些線程的標(biāo)識(shí)符取值為{0,1,…,k},并且足以驗(yàn)證Pk的k-定界執(zhí)行。3.2節(jié)給出的算法可解決并發(fā)下推系統(tǒng)k-定界可達(dá)問(wèn)題。
該簡(jiǎn)化方法的主要思想是:在一個(gè)k-定界執(zhí)行中,至多k個(gè)不同的線程會(huì)執(zhí)行一次遷移??梢允褂肞k中標(biāo)識(shí)符為{0,1,…,k-1}的k 個(gè)線程的遷移來(lái)模擬這k 個(gè)線程的遷移。Pk中的最后一個(gè)標(biāo)識(shí)符為k 的線程從不執(zhí)行遷移,該線程用于模擬P 中其它線程的存在。令Tidk={0,1,…,k}為整數(shù)k限定的線程標(biāo)識(shí)符集合。AbsGk和AbsΓk分別是有限全局狀態(tài)集合和有限局部狀態(tài)集合,其中包含線程標(biāo)識(shí)符的變量?jī)H從Tidk中取值。
給定動(dòng)態(tài)并發(fā)下推系統(tǒng)P=(G,Γ,Δ,ΔF,ΔJ,gin,γin)和正整數(shù)k,可以構(gòu)造出并發(fā)下推系統(tǒng)Pk=(AbsGk× Tidk×T (Tidk),AbsΓk∪{$},Δ0,…,Δk,(gin,0,?),γin$)。該并發(fā)下推系統(tǒng)Pk包含k+1個(gè)線程。Pk的全局狀態(tài)是一個(gè)三元組(g,n,α),其中g(shù) 是全局變量的賦值,n 是允許執(zhí)行遷移的線程對(duì)應(yīng)的最大線程標(biāo)識(shí)符,α 是終止線程對(duì)應(yīng)的線程標(biāo)識(shí)符集合。初始全局狀態(tài)是(gin,0,?),表明最初只有線程0可以執(zhí)行一個(gè)遷移并且其它線程沒(méi)有執(zhí)行。
以下規(guī)則定義了線程t的遷移關(guān)系Δt上的遷移:
(I′)如果t≤n,(〈g,γ〉,〈g′,w〉)∈Δ,添加遷移(〈(g,n,α),γ〉,〈(g′,n,α),w〉)到Δt中。
(II′)如果t≤n,添加遷移(〈(g,n,α),$〉,〈(g,n,α∪{t}),ε〉)到Δt中。
(III′a)如果t≤n,n+1<k,(n+1,〈g,γ〉,〈g′,w〉)∈ΔF,添加遷移(〈(g,n,α),γ〉,〈(g′,n+1,α),w〉)到Δt中。
(III′b)如果t≤n,(k,〈g,γ〉,〈g′,w〉)∈ΔF,添加遷移(〈(g,n,α),γ〉,〈(g′,n,α),w〉)到Δt中。
(IV′)如果t≤n,x∈LTV,(x,〈g,γ〉,〈g′,w〉)∈ΔJ,γ(x)∈α,添加遷移(〈(g,n,α),γ〉,〈(g′,n,α),w〉)到Δt中。
所有的規(guī)則都包含條件t≤n,表明從動(dòng)態(tài)并發(fā)下推系統(tǒng)中選擇的線程必須已經(jīng)被創(chuàng)建。如果t>n,線程t在格局〈(g,n,α),γ〉下沒(méi)有可以執(zhí)行的遷移。規(guī)則(I′)將Δ 中的遷移添加到Δt中。規(guī)則(II′)將棧為空的線程t添加到終止線程集合。規(guī)則(III′a)和規(guī)則(III′b)處理P 線程中的創(chuàng)建,是該轉(zhuǎn)換方法中最重要的部分。規(guī)則(III′a)對(duì)應(yīng)于新創(chuàng)建線程參與k-定界執(zhí)行的情況。該規(guī)則將計(jì)數(shù)器加1,允許線程n+1開(kāi)始模擬新創(chuàng)建的線程。規(guī)則(III′b)對(duì)應(yīng)于新創(chuàng)建線程不參與k-定界執(zhí)行的情況。該規(guī)則保持計(jì)數(shù)器n 不變,從而保存Pk中現(xiàn)有的線程標(biāo)識(shí)符。這兩個(gè)規(guī)則將ΔF中創(chuàng)建線程的遷移關(guān)系添加到線程t 的遷移集合Δt中。規(guī)則(IV′)處理Join運(yùn)算符,將所有先前終止線程的標(biāo)識(shí)符都存儲(chǔ)在α中。同時(shí),該規(guī)則將掛起線程的遷移ΔJ添加到Δt中。
由動(dòng)態(tài)并發(fā)下推系統(tǒng)P 構(gòu)造并發(fā)下推系統(tǒng)Pk時(shí),從初始全局狀態(tài)(gin,0,?)開(kāi)始,根據(jù)以上規(guī)則構(gòu)造線程t(0≤t≤n<k-1)可以執(zhí)行的遷移關(guān)系集合。構(gòu)造線程t的遷移關(guān)系集合Δt時(shí),線程t的所有可執(zhí)行遷移(包含F(xiàn)ork和Join遷移關(guān)系)均從動(dòng)態(tài)并發(fā)下推系統(tǒng)P 的遷移關(guān)系集合中提取。當(dāng)線程標(biāo)識(shí)符t=k時(shí),構(gòu)造過(guò)程終止,從而構(gòu)造出模擬P 的k-定界執(zhí)行的并發(fā)下推系統(tǒng)Pk。
本文給出了Fork/Join并行模式的并發(fā)程序的抽象模型——?jiǎng)討B(tài)并發(fā)下推系統(tǒng)的定界可達(dá)性分析。通過(guò)將動(dòng)態(tài)并發(fā)下推系統(tǒng)P 的k-定界可達(dá)問(wèn)題簡(jiǎn)化為模擬其k-定界執(zhí)行的并發(fā)下推系統(tǒng)Pk,從動(dòng)態(tài)并發(fā)下推系統(tǒng)P 中提取的并發(fā)下推系統(tǒng)的k-定界可達(dá)性問(wèn)題可使用現(xiàn)有的k-定界可達(dá)算法解決。能否直接對(duì)允許動(dòng)態(tài)線程創(chuàng)建的并發(fā)程序進(jìn)行可達(dá)性分析,及給出其求解算法,將是未來(lái)值得深入研究的問(wèn)題。
[1]Lea D.A Java fork/join framework[C]∥Proc of 2000ACM Java Grande Conference,2000:36-43.
[2]Queille J,Sifakis J.Specification and verification of concurrent systems in CESAR[C]∥Proc of the 5th International Symposium on Programming,1981:337-351.
[3]Qadeer S.The case for context-bounded verification of concurrent programs[C]∥Proc of the 15th International Workshop on Model Checking Software,2008:3-6.
[4]Atig M F,Bouajjani A,Qadeer S.Context-bounded analysis for concurrent programs with dynamic creation of threads[C]∥Proc of the 15th International Conference on Tools and Al-gorithms for the Construction and Analysis of Systems,2009:107-123.
[5]Clarke E M,Grumberg O,Peled D A.Model checking[M].Cambridge:MIT Press,2000.
[6]Autebert J M,Berstel J,Boasson L.Context-free languages and pushdown automata[M]∥Handbook of Formal Languages,New York:Springer-Verlag,1997:111-174.
[7]Schwoon S.Model-checking pushdown systems[D].Munchen:Lehrstuhl fur Informatic VII der Technischen University,2000.