基于上下文定界的Fork／Join并行性的并發程序可達性分析＊

錢俊彥，賈書貴，蔡國永，趙嶺忠

（1.桂林電子科技大學計算機科學與工程學院，廣西 桂林 541004）；2.并行與分布處理國家重點實驗室，湖南 長沙 410073）

1 引言

無論從理論，還是實踐角度來看，并發程序驗證都是極具挑戰性的問題。隨著多核技術日益發展，通過引入Fork／Join并行性，并發程序將任務分解為更細粒度的子任務并行執行，從而充分利用多核處理器提供的計算性能［1］。但是，多個線程之間的交錯執行可能會產生隱匿的錯誤和漏洞，故保證并發程序的正確性具有十分重要的意義［2］。近些年提出的上下文定界方法是一種適合并發程序的分析技術，其思想是僅考慮有限次上下文切換（控制權從一個線程切換到另一個線程）之內程序執行的計算。由于在有限次上下文切換之內可發現許多并發相關的錯誤，上下文定界思想有助于程序分析。在程序中存在遞歸和過程調用的情況下，雖然被搜索的狀態空間是無界的，但上下文定界可達問題是可判定的［3］。

針對Fork／Join并行性的并發程序進行可達性分析，主要基于以下考慮：Fork／Join 并行性涉及到動態線程創建，而動態線程創建對于構建操作系統的組件是非常重要的［4］。例如：（1）文件系統、設備驅動、無封裝數據結構等軟件模塊的無界并發執行；（2）異步行為的生成：例如創建一個線程、回調函數等；（3）實現應用軟件的并行化執行，充分利用多核體系結構的強大性能。

2 下推系統

3 并發下推系統

3.1 定界可達問題

3.2 k－定界可達算法

Qadeer提出的上下文定界模型檢驗算法假設全局狀態集合G 是有限的。算法執行過程中迭代地增加執行上下文的數目，在一個執行上下文內，全局狀態對于當前線程是局部的，只有該線程可以訪問全局狀態。上下文切換時同步該全局狀態，使得其他線程共享全局狀態。對于給定正整數k，該算法可以搜索并發下推系統在k 次上下文切換執行所有可達的格局集合。k－定界可達算法如下所示：

算法1k－定界可達算法

對于并發下推系統P＝（G，Γ，Δ0，…，ΔN，gin，win）和正整數k，該算法是可終止的，并且判定該問題的復雜度為O（k3（N｜G｜）k｜P｜5）。

4 Fork／Join并行模式的并發程序分析

隨著多核處理器逐漸成為主流，并發程序通過引入Fork／Join并行任務調度模式，將一個規模較大的任務分解為更細粒度的子任務（線程）并行執行，從而充分利用多核處理器的計算能力。由于任務可以用線程的執行模擬，因此下文中用線程的概念來表示任務。

4.1 Fork／Join并行模式

Fork／Join并行模式是獲取更高并行性能的最簡單和高效的設計技術。Fork操作創建一個新的并行執行子線程，Join操作使得當前線程等待執行，直到新創建的子線程執行結束。圖1給出了一個Fork／Join模式的示意圖，位于圖上部的線程依賴于位于其下的子線程的執行，只有當所有的子線程都執行結束之后，調用者才能獲得線程0的返回結果。

允許Fork／Join并行模式的并發程序的線程標識符的使用是有限制的，因此對存儲線程標識符的變量的使用也是有限制的。Fork操作創建一個線程標識符，存儲在一個變量中。隨后，該線程標識符被拷貝存儲到其父線程的線程標識符變量中。最后，Join操作監視該變量中包含的線程標識符，該線程執行結束后返回父線程繼續執行。

Figure 1 Fork／Join model圖1 Fork／Join 模式示意圖

4.2 動態并發下推系統

本節定義Fork／Join并行性的并發程序的抽象模型——動態并發下推系統。在并發程序中，各個線程模型可用新線程的下推系統來創建。線程包含局部變量并可訪問全局（共享）變量。使用棧字母表Γ 模擬局部變量值，G 中的狀態模擬全局變量的值。為了支持動態的Fork／Join并行模式，需使用存儲線程標識符的程序變量對線程標識符進行存儲。線程標識符取值于集合Tid＝｛0，1，2，…｝。新創建的線程標識符存儲在其父線程的標識符變量中，父線程可對該變量中包含的線程標識符對應的子線程執行Join操作。

4.2.1 語法

一個動態并發下推系統可表示為一個七元組（G，Γ，Δ，ΔF，ΔJ，gin，γin）。其中：

（1）G 是所有全局變量賦值的（無限）集合，由包含布爾值的全局變量集合GBV 和包含線程標識符的全局變量集合GTV 組成。

（2）Γ 是所有局部變量賦值的（無限）集合，由包含布爾值的局部變量集合LBV 和包含線程標識符的局部變量集合LTV 組成。

（3）Δ?（G×Γ）×（G×Γ＊）是描述任意線程單個步驟的遷移集合。

（4）ΔF?Tid×（G×Γ）×（G×Γ＊）是Fork遷移關系。如果（t，〈g，γ〉，〈g′，w〉）∈ΔF，那么在全局狀態g 下，棧頂符號為γ的線程創建一個標識符為t的線程，并修改全局狀態為g′，棧頂符號γ 替換為w。

（5）ΔJ?LTV×（G×Γ）×（G×Γ＊）是Join遷移關系。如果（x，〈g，γ〉，〈g′，w〉）∈ΔJ，那么在全局狀態g 下，棧頂符號為γ 的線程阻塞，直至標識符為γ（x）的線程執行完畢。一旦等待線程執行完畢，修改全局狀態為g′，并將棧頂符號γ 替換為w。

（6）gin是初始全局狀態，對于所有的x∈GTV，gin（x）＝0成立。

（7）γin是初始局部狀態（棧內容），對于所有的x∈LTV，γin（x）＝0成立。

4.2.2 語義

定義1ss∈Stacks＝Tid →（?！龋纾蔷€程標識符對應的棧內容，C＝G×Tid×Stacks是動態并發下推系統的格局集合，?C×C 是動態并發下推系統格局上的遷移關系。

每個動態并發下推系統使用一個特殊符號＄?Γ 來標記每個線程的棧底。動態并發下推系統的一個格局是一個元組〈g，n，ss〉，其中g 是全局狀態，n是最后被創建的線程的標識符，ss（t）是線程t∈Tid 的棧。動態并發下推系統的執行從格局〈gin，0，ss0〉開始，其中對于所有的t∈Tid，ss0（t）＝γin＄。

以下規則定義了從格局〈gin，0，ss0〉開始線程t可以執行的遷移：

所有的規則都包含條件t≤n，表明線程t必須已經被創建。因此，只有線程0可以從初始格局〈gin，0，ss0〉開始執行。規則（I）允許線程t執行遷移關系Δ 中的一個遷移。規則（II）表示線程t終止執行，即當線程t的棧頂符號是＄時，線程t從棧中彈出符號＄，不改變全局狀態，從而線程t終止執行。規則（III）模擬線程的Fork操作，即線程t根據一個Fork遷移關系創建一個標識符為n＋1的新線程。規則（IV）模擬線程的Join操作，線程t等待標識符為γ（x）的線程執行結束之后，線程t繼續執行下一個遷移，其中γ 是線程t 的棧頂符號。使用一個空棧來表示線程終止。

4.3 簡化為并發下推系統

本節說明如何將一個動態并發下推系統的k－定界可達問題轉換為包含k＋1個線程的并發下推系統的k－定界可達問題。給定動態并發系統P 和正整數k，可以從中提取一個包含k＋1個線程的并發下推系統Pk，這些線程的標識符取值為｛0，1，…，k｝，并且足以驗證Pk的k－定界執行。3.2節給出的算法可解決并發下推系統k－定界可達問題。

該簡化方法的主要思想是：在一個k－定界執行中，至多k個不同的線程會執行一次遷移?？梢允褂肞k中標識符為｛0，1，…，k－1｝的k 個線程的遷移來模擬這k 個線程的遷移。Pk中的最后一個標識符為k 的線程從不執行遷移，該線程用于模擬P 中其它線程的存在。令Tidk＝｛0，1，…，k｝為整數k限定的線程標識符集合。AbsGk和AbsΓk分別是有限全局狀態集合和有限局部狀態集合，其中包含線程標識符的變量僅從Tidk中取值。

給定動態并發下推系統P＝（G，Γ，Δ，ΔF，ΔJ，gin，γin）和正整數k，可以構造出并發下推系統Pk＝（AbsGk× Tidk×T （Tidk），AbsΓk∪｛＄｝，Δ0，…，Δk，（gin，0，?），γin＄）。該并發下推系統Pk包含k＋1個線程。Pk的全局狀態是一個三元組（g，n，α），其中g 是全局變量的賦值，n 是允許執行遷移的線程對應的最大線程標識符，α 是終止線程對應的線程標識符集合。初始全局狀態是（gin，0，?），表明最初只有線程0可以執行一個遷移并且其它線程沒有執行。

以下規則定義了線程t的遷移關系Δ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中。

所有的規則都包含條件t≤n，表明從動態并發下推系統中選擇的線程必須已經被創建。如果t＞n，線程t在格局〈（g，n，α），γ〉下沒有可以執行的遷移。規則（I′）將Δ 中的遷移添加到Δt中。規則（II′）將棧為空的線程t添加到終止線程集合。規則（III′a）和規則（III′b）處理P 線程中的創建，是該轉換方法中最重要的部分。規則（III′a）對應于新創建線程參與k－定界執行的情況。該規則將計數器加1，允許線程n＋1開始模擬新創建的線程。規則（III′b）對應于新創建線程不參與k－定界執行的情況。該規則保持計數器n 不變，從而保存Pk中現有的線程標識符。這兩個規則將ΔF中創建線程的遷移關系添加到線程t 的遷移集合Δt中。規則（IV′）處理Join運算符，將所有先前終止線程的標識符都存儲在α中。同時，該規則將掛起線程的遷移ΔJ添加到Δt中。

由動態并發下推系統P 構造并發下推系統Pk時，從初始全局狀態（gin，0，?）開始，根據以上規則構造線程t（0≤t≤n＜k－1）可以執行的遷移關系集合。構造線程t的遷移關系集合Δt時，線程t的所有可執行遷移（包含Fork和Join遷移關系）均從動態并發下推系統P 的遷移關系集合中提取。當線程標識符t＝k時，構造過程終止，從而構造出模擬P 的k－定界執行的并發下推系統Pk。

5 結束語

本文給出了Fork／Join并行模式的并發程序的抽象模型——動態并發下推系統的定界可達性分析。通過將動態并發下推系統P 的k－定界可達問題簡化為模擬其k－定界執行的并發下推系統Pk，從動態并發下推系統P 中提取的并發下推系統的k－定界可達性問題可使用現有的k－定界可達算法解決。能否直接對允許動態線程創建的并發程序進行可達性分析，及給出其求解算法，將是未來值得深入研究的問題。

［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.