• 
    

    
    

      99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

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

      2013-06-07 08:17:48錢俊彥賈書(shū)貴蔡國(guó)永趙嶺忠
      關(guān)鍵詞:定界標(biāo)識(shí)符線程

      錢俊彥,賈書(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.

      猜你喜歡
      定界標(biāo)識(shí)符線程
      淺析5G V2X 通信應(yīng)用現(xiàn)狀及其側(cè)鏈路標(biāo)識(shí)符更新技術(shù)
      基于底層虛擬機(jī)的標(biāo)識(shí)符混淆方法
      RTK技術(shù)在土地勘測(cè)定界中的應(yīng)用研究
      一類DC規(guī)劃問(wèn)題的分支定界算法
      基于區(qū)塊鏈的持久標(biāo)識(shí)符系統(tǒng)①
      基于外定界橢球集員估計(jì)的純方位目標(biāo)跟蹤
      淺談linux多線程協(xié)作
      數(shù)字美術(shù)館“數(shù)字對(duì)象唯一標(biāo)識(shí)符系統(tǒng)”建設(shè)需求淺議
      Linux線程實(shí)現(xiàn)技術(shù)研究
      基于MapGIS土地勘測(cè)定界中分類面積統(tǒng)計(jì)的應(yīng)用
      邢台市| 潼南县| 崇文区| 尉犁县| 文成县| 遵化市| 永靖县| 阳高县| 自治县| 无为县| 喀什市| 隆回县| 手游| 章丘市| 武功县| 定陶县| 金湖县| 延庆县| 平湖市| 江西省| 台湾省| 临江市| 邛崃市| 平山县| 会理县| 南开区| 鄂伦春自治旗| 郯城县| 炉霍县| 上杭县| 合山市| 格尔木市| 积石山| 新乐市| 嵩明县| 会宁县| 阿合奇县| 文化| 康马县| 拉萨市| 夹江县|