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

刘磊，刘丰，任俊绮，吕帅,2

(1. 吉林大学 计算机科学与技术学院，吉林 长春 130012；2. 吉林大学 数学学院，吉林 长春 130012)



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

刘磊1，刘丰1，任俊绮1，吕帅1,2

(1. 吉林大学 计算机科学与技术学院，吉林 长春 130012；2. 吉林大学 数学学院，吉林 长春 130012)

由于Dryad编程模型的实现并不开源，导致关于Dryad编程模型的理论研究较为缺乏。本文利用细胞膜演算在描述并发系统的优势，对Dryad编程模型中任务执行过程进行了准确清晰的形式化描述，并对Dryad编程模型的容错机制进行了描述，最后通过一个实例检验了形式化描述结果。本文的形式化描述方法有效地丰富了编程模型的理论体系，为编程人员提供了任务调度的优化依据，同时该形式化描述还可作为验证程序正确性的辅助工具。

云计算；编程模型；Dryad；细胞膜演算；形式化；有向无环图

云计算是当今IT产业发展的主要趋势，它改变了传统的服务方式，为了能够低成本、高效率地处理海量数据，各大互联网公司都建立了自己的大型集群系统[1-2]。云计算的基础设施以商用机器集群为主，为利于编程人员的软件开发，提出了编程模型的概念。

MapReduce是Google于2004年提出的编程模型，通过将作业简化为Map和Reduce任务的处理，大大降低了并行编程难度[3]。Hadoop项目的开源实现使得MapReduce编程模型得到了更为快速的发展[4-6]。不同于MapReduce编程模型固定的两阶段处理方式，微软开发的通用执行引擎Dryad，通过将一个程序表示成一个有向无环图(directed acyclic graph，DAG)，能有效地分布式处理大规模数据，具有较强的扩展性[7]。相比MapReduce，Dryad编程模型能更加有效地处理连接运算、迭代运算等。Dryad由于采用了显式并行，并不适合直接用来解决实际问题，因此微软开发了高层次编程语言DryadLINQ[8]，降低了在大规模集群上开发人员的编程难度。

编程模型的形式化描述便于人们更为准确地理解编程模型，对其进行研究具有重要的意义。Lämmel提出了MapReduce的严格准确的形式化描述，以函数式编程语言Haskell为工具，明确了其中的类型变化[9]。通过使用Haskell语言对编程模型Map-Reduce-Merge进行了严格的描述，为进行支持连接运算的并行编程模型的后续研究提供了理论基础[10]。戚正伟等提出了一种新的事务处理形式化方法——细胞膜演算[11]，并利用细胞膜演算形式化描述了Web服务中原子事务协调协议[12]。细胞膜演算具有非常强大的描述能力，且其多个细胞膜里面的对象可以同时进行反应，因而其在描述并行系统方面具有独特的优势。

Dryad编程模型的执行过程基于DAG，具有较好的通用性，但Dryad编程模型的不开源导致其理论研究相对较少。基于细胞膜演算在描述动态、移动的并发系统的独特优势，本文利用其对Dryad编程模型的执行流程进行严格的形式化描述。

1 基础知识

1.1 细胞膜演算

细胞膜演算是P-systems相应的演算系统。令类型对象集为Σ，其元素为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是一个用于并行数据应用的分布式执行引擎，一个Dryad的整体结构由该任务的通信流决定，一个任务是一个DAG，其中顶点表示程序，边表示数据通道，通过运行时调度将该DAG自动地映射到物理资源。

2 形式化描述

DAG是Dryad编程模型的一个核心结构，编程模型的执行过程以及容错性等方面都基于该DAG。

针对一个特定的DAG，将执行相同任务的结点划分为同层，并且同层结点一般是并行执行的。将当前正在执行的同层结点认定为当前层，将当前层结点指向的结点认定为下一层。本文将DAG中相邻层之间的关系分为4种，进行形式化描述。

2.1 相邻层结点为一一对应关系(o2o规则)

假设当前层有n个结点，下一层也为n个结点，当前层的每一个结点都有一条边指向下一层的结点，且分别指向不同的结点，则称当前层与下一层为一一对应关系，如图1所示。

规则o2o的具体描述如下：当前层结点有n个细胞膜，各个细胞膜内反应后产生一个代表结束状态的对象End:State，该对象会触发细胞膜内的溶解规则，溶解后产生的对象为O1,…,On，每一个对象会触发父细胞的规则集R中的一条反应规则，产生一个新的细胞膜。规则集R如下

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

⋮

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

图1 一对一对应关系Fig.1 One-to-one correspondence

2.2 相邻层结点之间为一对多对应关系(o2m规则)

假设当前层有1个结点，下一层有n个结点，当前层结点有n条边分别指向下一层的每个结点，则称当前层与下一层为一对多关系，如图2所示。

规则o2m的具体描述如下：当前层有一个细胞膜，细胞膜内反应后产生对象End:State，该对象会触发细胞膜内的溶解规则，溶解后产生的对象为O1,…,On，每一个对象会触发父细胞的规则集R中的一条反应规则，产生一个新的细胞膜。规则集R如下

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

⋮

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

图2 一对多对应关系Fig.2 One-to-multiple correspondence

2.3 相邻层结点之间为多对一对应关系(m2o规则)

假设当前层有n个结点，下一层有1个结点，且任意一个当前层结点都有且仅有一条边指向下一层的结点，称当前层与下一层为多对一关系，如图3所示。

规则m2o的具体描述如下：当前层有n个细胞膜，细胞膜内反应后产生对象End:State，该对象触发细胞膜内的溶解规则，当前层每个细胞膜溶解后产生一个对象，溶解后产生的对象为O1,…,On，所有这些对象会触发规则集R中的反应规则，产生一个新的细胞膜。R中仅有1条规则：

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

图3 多对一对应关系Fig.3 Multiple-to-one correspondence

2.4 相邻层结点之间为多对多对应关系(m2m规则)

假设当前层有m个结点，下一层有n个结点，并且当前层每一个结点都有n条边分别指向下一层的每一个结点，称当前层与下一层为多对多关系，如图4所示。规则m2m的具体描述如下：当前层有m个细胞膜，细胞膜内反应后产生对象End:State，该对象触发细胞膜内的溶解规则，每个细胞膜溶解后产生n个对象，共有m×n个对象。对于第i个(i= 1,…,m)细胞膜，溶解后产生的对象为Oi1,Oi2,…,Oin。m个对象会触发规则集R的一条反应规则，产生一个新的细胞膜。R中有n条规则，如下

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中一些复杂情况都可以通过上述规则进行形式化描述。

图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各分为一层。根据输入源结点的不同对B进行划分，可以得到三个集合为{B1}、{B2,B3}、{B4}。B1的输入为A1和C，可将A1和C看作当前层，B1看作下一层，应用规则m2o来表示从A1和C到B1的执行过程。同理，B4的输入为A4和C，应用规则m2o来表示从A4和C到B4的执行过程。B2和B3的输入都来自于C，可将C看作当前层，B2和B3看作下一层，应用规则o2m来表示从C到B2和B3的执行过程。C的输入为A1、A2、A3和A4，可将A1、A2、A3和A4看作当前层，C看作下一层，应用规则m2o来表示从A1、A2、A3和A4到C的执行过程。

图5 复合关系Fig.5 Composite correspondence

2.6 容错机制

对于Dryad编程模型，容错处理采用的方式是对该结点所分配的任务重新进行分配。本文描述容错机制的方式是令对象参加反应后得到的结果有两种情况，即对象按照规则反应之后得到的结果是不确定的，一种情况为正常处理的结果，另一种情况为结点失效时的情况。规则如下

| O1O2…Om→ O1O2…OmFault:State

RF:Fault:State→δ

这里用对象Fault表示错误状态。从规则R中可以看出，当出错时，不仅得到了错误状态，同时原来的对象也得到了保留，这是因为结点失效时重新分配的任务需要再次使用该节点处理的数据。而后，错误状态导致细胞膜的溶解，所有对象重新回到父细胞膜中，重新按照规则生成子细胞膜，从而表示任务的重新分配。如果父细胞膜中已经存在某些对象，则生成错误状态时不需要生成这些对象。

3 描述算法

Dryad的描述算法Dryadformalization的整体思路为：首先找出出度为0的结点，然后将具有相同输入的结点划分为同一集合Next。若Next中只有一个元素，且该集合的输入结点集Pre只有一个元素，则利用规则o2o；若Pre有多个元素，则利用规则m2o。若Next中有多个元素，且该集合的输入结点集Pre只有一个元素，则利用规则o2m；若Pre有多个元素，则利用规则m2m。

算法Dryadformalization

输入：DAG

输出：当前层结点集，下一层结点集，描述规则

1)whileDAG非空do

2)nodeset=DAG中所有出度为0的结点

3) 将nodeset进行划分，将具有相同输入边的结点划分到同一个集合Next_i，并将Next_i的输入结点放到集合Pre_i

4) 从DAG中删掉Next_i中的每一个结点和指向这些结点的每一条边

5)fori ←1to划分得到的集合数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) 用规则rule描述Pre_temp到Next_temp的执行过程

给出Dryadformalization算法的完备性证明过程。

对于任意一个连通的DAG，一定存在出度为0的结点，否则该DAG必然存在环，每执行一次循环(第1～15行)，将删去所有出度为0的结点以及所有指向这些结点的边。由于算法每次循环都会删除一些结点，最终一定使得结点全部删除完毕，此时第一个循环结束。栈中存储了DAG的分层结果，以及对应的描述规则。第二个循环(第16～18行)每次在栈中弹出一个元素，由于栈中元素的个数等同于第一个循环执行的次数，因此栈中元素有限，所以第二个循环也一定会结束，因此对于任意给定的一个连通的DAG，Dryadformalization算法一定会终止，因此本文的描述方法是完备的。

4 实例验证

本文针对文献[7]中的数据库查询实例进行实例描述。该实例所对应的联系图如图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 实例联系图Fig.6 The communication graph of the instance

为了便于描述，本文用一个名称来表示多个元素。如：R2表示规则R中下标以2开头的所有规则，包括R21,…,R2n。D表示D11,D12,…,Dn4的总称，共4n个元素。

描述结果可以看出：

1)初始细胞膜里只有类型为Table1的对象U1,…,Un和类型为Table2的对象N1,…,Nn，经过反应规则R1中的规则RC2后，产生n个子细胞膜，且每个子细胞膜中都包含一个Table1类型的对象和一个Table2类型的对象，两个对象的编号一样，其中产生子细胞膜的同时也会产生对象U1,…,Un，即对象U1,…,Un产生反应后并不会消失。之后这些子细胞膜中的两个对象会进行反应，产生一个Table3类型的对象以及一个表示结束状态的对象End，对象End按照规则R2中的规则RE进行反应，此时子细胞膜溶解，Table3类型的对象留在父细胞膜中。

2)接下来Table3类型的对象按照规则R1中的RC3进行反应，生成n个子细胞膜，每个细胞膜中包含一个Table3类型的对象，相当于创建细胞膜的同时对象进入了子细胞膜中。在子细胞膜中，Table3类型的对象按照规则R3中的规则RP3进行反应，生成四个Table4类型的对象以及一个表示结束状态的对象End，对象End按照规则RE进行反应后导致子细胞膜的溶解。

3)接下来每个Table4类型的对象按照规则R1中的规则RC4进行反应，生成4n个子细胞膜，同时每个对象也进入到子细胞膜中。然后子细胞膜中的对象按照R4中的RP4进行反应生成Table5类型的对象M以及表示结束状态的对象End，End对象按照规则RE反应后导致细胞膜的溶解。

4)溶解后进入到父细胞膜的对象M按照规则RC5进行反应，每个对象生成一个子细胞膜，每个子细胞膜中包含一个Table5类型的对象。在子细胞膜中，Table5类型的对象按照规则R5中的规则RP5进行反应，生成一个Table6类型的对象以及对象End，然后End对象按照RE进行反应导致子细胞膜的溶解。

5)接下来每四个Table6类型的对象和一个Table1类型的对象按照规则RC6进行反应生成一个子细胞膜，同时子细胞膜也包含这四个对象。在子细胞膜中，四个Table6类型的对象和一个Table1类型的对象按照规则R6中的规则RP6进行反应，生成一个Table7类型的对象以及对象End，然后对象End按照规则RE进行反应导致子细胞膜的溶解。

6)这些Table7类型的对象进入到父细胞膜后，按照规则RC7进行反应生成一个子细胞膜，该子细胞膜中包含n个Table7类型的对象，这n个对象按照规则R7中的规则RP7进行反应生成一个Table8类型的对象以及一个对象End，End对象按照R8进行反应导致子细胞膜溶解。

7)最后H对象按照规则RF进行反应，生成表示整个过程结束的对象Finish。

图7描述了细胞膜变化过程的一部分，第一部分为初始细胞膜，经过R1中的规则反应后变为第二部分，此时生成了n个子细胞膜，在子细胞膜内按照R2中的规则反应后变为第三部分，生成对象X以及End，接下来End导致细胞膜溶解，变为第四部分，对象遗留到父细胞膜中。

图7 无容错机制的实例细胞膜变化图Fig.7 The changes of membrane without fault tolerance

该例中具有相同类型的对象表示实际处理中的数据具有相同的类型，比较特殊的是对象End和Finish均表示一种状态，End表示当前结点已经处理完成，Finish表示整个系统处理已经结束。

对于该实例考虑容错机制的情况，只需要在每次生成的子细胞膜中增加两条规则，一条规则用于生成错误状态F同时保留原对象，另一条规则为错误状态F导致细胞膜溶解。

例如在图7中的细胞膜21中，可以增加两条规则后变为

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

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

| F:State→ δ

这里由于子细胞膜的父细胞膜中已经有对象U1，因此生成错误状态时不需要生成对象U1:Table1。

在所有子细胞膜中增加这两条规则后，如图8所示，在细胞膜21中当对象按照反应规则生成错误状态时，生成的错误状态会导致细胞膜的溶解，对象N1:Table2重新回到父细胞膜中，之后重新生成细胞膜21，表示任务重新执行一遍。

图8 加入容错机制的实例细胞膜变化图Fig.8 The changes of membrane with fault tolerance

5 结束语

本文利用细胞膜演算对Dryad编程模型进行了形式化描述。通过实例可以验证：本文的形式化描述方法能清晰地表达Dryad编程模型的执行过程，且描述了Dryad编程模型的容错机制。本文提供了一种严格的、准确的Dryad编程模型形式化方法，丰富了Dryad编程模型的理论体系，为编程模型提供了任务调度的优化依据，同时其描述结果可以作为验证程序正确性的辅助工具。

[1]陈康, 郑纬民. 云计算: 系统实例与研究现状[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]林子雨, 赖永炫, 林琛, 等. 云数据库研究[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)；吉林省科技发展计划项目(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.

网络出版地址：http://www.cnki.net/kcms/detail/23.1390.u.20160527.1354.010.html