Thèse

INSTITUT POLYTECHNIQUE DE GRENOBLE oN attribué par la bibliothèque Thèse pour obtenir le grade de Docteur de l’Institut Polytechnique de Grenoble Spécialité : Informatique préparée à l’Institut National de Recherche en Informatique et en Automatique centre Grenoble-Rhône-Alpes, projet Pop-Art École Doctorale Mathématiques, Sciences et Technologies de l’Information, Informatique présentée et soutenue publiquement par Gwenaël Delaval erle 1 juillet 2008 Répartition modulaire de programmes synchrones Co-directeurs de thèse : Marc Pouzet Alain Girault Jury Denis Trystram INP Grenoble Président François Pottier Inria Rocquencourt Rapporteur Jean-Pierre Talpin Inria Rennes Rapporteur Marc Pouzet Université Paris-Sud Co-directeur de thèse Alain Girault Inria Rhône-Alpes Co-directeur de thèse Mamoun Filali Amine CNRS, IRIT, Toulouse Examinateur Luc Maranget Inria Rocquencourt Examinateur23 Résumé Nous nous intéressons à la conception sûre de systèmes répartis. Nous mon- trons qu’avec la complexité et l’intégration croissante des systèmes embarqués, la structure fonctionnelle du système peut entrer en conflit avec la structure de son architecture. L’approche traditionnelle de conception par raffinement de cette architecture compromet alors la modularité fonctionnelle du système. Nous proposons donc une méthode permettant de concevoir un système ré- parti défini comme un programme unique, dont la structure fonctionnelle est in- dépendante de l’architecture du système. Cette méthode est basée sur l’ajout de primitives de répartition à un langage flots de données synchrone. Ces primitives permettent d’une part de déclarer l’architecture sous la forme d’un graphe défi- nissant les ressources existantes et les liens de communication existant entre ces ressources, et d’autre part de spécifier par des annotations la localisation de cer- taines valeurs et calculs du programme. Nous définissons ensuite la sémantique formelle de ce langage étendu. Cette sémantique a pour but de rendre compte de manière formelle l’effet des annota- tions ajoutées par le programmeur.Un système de types àeffets permet ensuite de vérifier la cohérence de ces annotations. Ce système de types est muni d’un méca- nisme d’inférence, qui permet d’inférer, à partir des annotations du programmeur, la localisation des calculs non annotés. Nous définissons ensuite, à partir de ce système de types, une méthode de répartition automatique permettant d’obtenir, à partir d’un programmeannoté, un fragment de programme parressource de l’ar- chitecture. La correction du système de types avec la sémantique du langage est prouvée, ainsi que l’équivalence sémantique de l’exécution des fragments obtenus par la méthode de répartition automatique avec le programme initial. Cette méthode a été implémentée dans le compilateur du langage Lucid Syn- chrone, et testée sur un exemple de radio logicielle.45 Abstract We address the problem of safe design of distributed embedded systems. We showthatwiththeincreasingcomplexityandintegrationofembeddedsystems,the functionalstructureofthesystemcanconflictwiththestructureofitsarchitecture. Theusualapproachofdesignbyrefinementofthisarchitecturecanthenjeopardize the functional modularity of the system. We propose a method allowing the design of a distributed system as a unique program, which functional structure is independent of the system’s architecture. This method is based on the extension of a synchronous dataflow programming language with primitives for program distribution. These primitives allow on one hand to describe the architecture as a graph defining existing computing resources andcommunication links between them, andontheother handtospecify bymean of annotations the localization of some values and computations of the program. We define the formal semantics of this extended language. The purpose of this semantics is to provide to the programmer a formal meaning to the annotations added to his program. A type and effect system is provided to ensure, at com- pilation time, the consistency of these annotations. A type inference mechanism allowtheinference, fromtheannotationsoftheprogrammer, ofthenon-annotated values and computations. We finally define, from this type system, an automatic distributionmethod,allowingthecomputation,fromanannotatedprogram,ofone program fragment for each computing resource of the architecture. The soundness of the type system with respect to the semantics has been proven, as well as the semantical equivalence of the composition of the fragments obtained via the automatic distribution method with the initial program. This method has been implemented in the compiler of the Lucid Synchrone language, and experimented with an example of software-defined radio.67 Remerciements Je tiens à remercier tout d’abord Alain Girault et Marc Pouzet de m’avoir permis de réaliser cette thèse sous leur co-direction. Leur apport, humain et scien- tifique,danscetravail,estinestimable. Ilsm’onténormément appris,etjesouhaite qu’ils sachent que malgré toutes les difficultés rencontrées, c’est grâce à eux, à leur patience, leurs encouragements, que cette thèse a pu être menée à bon terme. Jeremercielesmembresdemonjury,etparticulièrementmesdeuxrapporteurs, François Pottier et Jean-Pierre Talpin. J’ai eu la chance d’avoir eu des échanges très constructifs avec eux, je les remercient donc pour leur disponibilité. Ils m’ont permisd’améliorersignificativement cemémoire.JeremercieaussiDenisTrystram d’avoir accepté de présider ce jury, et Mamoun Filali-Amine et Luc Maranget d’y avoir été examinateurs. J’ai poursuivi, pendant ces quatre années, ma collaboration avec Éric Rutten, commencée à l’occasion de mon stage de master. Je le remercie chaleureusement pour cette collaboration, et pour la distance et l’ouverture d’esprit qu’il sait ap- porter en toute circonstance. Je remercie aussi Laurent Mounier, Philippe Bizard, Anne Rasse, Guillaume Huard, Jean-Marc Vincent et Cyril Labbé de m’avoir intégré dans leur équipe d’enseignement. L’environnement de travail n’étant rien sans environnement humain, au sens large, je remercie vivement : Hamoudi, Louis, Élodie, Florence, Alexandre, Mouaiad et Gérald, avec qui j’ai partagé... plus que mes directeurs de thèse; leur soutien et leurs conseils amicaux ont été plus que décisifs... ... L’équipe Pop-Art : Pascal, Simplice, Gregor,Xavier, Daniel,Bertrand, Emil, Shara, ainsi que les membres et ex-membres de l’équipe Bipop, Roger et Soraya... ... L’équipe VerTeCs, pour son accueil et ses pauses-café-polémiques interminables : Hervé, Thierry, Jérémy, Camille, Tristan, Christophe, Nathalie, Hatem, Florimont, Patricia et Vlad... ...Laurent,AurélieetLalao,rencontrésàl’occasiondumonitorat... ...LespotesdeVilleneuve etdeMounier:Pauline,Florian, Pauline, Olivier, Véro... ... Toute ma famille pour son soutien sans faille... ... Ceux que j’aurais oublié... ... Anne, enfin, sans qui rien ne serait aujourd’hui possible.8Table des matières 1 Introduction 13 2 Problématique 17 2.1 Programmation de systèmes répartis . . . . . . . . . . . . . . . . . 17 2.2 Compilation modulaire . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3 Programmation synchrone . . . . . . . . . . . . . . . . . . . . . . . 19 2.3.1 Systèmes réactifs synchrones . . . . . . . . . . . . . . . . . . 19 2.3.2 Langages synchrones . . . . . . . . . . . . . . . . . . . . . . 22 2.3.3 Intégration langage et répartition . . . . . . . . . . . . . . . 24 2.3.4 Compilation, répartition et désynchronisation . . . . . . . . 25 2.3.5 Compilation modulaire de programmes synchrones . . . . . . 26 2.3.6 Ordre supérieur et reconfiguration dynamique . . . . . . . . 30 2.4 Lucid Synchrone . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.4.1 Présentation générale . . . . . . . . . . . . . . . . . . . . . . 31 2.4.2 Formalisation du langage . . . . . . . . . . . . . . . . . . . . 41 2.4.3 Sémantique comportementale . . . . . . . . . . . . . . . . . 43 2.5 La radio logicielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 2.6 État de l’art . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 2.6.1 Conception de systèmes répartis . . . . . . . . . . . . . . . . 50 2.6.2 Répartition de programmes synchrones . . . . . . . . . . . . 53 2.6.3 Systèmes de types pour la répartition de programmes . . . . 55 2.7 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3 Extension du langage pour la répartition 59 3.1 Rappel de la problématique . . . . . . . . . . . . . . . . . . . . . . 59 3.2 Architectures homogènes . . . . . . . . . . . . . . . . . . . . . . . . 60 3.3 Architectures hétérogènes . . . . . . . . . . . . . . . . . . . . . . . 61 3.4 Communications . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 910 TABLE DES MATIÈRES 4 Sémantique synchrone et localisation 65 4.1 Une sémantique pour le programmeur . . . . . . . . . . . . . . . . . 65 4.2 Localisation des valeurs . . . . . . . . . . . . . . . . . . . . . . . . . 66 4.3 Exécution répartie . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.4 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 4.5 Sémantique pour architectures hétérogènes . . . . . . . . . . . . . . 73 4.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5 Système de types pour la répartition 75 5.1 Justification et description . . . . . . . . . . . . . . . . . . . . . . . 75 5.2 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 5.2.1 Typage d’équations . . . . . . . . . . . . . . . . . . . . . . . 77 5.2.2 Typage des nœuds . . . . . . . . . . . . . . . . . . . . . . . 78 5.3 Formalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 5.4 Illustration. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.5 Adaptation pour architectures hétérogènes . . . . . . . . . . . . . . 87 5.6 Correct