基于細胞膜演算的Dryad形式化描述

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

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

?

基于細胞膜演算的Dryad形式化描述

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

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

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

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

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

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

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

Dryad編程模型的執(zhí)行過程基于DAG，具有較好的通用性，但Dryad編程模型的不開源導致其理論研究相對較少?；诩毎ぱ菟阍诿枋鰟討B(tài)、移動的并發(fā)系統(tǒng)的獨特優(yōu)勢，本文利用其對Dryad編程模型的執(zhí)行流程進行嚴格的形式化描述。

1 基礎知識

1.1 細胞膜演算

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

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

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

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

1.2 Dryad編程模型

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

2 形式化描述

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

針對一個特定的DAG，將執(zhí)行相同任務的結點劃分為同層，并且同層結點一般是并行執(zhí)行的。將當前正在執(zhí)行的同層結點認定為當前層，將當前層結點指向的結點認定為下一層。本文將DAG中相鄰層之間的關系分為4種，進行形式化描述。

2.1 相鄰層結點為一一對應關系(o2o規(guī)則)

假設當前層有n個結點，下一層也為n個結點，當前層的每一個結點都有一條邊指向下一層的結點，且分別指向不同的結點，則稱當前層與下一層為一一對應關系，如圖1所示。

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

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

?

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

圖1 一對一對應關系Fig.1 One-to-one correspondence

2.2 相鄰層結點之間為一對多對應關系(o2m規(guī)則)

假設當前層有1個結點，下一層有n個結點，當前層結點有n條邊分別指向下一層的每個結點，則稱當前層與下一層為一對多關系，如圖2所示。

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

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

?

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

圖2 一對多對應關系Fig.2 One-to-multiple correspondence

2.3 相鄰層結點之間為多對一對應關系(m2o規(guī)則)

假設當前層有n個結點，下一層有1個結點，且任意一個當前層結點都有且僅有一條邊指向下一層的結點，稱當前層與下一層為多對一關系，如圖3所示。

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

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

圖3 多對一對應關系Fig.3 Multiple-to-one correspondence

2.4 相鄰層結點之間為多對多對應關系(m2m規(guī)則)

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

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

?

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

圖4 多對多對應關系Fig.4 Multiple-to-multiple correspondence

2.5 復雜圖的形式化

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

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

圖5 復合關系Fig.5 Composite correspondence

2.6 容錯機制

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

| O1O2…Om→ O1O2…OmFault:State

RF:Fault:State→δ

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

3 描述算法

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

算法Dryadformalization

輸入：DAG

輸出：當前層結點集，下一層結點集，描述規(guī)則

1)whileDAG非空do

2)nodeset=DAG中所有出度為0的結點

3) 將nodeset進行劃分，將具有相同輸入邊的結點劃分到同一個集合Next_i，并將Next_i的輸入結點放到集合Pre_i

4) 從DAG中刪掉Next_i中的每一個結點和指向這些結點的每一條邊

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

4 實例驗證

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

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

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 實例聯(lián)系圖Fig.6 The communication graph of the instance

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

描述結果可以看出：

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

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

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

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

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

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

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

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

圖7 無容錯機制的實例細胞膜變化圖Fig.7 The changes of membrane without fault tolerance

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

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

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

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

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

| F:State→ δ

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

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

圖8 加入容錯機制的實例細胞膜變化圖Fig.8 The changes of membrane with fault tolerance

5 結束語

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

[1]陳康, 鄭緯民. 云計算: 系統(tǒng)實例與研究現(xiàn)狀[J]. 軟件學報, 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]. 軟件學報, 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]戚正偉, 尤晉元. 基于細胞膜演算的Web服務事務處理形式化描述與驗證[J]. 計算機學報, 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.

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

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

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

10.11990/jheu.201509081

TP301

TP301A

1006-7043(2016) 11-1539-07

劉磊，劉豐，任俊綺，等. 基于細胞膜演算的Dryad形式化描述[J]. 哈爾濱工程大學學報, 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)絡出版地址：http://www.cnki.net/kcms/detail/23.1390.u.20160527.1354.010.html