Dynamic Management Protocol for Cloud Applications

Organisation:	Grenoble INP (FRANCE) University Joseph Fourier, Grenoble (FRANCE) Inria Grenoble - Rhône-Alpes / CONVECS project-team (FRANCE)
Method:	LNT CADP (Construction and Analysis of Distributed Processes)
Domain:	Cloud Computing
Period:	2013
Size:	2200 lines of LNT 600 reconfiguration scenarios 35 temporal logic properties
Description:	Cloud computing is a new programming paradigm that emerged a few years ago, which aims at delivering resources and software applications over a network (such as the Internet). Cloud computing leverages hosting platforms based on virtualization and promotes a new software licensing and billing model based on the pay-per-use concept. Cloud applications are inherently distributed and run on different virtual machines (VMs). Therefore, to deploy their applications, cloud users need first to instantiate several virtual machines. Moreover, during the application life time, various management operations may be required, such as instantiating new VMs, replicating some of them for load balancing purposes, destroying or replacing VMs, etc. We propose a novel protocol for (re)configuring distributed applications in cloud environments. These applications consist of interconnected software components hosted on several VMs. A deployment manager guides the reconfiguration tasks by instantiating new VMs or destroying existing ones. After instantiation, each VM tries to satisfy its required services (ports) by binding its components to other components providing these services. When a VM receives a destruction request from the deployment manager, that VM unbinds and stops its components. In order to (un)bind/start/stop components, VMs communicate together through a publish/subscribe communication media. Designing such protocols is a complicated task because they involve a high degree of parallelism, making it very difficult to anticipate all execution scenarios. Therefore, we followed a rigorous design process, based on formal methods and verification, to ensure that the protocol satisfies certain key properties. We specified the protocol in LNT, as well as over 600 hand-crafted examples (application model and reconfiguration scenario). We also identified 35 temporal properties that the protocol must respect during its execution, and specified them in MCL. For each example, we generated the Labelled Transition System (LTS) model from the LNT specification and verified all the MCL properties on it using the EVALUATOR model checker of the CADP toolbox.
Conclusions:	The use of verification techniques helped us to improve the protocol. For instance, in an initial version of the protocol, the component start-up/shutdown was guided by a centralised deployment manager. We observed an explosion in terms of states/transitions in the corresponding LTSs, even for simple examples involving few VMs. This was due to an overhead of messages transmitted to and from the deployment manager, which was supposed to keep track of all modifications in each VM to possibly start/stop components. To avoid this problem, we proposed a decentralised version of the protocol, where each VM is in charge of starting and stopping its own components. We also detected a major bug in the VM destruction process. Originally, when it was required to stop a component, it was stopped before the components bound to it. This typically violates some architectural invariants (e.g., a started component cannot be connected to a stopped component) and impedes the robustness level expected from the protocol. We corrected this issue by stopping properly components, which required a deep revision of the protocol. Thus, in the current version of the protocol, when a component must be stopped, it requests to all the components connected to it to unbind and once it is done, it can finally stop.
Publications:	[Abid-Salaun-Bongiovanni-dePalma-13] R. Abid, G. Salaün, F. Bongiovanni, and N. De Palma. Verification of a Dynamic Management Protocol for Cloud Applications. Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis ATVA'2013 (Hanoi, Vietnam), October 2013. Available on-line at: http://hal.inria.fr/hal-00863262/en or from the CADP Web site in PDF and PostScript [Abid-Salaun-dePalma-15] R. Abid, G. Salaün, and N. de Palma. "Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications". Science of Computer Programming, 117:1-16, 2016. Available on-line at: http://hal.inria.fr/hal-01246152/en or from the CADP Web site in PDF and PostScript
Contact:	Gwen Salaün Inria and LIG - CONVECS project-team 655, av. de l'Europe F-38330 Montbonnot Saint Martin France Tel: +33 (0)4 76 61 54 28 Fax: +33 (0)4 76 61 52 52 Email: gwen.salaun@inria.fr
Further remarks:	This case-study, amongst others, is described on the CADP Web Page site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page