Sûreté : de l'analyse à l'instrumentation et à la synthèse de code

Résumé : Les machines multiprocesseurs, multi-cœurs et les accélérateurs de type GPU se généralisent et pourtant il devient de plus en plus difficile pour les programmeurs de tirer profit de leurs capacités. La compilation source-à-source des applications permet de faciliter le développement d’implémentations efficaces pour ces architectures complexes. Mes travaux de recherche s’inscrivent selon deux axes principaux. Le premier relève de la compilation et de l’optimisation d’applications en vue de leur exécution efficace sur des architectures parallèles. Le deuxième axe relève de l’utilisation de l’algèbre linéaire en nombres entiers pour modéliser les problèmes rencontrés. Cette thèse présente, tout d’abord, les analyses statiques et dynamiques de programmes développées pour vérifier la correction d’un code et faciliter sa maintenance, telles que la mise en conformité par rapport à la norme du langage source, la détection de variables non initialisées, la vérification du non-débordement des accès à des éléments de tableaux et le calcul de dépendances de données. Ces analyses ont été intégrées dans le compilateur PIPS. Puis, des méthodes de génération automatique de code de contrôle et des communications à partir de spécifications sont exposées. Des modélisations du placement des données sur les processeurs, des calculs pouvant être exécutés en parallèle et des communications devant être générées pour conserver la cohérence des données sont proposées. Les algorithmes de synthèse de code spécifiquement développés pour HPF, pour une mémoire virtuelle partagée émulée sur une architecture distribuée et pour des transferts compatibles avec des DMAs sont ensuite détaillées. Finalement, une approche globale du problème de placement d’une application pour une architecture embarquée parallèle, qui utilise la programmation logique concurrente par contraintes comme moteur, est présentée. Une même abstraction a été choisie pour les analyses et la modélisation des problèmes d’optimisation et de génération de code : un système de contraintes linéaires où les variables sont des entiers. Le choix des Z -polyèdres a permis de rester dans un cadre algébrique disposant d’une large gamme de méthodes de résolution, aisées pour les preuves.
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/tel-01518362
Contributeur : Claire Medrala <>
Soumis le : jeudi 4 mai 2017 - 15:11:11
Dernière modification le : vendredi 10 novembre 2017 - 14:54:43
Document(s) archivé(s) le : samedi 5 août 2017 - 13:10:17

Fichier

Identifiants

  • HAL Id : tel-01518362, version 1

Collections

Citation

Corinne Ancourt. Sûreté : de l'analyse à l'instrumentation et à la synthèse de code. Calcul parallèle, distribué et partagé [cs.DC]. Université Pierre et Marie Curie (Paris 6), 2015. 〈tel-01518362〉

Partager

Métriques

Consultations de la notice

88

Téléchargements de fichiers

37