A Formal Description Method Of Dryad Using Membrane Calculus

In recent years,with the rapid development of computing,communication and storage technology,there has been a new business computing model-cloud computing.As an emerging computing model,cloud computing has played an important role in the field of scientific computing and business computing,and has been widely concerned by the current academia and industry.Programming model is an important aspect in the study of cloud computing,and provides a very convenient condition to use the distributed system.Dryad is a cloud programming model based on directed acyclic graph proposed by Microsoft,which has strong flexibility and versatility.However,because of Dryad programming model is not open source and the theoretical research on Dryad is relatively lacking,the theoretical system of Dryad programming model is not sufficient.Using biological cell membrane model,cell membrane calculation can effectively describe the dynamic,mobile and concurrent systems.In this paper,we propose a formal description of Dryad based on cell membrane calculus.We describe the executing processes of Dryad programming model with the advantage of cell membrane model,and we describe the fault-tolerant mechanism of Dryad programming model.At the same time,this paper designs an algorithm for the partition of adjacent nodes and the selection of description rules.Besides,we use an example to test the results of formal description.The cell membrane calculus has a very strong ability to describe,and the objects in the cell membrane can react simultaneously,so it has a unique advantage in describing the parallel system.Cell membrane calculus is used as a tool to describe two aspects of the benefits:1)the dissolution and creation of cell membrane can clearly describe the implemention of the tasks in the system,which can enhance the understanding of the implementation of the Dryad programming model and help evaluate and analyze task scheduling of the programming model,so the formalization can be as a theoretical basis for the optimization of task scheduling;2)the type of the object in the cell membrane can be used as reference of data type in the actual execution,the type changes of object indirectly reflect the changes of data in execution,so the formalization results can be as a tool to verify the correctness of the program.The formal description method in this paper can effectively enrich the theoretical system of the programming model,and provide a basis for the optimization of task scheduling.At the same time,it can also be used as an auxiliary tool to verify the correctness of the program.