|
|
|
|
|
Start date: as soon as possible
Type of contract: Fixed term contract (CDD) for 3 years.
Salary: About 1600 EUR net per month (1950 EUR gross), health insurance included (French Social Security system).
Location: This thesis project will be carried out at the INRIA Montbonnot site, about 10 kilometres from Grenoble.
Subject: « Parallel code generation in the cloud »
Objectives:
« Cloud computing », or « cloud » for short, consists in the delivery of resources and applications to computers and other devices as services through a network, by leveraging hosting platforms based on virtualization. As such, cloud computing applications involve a high degree of asynchronous concurrency. The INRIA/VASY project-team develops software tools and techniques based on formal methods for the design and verification of asynchronous concurrent systems, which are packaged in the internationally renowned CADP (Construction and Analysis of Distributed Processes) software toolbox. We advocate the use of CADP to develop, model and verify applications in the cloud.
More specifically, VASY has created and developed recently the LNT formal modeling language, which incorporates most constructs stemming from classical programming languages, thus easing its acceptance by industry engineers. LNT is derived from the ISO standard E-LOTOS (2001), of which it represents the first successful implementation based on a source-level translation from LNT to LOTOS, a former ISO standard (1989). LNT enjoyed unanimous support from all industrial partners (Bull, CEA/Leti, STMicroelectronics) who had the opportunity to use it for real-size designs.
Having in mind the goal to promote the use of LNT for designing applications in the cloud, the subject of this thesis is to study parallel code generation for LNT. This code generator would translate the LNT specification of a concurrent system into a set of concurrent threads or processes. An interesting research issue will be to map the powerful n-party rendezvous mechanism of LNT onto lower-level synchronization and communication paradigms, such as shared variables and locks or message-passing primitives. When available, this parallel code generator could enable LNT as a programming language for cloud applications, with the key benefit that LNT would be also equipped with formal verification tools provided by the CADP toolbox. To the best of our knowledge, this would make CADP the first tool chain for asynchronous systems enabling a formally verified design to be implemented automatically.
This thesis will be realised in synergy with the CloudForce project (funded by the French national program « Investissements d'Avenir - Développement de l'Economie Numérique »), which aims at providing an open software engineering platform for the collaborative development, the deployment, and the administration of cloud applications. CloudForce gathers 18 academic and industrial partners, among which Bull, INRIA, IRIT, France Telecom, LIG, Télécom Paris Tech, and Thalès.
Work proposed and expected results:
Initially, the candidate will complete an in-depth study of existing techniques and tools for (sequential and/or parallel) code generation. The candidate will also study the CADP toolbox, the LNT language, and the sequential code generator for the LNT language that already exists in CADP.
The candidate will then build on the sequential code generator to design a parallel code generator for a subset of LNT consisting in sequential LNT processes running concurrently. This will require the design of a communication library that implements protocols to achieve LNT parallel composition. Particular attention will be paid to the conformance of the generated code to LNT formal semantics. Formal modeling of the communication library in LNT itself might be a way to prove this conformance using the CADP toolbox.
The candidate will then propose extensions of the code generator to the full LNT language, including in particular concurrent process activation (spawning concurrent processes within a running process), termination (continuing the running process once the spawned concurrent processes have terminated), and disruption.
All along the thesis, the candidate will validate its ideas on realistic cloud applications that will be provided by the partners in the framework of CloudForce.
Required skills and profile:
Contacts:
All questions concerning this thesis project should be addressed to:
 |
M. Frédéric Lang INRIA Rhône-Alpes /VASY Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 55 11 E-mail : Frederic.Lang@inria.fr |
Application content:
Application submission:
Applications should be addressed directly to Frédéric Lang, preferably by email, mentioning the position number #2011C. Applications received after February 29th, 2012 might not be considered if a candidate has been selected already.