Détails sur le séminaire

Résumé : Dans l'objectif d'augmenter les performances, l'architecture des processeurs a évolué vers des plate-formes multi-core et many-core composées de multiple unités de traitements. Toutefois, trouver des moyens efficaces pour exécuter du logiciel parallèle reste un problème difficile. Avec un grand nombre d'unités de calcul disponibles, le logiciel doit orchestrer la communication et assurer la synchronisation lors de l’exécution du code. La communication (transport des données entre les différents processeurs) est gérée de façon transparente par le matériel ou explicitement par le logiciel.
Les modèles qui représentent les algorithmes de façon structurée et formelle mettent en évidence leur parallélisme inhérent. Le déploiement des logiciels représentés par ces modèles nécessite de spécifier placement (sur quel processeur s’exécute une certaine tâche) et l'ordonnancement (dans quel ordre sont exécutées les tâches). Le placement et l'ordonnancement sont des problèmes combinatoires difficile avec un nombre exponentiel de solutions. En outre, les solutions ont différents coûts qui doivent être optimisés : la consommation de mémoire, le temps d'exécution, les ressources utilisées, etc. C'est un problème d'optimisation multi-critères. La solution à ce problème est ce qu'on appelle un ensemble Pareto-optimal nécessitant des algorithmes spéciaux pour l’approximer.
Nous ciblons une classe d'applications, appelées applications de streaming, qui traitent un flux continu de données. Ces applications qui appliquent un calcul similaire sur différents éléments de données successifs, peuvent être commodément exprimées par une classe de modèles appelés modèles de flux de données. Le problème du placement et de l'ordonnancement est codé sous forme de contraintes logiques et résolu par un solveur Satisfaisabilité Modulo Théories (SMT). Les solveurs SMT résolvent le problème en combinant des techniques de recherche et de la propagation de contraintes afin d'attribuer des valeurs aux variables du problème satisfaisant les contraintes de coût données.
Dans les applications de flux de données, l'espace de conception explose avec l'augmentation du nombre de tâches et de processeurs. Dans cette thèse, nous nous attaquons à ce problème par l'introduction des techniques de réduction de symétrie et démontrons que la rupture de symétrie accélère la recherche dans un solveur SMT, permettant ainsi l'augmentation de la taille du problème qui peut être résolu. Notre algorithme d'exploration de l'espace de conception approxime le front de Pareto du problème et produit des solutions pour différents compromis de coûts. De plus, nous étendons le problème d'ordonnancement pour les plate-formes many-core qui sont une catégorie de plate-forme multi coeurs où les unités sont connectés par un réseau sur puce (NOC). Nous fournissons un flot de conception qui réalise le placement des applications sur de telles plate-formes et insert automatiquement des éléments supplémentaires pour modéliser la communication à l'aide de mémoires de taille bornée. Nous présentons des résultats expérimentaux obtenus sur deux plate-formes existantes : la machine Kalray à 256 processeurs et les Tilera TILE-64.
Les processeurs multi-cœurs ont typiquement une faible quantité de mémoire proche du processeur. Celle ci est généralement insuffisante pour contenir toutes les données necessaires au calcul d'une tâche. Nous étudions une classe d'applications parallèles présentant un pattern régulier d'accès aux données et une grande quantité de données à traiter par un calcul uniforme. Les données doivent être acheminées depuis la mémoire principale vers la mémoire locale, traitées, puis, les résultats retournés en mémoire centrale, tout en lots. Fixer la bonne granularité des données acheminées en mémoire locale est un problème d'optimisation. Nous formalisons ce problème et proposons un moyen de déterminer la granularité de transfert optimale en fonction des caractéristiques de l'application et de la plate-forme matérielle.
En plus des problèmes d'ordonnancement et de gestion de la mémoire locale, nous étudions une partie du problème de la gestion de l'exécution des applications. Dans les systèmes embarqués modernes, les applications peuvent démarrer et s'arrêter dynamiquement. Afin d'exécuter toutes les applications de manière efficace et d'optimiser les coûts globaux tels que la consommation d'énergie, temps d'exécution, etc., les applications nécessitent d'être reconfigurées dynamiquement à l'exécution. Nous présentons une manière prévisible et composable (exécution indépendamment sans affecter les autres) de réaliser la migration des tâches conformément à la décision de reconfiguration.



Dear all,
It is a great pleasure to invite you to the defense of my PhD thesis titled
Mapping and Scheduling on Multi-core Processors using SMT Solvers
The defense will be held on the 13th of October at 14:00, in English, at
CTL Amphitheater, Verimag. A map is available at
http://www-verimag.imag.fr/Venir-a-Verimag.html?lang=.
You are all cordially invited to the pot de thèse that will happen
after in the same place.
Jury :
Dr. Albert Cohen INRIA, Paris, Rapporteur
Prof. Marc Geilen Technical University of Eindhoven, Netherlands, Rapporteur
Prof. Dimitrios S. Nikolopoulos Queen’s University, Belfast, UK, Examinateur
Dr. Alain Girault INRIA, Grenoble, Examinateur
Dr. Benoît Dinechin Kalray, Grenoble, Examinateur
Dr. Phil Harris United Technologies Research Center, Cork, Ireland, Examinateur
Dr. Oded Maler CNRS, Verimag, Directeur de thèse
Dr. Peter Poplavko Verimag, Co-Directeur de thèse