Search

International audience; For over a decade, MapReduce has become a prominent programming model to handle vast amounts of raw data in large scale systems. This model ensures scalability, reliability and availability aspects with reasonable query processing time. However these large scale systems still face some challenges: data skew, task imbalance, high disk I/O and redistribution costs can have disastrous effects on performance. In this paper, we introduce MRFA-Join algorithm: a new frequency adaptive algorithm based on MapReduce programming model and a randomised key redistribution approach for join processing of large-scale datasets. A cost analysis of this algorithm shows that our approach is insensitive to data skew and ensures perfect balancing properties during all stages of join computation. These performances have been confirmed by a series of experimentations.

The number of cloud offerings increases rapidly. Therefore, it is difficult for clients to select the adequate cloud providers which fit their needs. In this thesis, we introduce a cloud service brokerage mechanism that considers the client security requirements. We consider two types of the client requirements. The amount of resources is represented by the functional requirements. The non-functional requirements consist on security properties and placement constraints. The requirements and the offers are specified using the Alloy language. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required resources in the adequate cloud providers, in a way that fulfills all customer requirements, including security properties. The broker checks that the placement configuration ensures all the security requirements. All these steps are done before the resources deployment in the cloud computing. This allows to detect the conflicts and errors in the clients requirements, thus resources vulnerabilities can be avoided after the deployment.; Les offres de l’informatique en nuage augmentent de plus en plus et les clients ne sont pas capables de lescomparer afin de choisir la plus adaptée à leurs besoins. De plus, les garanties de sécurité proposées parles fournisseurs restent incompréhensibles pour les clients. Cela représente un frein pour l'adoption dessolutions de l’informatique en nuage.Dans cette thèse, nous proposons un mécanisme de courtage des services de l’informatique en nuage quiprend en compte les besoins du client en termes de sécurité.Les besoins exprimés par le client sont de deux natures. Les besoins fonctionnels représentent lesressources et leurs performances. Les besoins non-fonctionnels représentent les propriétés de sécurité etles contraintes de placement des ressources dans le nuage informatique. Nous utilisons le langage Alloypour décrire les offres et les besoins. Nous utilisons l'analyseur Alloy pour l'analyse et la vérification desspécifications du client. Le courtier sélectionne les fournisseurs qui satisfont les besoins fonctionnels et nonfonctionnelsdu client. Il vérifie ensuite, que la configuration du placement des ressources chez lesfournisseurs respecte toutes les propriétés de sécurité exigées par le client.Toutes ces démarches sont effectuées avant le déploiement des ressources dans le nuage informatique.Cela permet de détecter les erreurs et conflits des besoins du client tôt. Ainsi, on réduit les vulnérabilités desressources du client une fois déployées.

Nowadays, we are using an increasing number of computer applications. Errors in critical applications (medicine, transport, . . .) may carry serious health or financial issues. Avoiding errors in programs is a challenge and may be achieved by deductive verification. Deductive verification applies to program written in a high-level languages, which are transformed into machine language by compilers. These compilers must be correct to ensure the nonpropagation of errors to machine code. Since 2005, multicore processors have spread in all electronic devices. So, these architectures need adapted compilers and proofs of correctness. Our work is the modular extension of a verified compiler for parallel languages targeting multicore architectures. Specifications of these languages (and their operational semantics) needed at all levels of the compiler and proofs of correctness of this compiler are parameterized by modules specifying elements of parallelism such as a relaxed memory model and notions of synchronization and scheduling between threads. This work is the first step in the conception of a certified compiler for high-level parallel languages such as algorithmic skeletons.; Les applications informatiques sont de plus en plus présentes dans nos vies. Pour les applications critiques (médecine, transport, . . .), les conséquences d’une erreur informatique ont un coût inacceptable, que ce soit sur le plan humain ou financier. Une des méthodes pour éviter la présence d’erreurs dans les programmes est la vérification déductive. Celle-ci s’applique à des programmes écrits dans des langages de haut-niveau transformés, par des compilateurs, en programmes écrits en langage machine. Les compilateurs doivent être corrects pour ne pas propager d’erreurs au langage machine. Depuis 2005, les processeurs multi-coeurs se sont répandus dans l’ensemble des systèmes informatiques. Ces architectures nécessitent des compilateurs et des preuves de correction adaptées. Notre contribution est l’extension modulaire d’un compilateur vérifié pour un langage parallèle ciblant des architectures parallèles multi-coeurs. Les spécifications des langages (et leurs sémantiques opérationnelles) présents aux divers niveaux du compilateur ainsi que les preuves de la correction du compilateur sont paramétrées par des modules spécifiant des éléments de parallélisme tels qu’un modèle mémoire faible et des notions de synchronisation et d’ordonnancement entre processus légers. Ce travail ouvre la voie à la conception d’un compilateur certifié pour des langages parallèles de haut-niveau tels que les langages à squelettes algorithmiques.

Transactions are becoming a popular mechanism for parallel and concurrent programming. In most implementations the nesting of transactions is not supported which hinders modularity. Rather than transactions, which are an implementation choice, we consider directly the notion of atomic section. For the sake of modularity with we consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our first contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. This is done on execution traces without being specific to a language syntax and operational semantics. This first part of our work could be considered as a specification for the design and implementation of such a parallel language. A formalisation of our results in the Coq proof assistant is also available. Our second contribution is a formal definition of the Atomic Fork Join (AFJ) language and its operational semantics. We show that it indeed satisfies the conditions previously defined. The third contribution of our work is a compilation procedure of AFJ programs to programs another language with threads and locks but without atomic sections, named Lock Unlock Fork Join (LUFJ). We study the correctness of the compilation from AFJ to LUFJ.; La mémoire transactionnelle est un mécanisme de plus en plus populaire pour la programmation parallèle et concurrente. Dans la plupart des implantations, l’emboîtement de transactions n’est pas possible ce qui pénalise la modularité. Plutôt que les transactions, qui sont un choix possible d’implantation, nous considérons directement la notion de section atomique. Dans un objectif d’améliorer la modularité et l’expressivité, nous considérons un langage impératif simple étendu avec des instructions de parallélisme avec lancement et attente de processus légers et une instruction de section atomique à portée syntaxique, depuis laquelle des processus légers peuvent s’échapper. Dans ce contexte notre première contribution est la définition précise de l’atomicité et de la bonne synchronisation. Nous prouvons que pour des traces bien formées, la dernière implique la forme forte de la première. Ceci est fait sur des traces d’exécution abstraites dans le sens où nous ne définissons par précisément la syntaxe et la sémantique opérationnelle d’un langage de programmation. Cette première partie de notre travail peut être considérée comme une spécification pour un tel langage. Nous avons utilisé l’assistant de preuve Coq pour modéliser et prouver nos résultats. Notre deuxième contribution est la définition formelle du langage Atomic Fork Join (AFJ). Nous montrons que les traces de sa sémantique opérationnelle vérifient effectivement les conditions de bonne formation définies précédemment. La troisième contribution est la compilation de programmes AFJ en programmes Lock Unlock Fork Join (LUFJ) un langage avec processus léger et verrous mais sans sections atomiques. Nous étudions la correction de la compilation de AFJ vers LUFJ.

Parallel program design and implementation is a complex, error prone task. Verifying parallel programs is also harder than verifying sequential ones. To ease the development and the proof of correction of parallel programs, we propose to combine the functional bulk synchronous parallel language BSML; the algorithmic skeleton, that are higher order function on distributed data structures which offer an abstraction of the parallelism ; and the Coq proof assistant, who’s specification language is rich enough to write purely functional programs together with their properties. We propose an embedding of BSML primitives in the Coq logic in a modular form, adapted to program extraction. So we can write BSML programs in Coq, reason on them, extract them and then execute them in parallel. To ease the specification of these programs, we formalise the relation between parallel programs using distributed data structures and specification using sequential data structure. We prove the correctness of an implementation of the BH skeleton. This skeleton is devoted to the treatment of distributed lists in the BSP model. For a set of application, starting from a sequential specification of a problem, we derive an instance of our skeletons, then extract a BSML program which is executed on parallel machines.; Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels. Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d’ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme – et l’assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l’extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, raisonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles. Nous prouvons ainsi la correction d’une implantation du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d’applications partant d’une spécification d’un problème sous forme d’un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l’exécuter sur des machines parallèles.

The appeal of parallel processing becomes very strong in applications which require ever higher performance and particularly in applications such as: data-warehousing, decision support, On-Line Analytical Processing (OLAP) and more generally DBMS. A linear speed-up is the main objective of parallel algorithms. However, in real applications, it's not obvious to reach this objective due to the high communication cost in parallel and distributed systems and to the possible skew in the charge of different processors. In addition, on heterogeneous multi-user architectures, the load of each processor may highly vary in a dynamic and unpredictable way. In this thesis, we are interested in treating the join and multi-join queries on distributed multi-user heteregeneous systems, grid systems and distributed file systems. We have proposed several algorithms based on using distributed histograms. These algorithms are based on a dynamic data distribution and task allocation which makes them insensitive to data skew and ensure perfect balancing properties during all stages of join computation even on heteregeneous multi-user environment. The complexity analysis of our algorithms and the experimental results show that they have a near-linear speedup.; L'émergence des applications de bases de données dans les domaines tels que le data warehousing, le data mining et l'aide à la décision qui font généralement appel à de très grands volumes de données rend la parallélisation des algorithmes des jointures nécessaire pour avoir un temps de réponse acceptable. Une accélération linéaire est l'objectif principal des algorithmes parallèles, cependant dans les applications réelles, elle est difficilement atteignable : ceci est dû généralement d'une part aux coûts de communications inhérents aux systèmes multi-processeur et d'autre part au déséquilibre des charges des différents processeurs. En plus, dans un environnement hétérogène multi-utilisateur, la charge des différents processeurs peut varier de manière dynamique et imprévisible. Dans le cadre de cette thèse, nous nous intéressons au traitement de la jointure et de la multi-jointure sur les architectures distribuées hétérogènes, les grilles de calcul et les systèmes de fichiers distribués. Nous avons proposé une variété d'algorithmes, basés sur l'utilisation des histogrammes distribués, pour traiter de manière efficace le déséquilibre des données, tout en garantissant un équilibrage presque parfait de la charge des différents processeurs même dans un environnement hétérogène et multi-utilisateur. Ces algorithmes sont basés sur une approche dynamique de redistribution des données permettant de réduire les coûts de communication à un minimum tout en traitant de manière très efficace le problème de déséquilibre des valeurs de l'attribut de jointure. L'analyse de complexité de nos algorithmes et les résultats expérimentaux obtenus montrent que ces algorithmes possèdent une accélération presque linéaire.

The appeal of parallel processing becomes very strong in applications which require ever higher performance and particularly in applications such as: data-warehousing, decision support, On-Line Analytical Processing (OLAP) and more generally DBMS. A linear speed-up is the main objective of parallel algorithms. However, in real applications, it's not obvious to reach this objective due to the high communication cost in parallel and distributed systems and to the possible skew in the charge of different processors. In addition, on heterogeneous multi-user architectures, the load of each processor may highly vary in a dynamic and unpredictable way. In this thesis, we are interested in treating the join and multi-join queries on distributed multi-user heteregeneous systems, grid systems and distributed file systems. We have proposed several algorithms based on using distributed histograms. These algorithms are based on a dynamic data distribution and task allocation which makes them insensitive to data skew and ensure perfect balancing properties during all stages of join computation even on heteregeneous multi-user environment. The complexity analysis of our algorithms and the experimental results show that they have a near-linear speedup., L'émergence des applications de bases de données dans les domaines tels que le data warehousing, le data mining et l'aide à la décision qui font généralement appel à de très grands volumes de données rend la parallélisation des algorithmes des jointures nécessaire pour avoir un temps de réponse acceptable. Une accélération linéaire est l'objectif principal des algorithmes parallèles, cependant dans les applications réelles, elle est difficilement atteignable : ceci est dû généralement d'une part aux coûts de communications inhérents aux systèmes multi-processeur et d'autre part au déséquilibre des charges des différents processeurs. En plus, dans un environnement hétérogène multi-utilisateur, la charge des différents processeurs peut varier de manière dynamique et imprévisible. Dans le cadre de cette thèse, nous nous intéressons au traitement de la jointure et de la multi-jointure sur les architectures distribuées hétérogènes, les grilles de calcul et les systèmes de fichiers distribués. Nous avons proposé une variété d'algorithmes, basés sur l'utilisation des histogrammes distribués, pour traiter de manière efficace le déséquilibre des données, tout en garantissant un équilibrage presque parfait de la charge des différents processeurs même dans un environnement hétérogène et multi-utilisateur. Ces algorithmes sont basés sur une approche dynamique de redistribution des données permettant de réduire les coûts de communication à un minimum tout en traitant de manière très efficace le problème de déséquilibre des valeurs de l'attribut de jointure. L'analyse de complexité de nos algorithmes et les résultats expérimentaux obtenus montrent que ces algorithmes possèdent une accélération presque linéaire.

Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs, Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées

Some problems require performances that can only be provided by massively parallel machinesand meta-computers. Nevertheless, algorithm writing for this kind of machine remains more difficultthan for those strictly sequential and the conception of adapted languages is an active subject of researchnotwithstanding the frequent use of the concurrent programming. Indeed, the conception of a programminglanguage is the result of a compromise which determines balance between various qualities of the languagesuch as expressivity, safety, effectiveness or the simplicity of the semantics.In the prior works to this thesis, it was undertaken to study, with greater details, the intermediate positionthat the paradigm of the skeletons occupies. However, this did not involve conceiving an a priori fixed setsof operations and then to design performance models, but, to fix a structured parallelism model (with itsperformancemodel) and then to design a universal number of operations making it possible to program anyalgorithm of this model. The objective is therefore as follows : have an universal language in which theprogrammer can have an idea of the cost from the source code.This thesis comes under the project "CoordinAtion and Distribution of Multiprocessor Applications inobjective camL" (CARAML) of the ACI GRID. The objective was the development of libraries for highperformanceand globalised computations around the OCaml language. This project was organized in threesuccessive phases : safety and irregular data-parallel operations (mono-user) ; data-parallel multiprocessingoperations ; globalised operations for grid computing.The thesis follows the organization in three phases of the CARAML project and presents the contributionsof the author in each phase in the three parts : a semantic study of a functional language for BSP programmingand the certification of the written programs in this language ; a presentation of a primitive of parallelcomposition (and which also allows programming parallel "divide-and-conquer" algorithms), an exampleof application using an implementation of parallel data structures and an extension for parallel input/outputsin BSML ; the adaption of the language for meta-computing., Certains problèmes nécessitent des performances que seules les machines massivement parallèlesou les méta-ordinateurs peuvent offrir. L'écriture d'algorithmes pour ce type de machines demeureplus difficile que pour celles strictement séquentielles et la conception de langages adaptés est un sujet derecherche actif nonobstant la fréquente utilisation de la programmation concurrente. En effet, la conceptiond'un langage de programmation est le résultat d'un compromis qui détermine l'équilibre entre les différentesqualités du langage telles que l'expressivité, la sûreté, la prédiction des performances, l'efficacité oubien la simplicité de la sémantique.Dans des travaux antérieurs à cette thèse, il a été entrepris d'approfondir la position intermédiaire que leparadigme des patrons occupe. Toutefois il ne s'agissait pas de concevoir un ensemble a priori fixé d'opérationspuis de concevoir des méthodologies pour la prédiction des performances, mais de fixer un modèlede parallélisme structuré (avec son modèle de coûts) puis de concevoir un ensemble universel d'opérationspermettant de programmer n'importe quel algorithme de ce modèle. L'objectif est donc le suivant : parvenirà la conception de langages universels dans lesquels le programmeur peut se faire une idée du coût à partirdu code source.Cette thèse s'inscrit dans le cadre du projet «CoordinAtion et Répartition des Applications Multiprocesseursen objective camL» (CARAML) de l'ACI GRID dont l'objectif était le développement de bibliothèquespour le calcul haute-performance et globalisé autour du langage OCaml. Ce projet était organisé en troisphases successives : sûreté et opérations data-parallèles irrégulières mono-utilisateur ; opérations de multitraitementdata-parallèle ; opérations globalisées pour la programmation de grilles de calcul.Ce tapuscrit est organisé en 3 parties correspondant chacune aux contributions de l'auteur dans chacunedes phases du projet CARAML : une étude sémantique d'un langage fonctionnel pour la programmationBSPet la certification des programmes écrits dans ce langage ; une présentation d'une primitive de compositionparallèle (et qui permet aussi la programmation d'algorithmes «diviser-pour-régner» parallèles), un exempled'application via l'utilisation et l'implantation de structures de données parallèles et une extension pour lesentrées/sorties parallèles en BSML ; l'adaption du langage pour le méta-calcul.

Cet ouvrage s'adresse à tous ceux qui, au-delà de l'utilisation d'un système d'exploitation et de la programmation système, veulent comprendre comment est conçu et implémenté le noyau du système Linux. Il en explore le code source dans sa toute première version (Linux 0.01), et commente ses évolutions vers les noyaux actuels. L'ouvrage éclaire notamment l'utilisation des ressources du microprocesseur et les commandes des cartes des périphériques, et permet de comprendre comment aborder la conception de pilotes.