基于上下文定界的Fork／Join并行性的并發(fā)程序可達(dá)性分析＊

錢俊彥，賈書(shū)貴，蔡國(guó)永，趙嶺忠

（1.桂林電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院，廣西 桂林 541004）；2.并行與分布處理國(guó)家重點(diǎn)實(shí)驗(yàn)室，湖南 長(zhǎng)沙 410073）

1 引言

無(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)大性能。

2 下推系統(tǒng)

3 并發(fā)下推系統(tǒng)

3.1 定界可達(dá)問(wèn)題

3.2 k－定界可達(dá)算法

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）。

4 Fork／Join并行模式的并發(fā)程序分析

隨著多核處理器逐漸成為主流，并發(fā)程序通過(guò)引入Fork／Join并行任務(wù)調(diào)度模式，將一個(gè)規(guī)模較大的任務(wù)分解為更細(xì)粒度的子任務(wù)（線程）并行執(zhí)行，從而充分利用多核處理器的計(jì)算能力。由于任務(wù)可以用線程的執(zhí)行模擬，因此下文中用線程的概念來(lái)表示任務(wù)。

4.1 Fork／Join并行模式

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 模式示意圖

4.2 動(dòng)態(tài)并發(fā)下推系統(tǒng)

本節(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)表示線程終止。

4.3 簡(jiǎn)化為并發(fā)下推系統(tǒng)

本節(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。

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

本文給出了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.