Dans le domaine du développement logiciel, le changement est la seule constante. Les logiciels évoluent parfois de façon substantielle et, pendant ce processus, des séquences de transformation de code (par exemple, créer une classe, puis surcharger une méthode) sont systématiquement appliquées dans le système (e.g. à certaines classes dans une même hiérarchie). De par la nature répétitive de ces transformations, il est nécessaire d’automatiser leur support afin d’assurer que ces séquences de transformations sont appliquées de façon consistante sur la globalité du système.Dans cette thèse, nous proposons d’améliorer les transformations de code pour mieux aider les développeurs dans l’application de transformation de code systématiques et complexes. Nous couvrons deux aspects:• Le support automatisé pour composer et appliquer des séquences de transformations de code. Nous réalisons une recherche de l’existence de telles séquences dans de vrais logiciels. Nous proposons un outil pour appliquer automatiquement ces séquences dans les systèmes que nous avons analysés. • La détection de violations de bons principes dans la conception lors d’efforts de transformation. Nous proposons un outil qui recommande des transformations additionnelles pour résoudre les violations de conception qui ont pu être détectées après avoir effectué les transformations de refactoring.Nous évaluons les approches proposées quantitativement et qualitativement sur des cas d’étude issus du monde réel, parfois avec l’aide des experts du système analysé. Les résultats obtenus montrent la pertinence de nos approches. / In software development, change is the only constant. Software systems sometimes evolve in a substantial way and, during this process, sequences of code transformations (e.g., create a class, then override a method) are systematically performed in the system (e.g., to some classes in the same hierarchy). Due to the repetitive nature of these transformations, some automated support is needed to ensure that these sequences of transformations are consistently applied to the entire system.In this thesis we propose to improve source code transformations to better sup- port developers performing more complex and systematic code transformations. We cover two aspects: • The automated support to compose and apply sequences of code transformations. We undergo an investigation on the existence of these sequences in real-world software systems. We propose a tool to automatically apply these sequences in the systems we analyzed. • The detection of design violations during a transformation effort. We undergo an investigation on cases of systematic application of refactoring transformations. We proposed a tool that recommends additional transformations to fix design violations that are detected after performing refactoring transformations.We evaluated the proposed approaches quantitatively and qualitatively in real-world case studies and, in some cases, with the help of experts on the systems under analysis. The results we obtained demonstrate the usefulness of our approaches.

Cette thèse cherche à exploiter le parallélisme dans le contexte des systèmes de gestion de bases de données à objet à d'autres niveaux d'abstraction que celui d'une requête SQL, à savoir le parallélisme intra-transaction et le parallélisme intra-application. Notre approche pour parallélisation des transactions considère un modèle de transactions classiques, ou une transaction est une séquence d'opérations. Le parallélisme intra-transaction consiste à transformer le code d'une transaction pour pouvoir exécuter ses opérations en parallèle. Notre approche pour l'exploitation du parallélisme intra-application étend tout d'abord le modèle de parallélisme intra-transaction de manière à considérer la transaction comme unité de parallélisation. Deuxièmement nous avons considéré l'exploitation du parallélisme intra-application dans un contexte ou le modèle de transactions fournit des transactions emboîtées. Nous avons développé un modèle de parallélisation des applications où nous associons le parallélisme offert par le modèle des transactions emboîtées avec le parallélisme par transformation de notre approche de parallélisation des transactions. Nous avons implanté un premier prototype qui met en oeuvre le modèle de parallélisation des transactions. Pour cela, nous avons utilisé le système de bases de données à objet O2. Notre prototype introduit le parallélisme par la création et la synchronisation des activités parallèles au sein du processus client O2 qui exécute une application. Le système étant développé sur une machine monoprocesseur, les fonctions liées au parallélisme utilisent de processus légers. Nous avons appliqué ensuite notre modèle de parallélisation au système de règles NAOS. Notre approche considère l'ensemble de règles d'un cycle d'exécution, dites règles candidates, pour la parallélisation. Nous construisons un plan d'exécution pour les règles candidates d'un cycle qui détermine l'exécution séquentielle ou parallèle des règles.

Les processeurs graphiques (GPU), originellement dédiés à l'accélération de traitements graphiques, ont une structure hautement parallèle. Les innovations matérielles et de langage de programmation ont permis d'ouvrir le domaine du GPGPU, où les cartes graphiques sont utilisées comme des accélérateurs de calcul pour des applications HPC généralistes.L'objectif de nos travaux est de faciliter l'utilisation de ces nouvelles architectures pour les besoins du calcul haute performance ; ils suivent deux objectifs complémentaires.Le premier axe de nos recherches concerne la transformation automatique de code, permettant de partir d'un code de haut niveau pour le transformer en un code de bas niveau, équivalent, pouvant être exécuté sur des accélérateurs. Dans ce but nous avons implémenté un transformateur de code capable de prendre en charge les boucles « pour » parallèles d'un code OpenMP (simples ou imbriquées) et de le transformer en un code CUDA équivalent, qui soit suffisamment lisible pour permettre de le retravailler par des optimisations ultérieures.Par ailleurs, le futur des architectures HPC réside dans les architectures distribuées basées sur des nœuds dotés d'accélérateurs. Pour permettre aux utilisateurs d'exploiter les nœuds multiGPU, il est nécessaire de mettre en place des schémas d'exécution appropriés. Nous avons mené une étude comparative et mis en évidence que les threads OpenMP permettent de gérer de manière efficace plusieurs cartes graphiques et les communications au sein d'un nœud de calcul multiGPU. / Graphic cards (GPUs), initially used for graphic processing, have a highly parallel architecture. Innovations in both architecture and programming languages opened the new domain of GPGPU where GPUs are used as accelerators for general purpose HPC applications.Our main objective is to facilitate the use of these new architectures for high-performance computing needs; our research follows two main directions.The first direction concerns an automatic code transformation from a high level code into an equivalent low level one, capable of running on accelerators. To this end we implemented a code transformer that can handle parallel “for” loops (single or nested) of an OpenMP code and convert it into an equivalent CUDA code, which is in a human readable form that allows for further optimizations.Moreover, the future of HPC lies in distributed architectures based on hybrid nodes. Specific programming schemes have to be used in order to allow users to benefit from such multiGPU nodes. We conducted a comparative study which revealed that using OpenMP threads is the most adequate way to control multiple graphic cards as well as manage communications efficiently within a multiGPU node.

Les processeurs graphiques (GPU), originellement dédiés à l'accélération de traitements graphiques, ont une structure hautement parallèle. Les innovations matérielles et de langage de programmation ont permis d'ouvrir le domaine du GPGPU, où les cartes graphiques sont utilisées comme des accélérateurs de calcul pour des applications HPC généralistes. L'objectif de nos travaux est de faciliter l'utilisation de ces nouvelles architectures pour les besoins du calcul haute performance ; ils suivent deux objectifs complémentaires. Le premier axe de nos recherches concerne la transformation automatique de code, permettant de partir d'un code de haut niveau pour le transformer en un code de bas niveau, équivalent, pouvant être exécuté sur des accélérateurs. Dans ce but nous avons implémenté un transformateur de code capable de prendre en charge les boucles " pour " parallèles d'un code OpenMP (simples ou imbriquées) et de le transformer en un code CUDA équivalent, qui soit suffisamment lisible pour permettre de le retravailler par des optimisations ultérieures. Par ailleurs, le futur des architectures HPC réside dans les architectures distribuées basées sur des noeuds dotés d'accélérateurs. Pour permettre aux utilisateurs d'exploiter les noeuds multiGPU, il est nécessaire de mettre en place des schémas d'exécution appropriés. Nous avons mené une étude comparative et mis en évidence que les threads OpenMP permettent de gérer de manière efficace plusieurs cartes graphiques et les communications au sein d'un noeud de calcul multiGPU.

Il est de plus en plus fréquent de faire appel à des opérateurs spécifiques en conception de circuits. Les opérateurs spécifiques peuvent être mis en oeuvre par des unités matérielles dédiées, en vue de réduire la taille du code, d'améliorer les performances et de réduire la surface du circuit. Dans cette thèse, nous proposons un flot de conception basé sur l'identification d'opérateurs spécifiques pour la synthèse de haut niveau. Les points clés de ce flot de conception sont l'énumération automatique et la sélection des opérateurs spécifiques à partir d'un code de l'application de haut niveau et la re-génération du code source intégrant les opérateurs spécifiques sélectionnés. Contrairement aux approches proposées précédemment, notre flot de conception est adaptable et est indépendant des outils de synthèse de haut niveau (il ne nécessite pas d'intervenir sur les algorithmes d'ordonnancement et de projection des outils de synthèse de haut niveau). Les résultats expérimentaux montrent que notre approche permet de réduire la surface du circuit de 19% en moyenne, et jusqu'à 37% dans certains cas, par rapport à une synthèse de haut niveau traditionnelle. La latence du circuit est réduite en moyenne de 22%, et atteint jusqu'à 59%. De plus, la taille du code est réduite de 74% en moyenne.

Vérifier formellement des programmes concurrents est une tâche difficile. S’il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d’atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d’analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d’analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d’un code concurrent issu d’un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d’en prouver la validité. Cette validité n’est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cible. / Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.