劉磊，劉豐，任俊綺，呂帥,2

(1. 吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012；2. 吉林大學(xué) 數(shù)學(xué)學(xué)院，吉林 長春 130012)

?

基于細(xì)胞膜演算的Dryad形式化描述

劉磊1，劉豐1，任俊綺1，呂帥1,2

(1. 吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，吉林 長春 130012；2. 吉林大學(xué) 數(shù)學(xué)學(xué)院，吉林 長春 130012)

由于Dryad編程模型的實(shí)現(xiàn)并不開源，導(dǎo)致關(guān)于Dryad編程模型的理論研究較為缺乏。本文利用細(xì)胞膜演算在描述并發(fā)系統(tǒng)的優(yōu)勢，對Dryad編程模型中任務(wù)執(zhí)行過程進(jìn)行了準(zhǔn)確清晰的形式化描述，并對Dryad編程模型的容錯機(jī)制進(jìn)行了描述，最后通過一個實(shí)例檢驗(yàn)了形式化描述結(jié)果。本文的形式化描述方法有效地豐富了編程模型的理論體系，為編程人員提供了任務(wù)調(diào)度的優(yōu)化依據(jù)，同時該形式化描述還可作為驗(yàn)證程序正確性的輔助工具。

云計(jì)算；編程模型；Dryad；細(xì)胞膜演算；形式化；有向無環(huán)圖

云計(jì)算是當(dāng)今IT產(chǎn)業(yè)發(fā)展的主要趨勢，它改變了傳統(tǒng)的服務(wù)方式，為了能夠低成本、高效率地處理海量數(shù)據(jù)，各大互聯(lián)網(wǎng)公司都建立了自己的大型集群系統(tǒng)[1-2]。云計(jì)算的基礎(chǔ)設(shè)施以商用機(jī)器集群為主，為利于編程人員的軟件開發(fā)，提出了編程模型的概念。

MapReduce是Google于2004年提出的編程模型，通過將作業(yè)簡化為Map和Reduce任務(wù)的處理，大大降低了并行編程難度[3]。Hadoop項(xiàng)目的開源實(shí)現(xiàn)使得MapReduce編程模型得到了更為快速的發(fā)展[4-6]。不同于MapReduce編程模型固定的兩階段處理方式，微軟開發(fā)的通用執(zhí)行引擎Dryad，通過將一個程序表示成一個有向無環(huán)圖(directed acyclic graph，DAG)，能有效地分布式處理大規(guī)模數(shù)據(jù)，具有較強(qiáng)的擴(kuò)展性[7]。相比MapReduce，Dryad編程模型能更加有效地處理連接運(yùn)算、迭代運(yùn)算等。Dryad由于采用了顯式并行，并不適合直接用來解決實(shí)際問題，因此微軟開發(fā)了高層次編程語言DryadLINQ[8]，降低了在大規(guī)模集群上開發(fā)人員的編程難度。

編程模型的形式化描述便于人們更為準(zhǔn)確地理解編程模型，對其進(jìn)行研究具有重要的意義。L?mmel提出了MapReduce的嚴(yán)格準(zhǔn)確的形式化描述，以函數(shù)式編程語言Haskell為工具，明確了其中的類型變化[9]。通過使用Haskell語言對編程模型Map-Reduce-Merge進(jìn)行了嚴(yán)格的描述，為進(jìn)行支持連接運(yùn)算的并行編程模型的后續(xù)研究提供了理論基礎(chǔ)[10]。戚正偉等提出了一種新的事務(wù)處理形式化方法——細(xì)胞膜演算[11]，并利用細(xì)胞膜演算形式化描述了Web服務(wù)中原子事務(wù)協(xié)調(diào)協(xié)議[12]。細(xì)胞膜演算具有非常強(qiáng)大的描述能力，且其多個細(xì)胞膜里面的對象可以同時進(jìn)行反應(yīng)，因而其在描述并行系統(tǒng)方面具有獨(dú)特的優(yōu)勢。

Dryad編程模型的執(zhí)行過程基于DAG，具有較好的通用性，但Dryad編程模型的不開源導(dǎo)致其理論研究相對較少?；诩?xì)胞膜演算在描述動態(tài)、移動的并發(fā)系統(tǒng)的獨(dú)特優(yōu)勢，本文利用其對Dryad編程模型的執(zhí)行流程進(jìn)行嚴(yán)格的形式化描述。

1 基礎(chǔ)知識

1.1 細(xì)胞膜演算

細(xì)胞膜演算是P-systems相應(yīng)的演算系統(tǒng)。令類型對象集為Σ，其元素為T，對象多集中的元素為a、b、c、…，標(biāo)識符集為N，其元素為i、j、k、…，細(xì)胞膜演算定義如下

M,M′ ::= 0 | [iO,R,M] |MM′

O,O′ ::= 0 |a:T|OO′

λ::=δ|σk|ηk|M

1.2 Dryad編程模型

Dryad是一個用于并行數(shù)據(jù)應(yīng)用的分布式執(zhí)行引擎，一個Dryad的整體結(jié)構(gòu)由該任務(wù)的通信流決定，一個任務(wù)是一個DAG，其中頂點(diǎn)表示程序，邊表示數(shù)據(jù)通道，通過運(yùn)行時調(diào)度將該DAG自動地映射到物理資源。

2 形式化描述

DAG是Dryad編程模型的一個核心結(jié)構(gòu)，編程模型的執(zhí)行過程以及容錯性等方面都基于該DAG。

針對一個特定的DAG，將執(zhí)行相同任務(wù)的結(jié)點(diǎn)劃分為同層，并且同層結(jié)點(diǎn)一般是并行執(zhí)行的。將當(dāng)前正在執(zhí)行的同層結(jié)點(diǎn)認(rèn)定為當(dāng)前層，將當(dāng)前層結(jié)點(diǎn)指向的結(jié)點(diǎn)認(rèn)定為下一層。本文將DAG中相鄰層之間的關(guān)系分為4種，進(jìn)行形式化描述。

2.1 相鄰層結(jié)點(diǎn)為一一對應(yīng)關(guān)系(o2o規(guī)則)

假設(shè)當(dāng)前層有n個結(jié)點(diǎn)，下一層也為n個結(jié)點(diǎn)，當(dāng)前層的每一個結(jié)點(diǎn)都有一條邊指向下一層的結(jié)點(diǎn)，且分別指向不同的結(jié)點(diǎn)，則稱當(dāng)前層與下一層為一一對應(yīng)關(guān)系，如圖1所示。

規(guī)則o2o的具體描述如下：當(dāng)前層結(jié)點(diǎn)有n個細(xì)胞膜，各個細(xì)胞膜內(nèi)反應(yīng)后產(chǎn)生一個代表結(jié)束狀態(tài)的對象End:State，該對象會觸發(fā)細(xì)胞膜內(nèi)的溶解規(guī)則，溶解后產(chǎn)生的對象為O1,…,On，每一個對象會觸發(fā)父細(xì)胞的規(guī)則集R中的一條反應(yīng)規(guī)則，產(chǎn)生一個新的細(xì)胞膜。規(guī)則集R如下

R1:O1→M1，其中M1: [1O1,Ru]

?

Rn:On→Mn， 其中Mn: [nOn,Ru]

圖1 一對一對應(yīng)關(guān)系Fig.1 One-to-one correspondence

2.2 相鄰層結(jié)點(diǎn)之間為一對多對應(yīng)關(guān)系(o2m規(guī)則)

假設(shè)當(dāng)前層有1個結(jié)點(diǎn)，下一層有n個結(jié)點(diǎn)，當(dāng)前層結(jié)點(diǎn)有n條邊分別指向下一層的每個結(jié)點(diǎn)，則稱當(dāng)前層與下一層為一對多關(guān)系，如圖2所示。

規(guī)則o2m的具體描述如下：當(dāng)前層有一個細(xì)胞膜，細(xì)胞膜內(nèi)反應(yīng)后產(chǎn)生對象End:State，該對象會觸發(fā)細(xì)胞膜內(nèi)的溶解規(guī)則，溶解后產(chǎn)生的對象為O1,…,On，每一個對象會觸發(fā)父細(xì)胞的規(guī)則集R中的一條反應(yīng)規(guī)則，產(chǎn)生一個新的細(xì)胞膜。規(guī)則集R如下

R1:O1→M1， 其中M1: [1O1,Ru]

?

Rn:On→Mn， 其中Mn: [nOn,Ru]

圖2 一對多對應(yīng)關(guān)系Fig.2 One-to-multiple correspondence

2.3 相鄰層結(jié)點(diǎn)之間為多對一對應(yīng)關(guān)系(m2o規(guī)則)

假設(shè)當(dāng)前層有n個結(jié)點(diǎn)，下一層有1個結(jié)點(diǎn)，且任意一個當(dāng)前層結(jié)點(diǎn)都有且僅有一條邊指向下一層的結(jié)點(diǎn)，稱當(dāng)前層與下一層為多對一關(guān)系，如圖3所示。

規(guī)則m2o的具體描述如下：當(dāng)前層有n個細(xì)胞膜，細(xì)胞膜內(nèi)反應(yīng)后產(chǎn)生對象End:State，該對象觸發(fā)細(xì)胞膜內(nèi)的溶解規(guī)則，當(dāng)前層每個細(xì)胞膜溶解后產(chǎn)生一個對象，溶解后產(chǎn)生的對象為O1,…,On，所有這些對象會觸發(fā)規(guī)則集R中的反應(yīng)規(guī)則，產(chǎn)生一個新的細(xì)胞膜。R中僅有1條規(guī)則：

R:O1O2…On→M其中M: [1O1O2…On,Ru]

圖3 多對一對應(yīng)關(guān)系Fig.3 Multiple-to-one correspondence

2.4 相鄰層結(jié)點(diǎn)之間為多對多對應(yīng)關(guān)系(m2m規(guī)則)

假設(shè)當(dāng)前層有m個結(jié)點(diǎn)，下一層有n個結(jié)點(diǎn)，并且當(dāng)前層每一個結(jié)點(diǎn)都有n條邊分別指向下一層的每一個結(jié)點(diǎn)，稱當(dāng)前層與下一層為多對多關(guān)系，如圖4所示。規(guī)則m2m的具體描述如下：當(dāng)前層有m個細(xì)胞膜，細(xì)胞膜內(nèi)反應(yīng)后產(chǎn)生對象End:State，該對象觸發(fā)細(xì)胞膜內(nèi)的溶解規(guī)則，每個細(xì)胞膜溶解后產(chǎn)生n個對象，共有m×n個對象。對于第i個(i= 1,…,m)細(xì)胞膜，溶解后產(chǎn)生的對象為Oi1,Oi2,…,Oin。m個對象會觸發(fā)規(guī)則集R的一條反應(yīng)規(guī)則，產(chǎn)生一個新的細(xì)胞膜。R中有n條規(guī)則，如下

R1:O11O21…Om1→M1，其中M1: [1O11O21…Om1,Ru]

?

Rn:O1nO2n…Omn→Mn，其中Mn: [nO1nO2n…Omn,Ru]

圖4 多對多對應(yīng)關(guān)系Fig.4 Multiple-to-multiple correspondence

2.5 復(fù)雜圖的形式化

舉例說明DAG中一些復(fù)雜情況都可以通過上述規(guī)則進(jìn)行形式化描述。

圖5中的DAG并不屬于簡單的分層情況。對于結(jié)點(diǎn)集A(包含A1、A2、A3和A4)和結(jié)點(diǎn)C，A屬于當(dāng)前層，C屬于下一層。對于結(jié)點(diǎn)C和結(jié)點(diǎn)集B(包含B1、B2、B3和B4)，C屬于當(dāng)前層，B屬于下一層。對于結(jié)點(diǎn)集A和B，A屬于當(dāng)前層，B屬于下一層。基于此，并不能簡單地把A、B、C各分為一層。根據(jù)輸入源結(jié)點(diǎn)的不同對B進(jìn)行劃分，可以得到三個集合為{B1}、{B2,B3}、{B4}。B1的輸入為A1和C，可將A1和C看作當(dāng)前層，B1看作下一層，應(yīng)用規(guī)則m2o來表示從A1和C到B1的執(zhí)行過程。同理，B4的輸入為A4和C，應(yīng)用規(guī)則m2o來表示從A4和C到B4的執(zhí)行過程。B2和B3的輸入都來自于C，可將C看作當(dāng)前層，B2和B3看作下一層，應(yīng)用規(guī)則o2m來表示從C到B2和B3的執(zhí)行過程。C的輸入為A1、A2、A3和A4，可將A1、A2、A3和A4看作當(dāng)前層，C看作下一層，應(yīng)用規(guī)則m2o來表示從A1、A2、A3和A4到C的執(zhí)行過程。

圖5 復(fù)合關(guān)系Fig.5 Composite correspondence

2.6 容錯機(jī)制

對于Dryad編程模型，容錯處理采用的方式是對該結(jié)點(diǎn)所分配的任務(wù)重新進(jìn)行分配。本文描述容錯機(jī)制的方式是令對象參加反應(yīng)后得到的結(jié)果有兩種情況，即對象按照規(guī)則反應(yīng)之后得到的結(jié)果是不確定的，一種情況為正常處理的結(jié)果，另一種情況為結(jié)點(diǎn)失效時的情況。規(guī)則如下

| O1O2…Om→ O1O2…OmFault:State

RF:Fault:State→δ

這里用對象Fault表示錯誤狀態(tài)。從規(guī)則R中可以看出，當(dāng)出錯時，不僅得到了錯誤狀態(tài)，同時原來的對象也得到了保留，這是因?yàn)榻Y(jié)點(diǎn)失效時重新分配的任務(wù)需要再次使用該節(jié)點(diǎn)處理的數(shù)據(jù)。而后，錯誤狀態(tài)導(dǎo)致細(xì)胞膜的溶解，所有對象重新回到父細(xì)胞膜中，重新按照規(guī)則生成子細(xì)胞膜，從而表示任務(wù)的重新分配。如果父細(xì)胞膜中已經(jīng)存在某些對象，則生成錯誤狀態(tài)時不需要生成這些對象。

3 描述算法

Dryad的描述算法Dryadformalization的整體思路為：首先找出出度為0的結(jié)點(diǎn)，然后將具有相同輸入的結(jié)點(diǎn)劃分為同一集合Next。若Next中只有一個元素，且該集合的輸入結(jié)點(diǎn)集Pre只有一個元素，則利用規(guī)則o2o；若Pre有多個元素，則利用規(guī)則m2o。若Next中有多個元素，且該集合的輸入結(jié)點(diǎn)集Pre只有一個元素，則利用規(guī)則o2m；若Pre有多個元素，則利用規(guī)則m2m。

算法Dryadformalization

輸入：DAG

輸出：當(dāng)前層結(jié)點(diǎn)集，下一層結(jié)點(diǎn)集，描述規(guī)則

1)whileDAG非空do

2)nodeset=DAG中所有出度為0的結(jié)點(diǎn)

3) 將nodeset進(jìn)行劃分，將具有相同輸入邊的結(jié)點(diǎn)劃分到同一個集合Next_i，并將Next_i的輸入結(jié)點(diǎn)放到集合Pre_i

4) 從DAG中刪掉Next_i中的每一個結(jié)點(diǎn)和指向這些結(jié)點(diǎn)的每一條邊

5)fori ←1to劃分得到的集合數(shù)do

6)ifNext_i中只有一個元素then

7)ifPre_i中只有一個元素then

8) 將三元組(o2o,Pre_i,Next_i)壓入stack

9)else

10) 將三元組(o2m,Pre_i,Next_i)壓入stack

11)else

12)ifPre_i中只有一個元素then

13) 將三元組(m2o,Pre_i,Next_i)壓入stack

14)else

15) 將三元組(m2m,Pre_i,Next_i)壓入stack

16)whilestack非空do

17) 彈出stack棧頂元素(rule,Pre_temp,Next_temp)

18) 用規(guī)則rule描述Pre_temp到Next_temp的執(zhí)行過程

給出Dryadformalization算法的完備性證明過程。

對于任意一個連通的DAG，一定存在出度為0的結(jié)點(diǎn)，否則該DAG必然存在環(huán)，每執(zhí)行一次循環(huán)(第1～15行)，將刪去所有出度為0的結(jié)點(diǎn)以及所有指向這些結(jié)點(diǎn)的邊。由于算法每次循環(huán)都會刪除一些結(jié)點(diǎn)，最終一定使得結(jié)點(diǎn)全部刪除完畢，此時第一個循環(huán)結(jié)束。棧中存儲了DAG的分層結(jié)果，以及對應(yīng)的描述規(guī)則。第二個循環(huán)(第16～18行)每次在棧中彈出一個元素，由于棧中元素的個數(shù)等同于第一個循環(huán)執(zhí)行的次數(shù)，因此棧中元素有限，所以第二個循環(huán)也一定會結(jié)束，因此對于任意給定的一個連通的DAG，Dryadformalization算法一定會終止，因此本文的描述方法是完備的。

4 實(shí)例驗(yàn)證

本文針對文獻(xiàn)[7]中的數(shù)據(jù)庫查詢實(shí)例進(jìn)行實(shí)例描述。該實(shí)例所對應(yīng)的聯(lián)系圖如圖6所示。

利用Dryad-Description算法，可以得到該實(shí)例的描述結(jié)果，這里暫時沒有考慮容錯機(jī)制。

MC = [1U1:Table1U2:Table1… Un:Table1N1:Table2N2:Table2…Nn:Table2, R1]

R1= RC2RC3RC4RC5RC6RC7RF

RC2= U1:Table1N1:Table2→ U1:Table1Create[21U1:Table1N1:Table2, R21] | … | Un:Table1Nn:Table2→ Un:Table1Create[2nUn:Table1Nn:Table2, R2n]

RC3= X1:Table3→Create[31X1:Table3, R31] | … | Xn:Table3→Create[3nXn:Table3, R3n]

RC4= D11:Table4→Create[411D11:Table4, R411] | … | D14:Table4→Create[414D14:Table4, R414]

| … |

Dn1:Table4→Create[4n1Dn1:Table4, R4n1] | … | Dn4:Table4→Create[4n4Dn4:Table4, R4n4]

RC5= M11:Table5→Create[511M11:Table5, R511] | … | M14:Table5→Create[514M14:Table5, R514]

| … |

Mn1:Table5→Create[5n1Mn1:Table5, R5n1] | … | Mn4:Table5→Create[5n4Mn4:Table5, R5n4]

RC6= U1:Table1S11:Table6S12:Table6S13:Table6S14:Table6→Create[61U1:Table1S11:Table6S12:Table6S13:Table6S14:Table6, R61]

| … |

Un:Table1Sn1:Table6Sn2:Table6Sn3:Table6Sn4:Table6→Create[6nUn:Table1Sn1:Table6Sn2:Table6Sn3:Table6Sn4:Table6, R6n]

RC7= Y1:Table7Y2:Table7… Yn:Table7→Create[7Y1:Table7Y2:Table7…Yn:Table7, R7]

RF= OH:Table8→Finish:State

R21= RP21RE

…

R2n= RP2nRE

RP21= U1:Table1N1:Table2→ X1:Table3END:State

…

RP2n= Un:Table1Nn:Table2→ Xn:Table3END:State

RE=END:State→ δ

R31= RP31RE

…

R3n= RP3nRE

RP31= X1:Table3→ D11:Table4D12:Table4D13:Table4D14:Table4END:State

…

RP3n= Xn:Table3→ Dn1:Table4Dn2:Table4Dn3:Table4Dn4:Table4END:State

R411= RP411RE

…

R414= RP414RE

…

R4n1= RP4n1RE

…

R4n4= RP4n4RE

RP411= D11:Table4→ M11:Table5END:State

…

RP414= D14:Table4→ M14:Table5END:State

…

RP4n1= Dn1:Table4→ Mn1:Table5END:State

…

RP4n4= Dn4:Table4 → Mn4:Table5END:State

R511= RP511RE

…

R514= RP514RE

…

R5n1= RP5n1RE

…

R5n4= RP5n4RE

RP511= M11:Table5→ S11:Table6END:State

…

RP514= M14:Table5→ S14:Table6END:State

…

RP5n1= Mn1:Table5→ Sn1:Table6END:State

…

RP5n4= Mn4:Table5→ Sn4:Table6END:State

R61= RP61RE

…

R6n= RP6nRE

RP61= U1:Table1S11:Table6S12:Table6S13:Table6S14:Table6→ Y1:Table7END:State

…

RP6n= Un:Table1Sn1:Table6Sn2:Table6Sn3:Table6Sn4:Table6→ Yn:Table7END:State

R7= RP7RE

RP7= Y1:Table7Y2:Table7…Yn:Table7→ H:Table8END:State

圖6 實(shí)例聯(lián)系圖Fig.6 The communication graph of the instance

為了便于描述，本文用一個名稱來表示多個元素。如：R2表示規(guī)則R中下標(biāo)以2開頭的所有規(guī)則，包括R21,…,R2n。D表示D11,D12,…,Dn4的總稱，共4n個元素。

描述結(jié)果可以看出：

1)初始細(xì)胞膜里只有類型為Table1的對象U1,…,Un和類型為Table2的對象N1,…,Nn，經(jīng)過反應(yīng)規(guī)則R1中的規(guī)則RC2后，產(chǎn)生n個子細(xì)胞膜，且每個子細(xì)胞膜中都包含一個Table1類型的對象和一個Table2類型的對象，兩個對象的編號一樣，其中產(chǎn)生子細(xì)胞膜的同時也會產(chǎn)生對象U1,…,Un，即對象U1,…,Un產(chǎn)生反應(yīng)后并不會消失。之后這些子細(xì)胞膜中的兩個對象會進(jìn)行反應(yīng)，產(chǎn)生一個Table3類型的對象以及一個表示結(jié)束狀態(tài)的對象End，對象End按照規(guī)則R2中的規(guī)則RE進(jìn)行反應(yīng)，此時子細(xì)胞膜溶解，Table3類型的對象留在父細(xì)胞膜中。

2)接下來Table3類型的對象按照規(guī)則R1中的RC3進(jìn)行反應(yīng)，生成n個子細(xì)胞膜，每個細(xì)胞膜中包含一個Table3類型的對象，相當(dāng)于創(chuàng)建細(xì)胞膜的同時對象進(jìn)入了子細(xì)胞膜中。在子細(xì)胞膜中，Table3類型的對象按照規(guī)則R3中的規(guī)則RP3進(jìn)行反應(yīng)，生成四個Table4類型的對象以及一個表示結(jié)束狀態(tài)的對象End，對象End按照規(guī)則RE進(jìn)行反應(yīng)后導(dǎo)致子細(xì)胞膜的溶解。

3)接下來每個Table4類型的對象按照規(guī)則R1中的規(guī)則RC4進(jìn)行反應(yīng)，生成4n個子細(xì)胞膜，同時每個對象也進(jìn)入到子細(xì)胞膜中。然后子細(xì)胞膜中的對象按照R4中的RP4進(jìn)行反應(yīng)生成Table5類型的對象M以及表示結(jié)束狀態(tài)的對象End，End對象按照規(guī)則RE反應(yīng)后導(dǎo)致細(xì)胞膜的溶解。

4)溶解后進(jìn)入到父細(xì)胞膜的對象M按照規(guī)則RC5進(jìn)行反應(yīng)，每個對象生成一個子細(xì)胞膜，每個子細(xì)胞膜中包含一個Table5類型的對象。在子細(xì)胞膜中，Table5類型的對象按照規(guī)則R5中的規(guī)則RP5進(jìn)行反應(yīng)，生成一個Table6類型的對象以及對象End，然后End對象按照RE進(jìn)行反應(yīng)導(dǎo)致子細(xì)胞膜的溶解。

5)接下來每四個Table6類型的對象和一個Table1類型的對象按照規(guī)則RC6進(jìn)行反應(yīng)生成一個子細(xì)胞膜，同時子細(xì)胞膜也包含這四個對象。在子細(xì)胞膜中，四個Table6類型的對象和一個Table1類型的對象按照規(guī)則R6中的規(guī)則RP6進(jìn)行反應(yīng)，生成一個Table7類型的對象以及對象End，然后對象End按照規(guī)則RE進(jìn)行反應(yīng)導(dǎo)致子細(xì)胞膜的溶解。

6)這些Table7類型的對象進(jìn)入到父細(xì)胞膜后，按照規(guī)則RC7進(jìn)行反應(yīng)生成一個子細(xì)胞膜，該子細(xì)胞膜中包含n個Table7類型的對象，這n個對象按照規(guī)則R7中的規(guī)則RP7進(jìn)行反應(yīng)生成一個Table8類型的對象以及一個對象End，End對象按照R8進(jìn)行反應(yīng)導(dǎo)致子細(xì)胞膜溶解。

7)最后H對象按照規(guī)則RF進(jìn)行反應(yīng)，生成表示整個過程結(jié)束的對象Finish。

圖7描述了細(xì)胞膜變化過程的一部分，第一部分為初始細(xì)胞膜，經(jīng)過R1中的規(guī)則反應(yīng)后變?yōu)榈诙糠?，此時生成了n個子細(xì)胞膜，在子細(xì)胞膜內(nèi)按照R2中的規(guī)則反應(yīng)后變?yōu)榈谌糠?，生成對象X以及End，接下來End導(dǎo)致細(xì)胞膜溶解，變?yōu)榈谒牟糠郑瑢ο筮z留到父細(xì)胞膜中。

圖7 無容錯機(jī)制的實(shí)例細(xì)胞膜變化圖Fig.7 The changes of membrane without fault tolerance

該例中具有相同類型的對象表示實(shí)際處理中的數(shù)據(jù)具有相同的類型，比較特殊的是對象End和Finish均表示一種狀態(tài)，End表示當(dāng)前結(jié)點(diǎn)已經(jīng)處理完成，F(xiàn)inish表示整個系統(tǒng)處理已經(jīng)結(jié)束。

對于該實(shí)例考慮容錯機(jī)制的情況，只需要在每次生成的子細(xì)胞膜中增加兩條規(guī)則，一條規(guī)則用于生成錯誤狀態(tài)F同時保留原對象，另一條規(guī)則為錯誤狀態(tài)F導(dǎo)致細(xì)胞膜溶解。

例如在圖7中的細(xì)胞膜21中，可以增加兩條規(guī)則后變?yōu)?/p>

R21= U1:Table1N1:Table2→ X1:Table3END:State

| U1:Table1N1:Table2→ N1:Table2F:State

| F:State→ δ

這里由于子細(xì)胞膜的父細(xì)胞膜中已經(jīng)有對象U1，因此生成錯誤狀態(tài)時不需要生成對象U1:Table1。

在所有子細(xì)胞膜中增加這兩條規(guī)則后，如圖8所示，在細(xì)胞膜21中當(dāng)對象按照反應(yīng)規(guī)則生成錯誤狀態(tài)時，生成的錯誤狀態(tài)會導(dǎo)致細(xì)胞膜的溶解，對象N1:Table2重新回到父細(xì)胞膜中，之后重新生成細(xì)胞膜21，表示任務(wù)重新執(zhí)行一遍。

圖8 加入容錯機(jī)制的實(shí)例細(xì)胞膜變化圖Fig.8 The changes of membrane with fault tolerance

5 結(jié)束語

本文利用細(xì)胞膜演算對Dryad編程模型進(jìn)行了形式化描述。通過實(shí)例可以驗(yàn)證：本文的形式化描述方法能清晰地表達(dá)Dryad編程模型的執(zhí)行過程，且描述了Dryad編程模型的容錯機(jī)制。本文提供了一種嚴(yán)格的、準(zhǔn)確的Dryad編程模型形式化方法，豐富了Dryad編程模型的理論體系，為編程模型提供了任務(wù)調(diào)度的優(yōu)化依據(jù)，同時其描述結(jié)果可以作為驗(yàn)證程序正確性的輔助工具。

[1]陳康, 鄭緯民. 云計(jì)算: 系統(tǒng)實(shí)例與研究現(xiàn)狀[J]. 軟件學(xué)報, 2009, 20(5): 1337-1348. CHEN Kang, ZHENG Weimin. Cloud computing: system instances and current research[J]. Journal of software, 2009, 20(5): 1337-1348.

[2]林子雨, 賴永炫, 林琛, 等. 云數(shù)據(jù)庫研究[J]. 軟件學(xué)報, 2012, 23(5): 1148-1166. LIN Ziyu, LAI Yongxuan, LIN Chen, et al. Research on cloud databases[J]. Journal of software, 2012, 23(5): 1148-1166.

[3]DEAN J, GHEMAWAT S. MapReduce: simplified data processing on large clusters[J]. Communications of the ACM, 2008, 51(1): 107-113.

[4]BHANDARKAR M. MapReduce programming with apache Hadoop[C]//Proceedings of the IEEE International Symposium on Parallel & Distributed Processing. Atlanta, GA, USA: IEEE, 2010.

[5]WANG Lizhe, TAO Jie, RANJAN R, et al. G-Hadoop: mapReduce across distributed data centers for data-intensive computing[J]. Future generation computer systems, 2013, 29(3): 739-750.

[6]LEVERICH J, KOZYRAKIS C. On the energy (in) efficiency of hadoop clusters[J]. ACM SIGOPS operating systems review, 2010, 44(1): 61-65.

[7]ISARD M, BUDIU M, YU Yuan, et al. Dryad: distributed data-parallel programs from sequential building blocks[C]//Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems. Lisbon, Portugal: ACM, 2007: 59-72.

[8]YU Yuan, ISARD M, FETTERLY D, et al. DryadLINQ: a system for general-purpose distributed data-parallel computing using a high-level language[C]//Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. San Diego, California, USA: ACM, 2008: 1-14.

[10]LIU Lei, LIU Dongqing, LYU Shuai, et al. An abstract description method of map-reduce-merge using haskell[J]. Mathematical problems in engineering, 2013, 2013: 147593.

[11]QI Zhengwei, LI Minglu, FU Cheng, et al. Membrane calculus: a formal method for Grid transactions[J]. Concurrency and computation: practice and experience, 2006, 18(14): 1799-1809.

[12]戚正偉, 尤晉元. 基于細(xì)胞膜演算的Web服務(wù)事務(wù)處理形式化描述與驗(yàn)證[J]. 計(jì)算機(jī)學(xué)報, 2006, 29(7): 1137-1144. QI Zhengwei, YOU Jinyuan. The formal specification and verification of transaction processing in Web services by membrane calculus[J]. Chinese journal of computers, 2006, 29(7): 1137-1144.

Formal description of Dryad based on membrane calculus

LIU Lei1, LIU Feng1, REN Junqi1, LYU Shuai1,2

(1. College of Computer Science and Technology, Jilin University, Changchun 130012, China; 2. College of Mathematics, Jilin University, Changchun 130012, China)

Because the dryad programming model is not an open-source model, conducting research on this model is relatively scarce. This study provides an accurate and explicit formal description for the task performance of the dryad programming model by utilizing the advantages of membrane calculus on the aspect of describing the concurrent system. This research also describes the fault-tolerant mechanism of the model. Accordingly, a real case is used to test the formalized description results. The formalized description method herein effectively enriches the theoretical system of the programming model. The method also provides a basis for the task scheduling optimization. Simultaneously, the method can be used as an auxiliary tool to verify the program correctness.

cloud computing; programming model; Dryad; cytomembrane calculation; formalization; directed acyclic graph(DAG)

2015-09-26.

日期：2016-05-27.

國家自然科學(xué)基金項(xiàng)目(61300049，61402195，61502197)；吉林省科技發(fā)展計(jì)劃項(xiàng)目(20130206052GX，20140520069JH).

劉磊(1960-), 男, 教授, 博士生導(dǎo)師； 呂帥(1981-), 男, 副教授, 博士.

呂帥，E-mail: lus@jlu.edu.cn.

10.11990/jheu.201509081

TP301

TP301A

1006-7043(2016) 11-1539-07

劉磊，劉豐，任俊綺，等. 基于細(xì)胞膜演算的Dryad形式化描述[J]. 哈爾濱工程大學(xué)學(xué)報, 2016, 37(11): 1539-1545. LIU Lei, LIU Feng, REN Junqi, et al. Formal description of Dryad based on membrane calculus[J]. Journal of Harbin Engineering University, 2016, 37(11): 1539-1545.

網(wǎng)絡(luò)出版地址：http://www.cnki.net/kcms/detail/23.1390.u.20160527.1354.010.html