Allocation et ordonnancement sur des processeurs multi-coeur avec des solveurs SMT
Pranav Tendulkar · 2014
Mapping and scheduling on multi-core processors using SMT solvers Dans l’objectif d’augmenter les performances, l’architecture des processeurs a évolué versdes 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èmedifficile. Avec un grand nombre d’unités de calcul disponibles, le logiciel doit orchestrer lacommunication 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 lematé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èlesné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 sontdes problèmes combinatoires difficile avec un nombre exponentiel de solutions. En outre, lessolutions ont différents coûts qui doivent être optimisés : la consommation de mémoire, letemps 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 desalgorithmes spéciaux pour l’approximer.Nous ciblons une classe d’applications, appelées applications de streaming, qui traitentun 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èlesappelés modèles de flux de données. Le problème du placement et de l’ordonnancementest codé sous forme de contraintes logiques et résolu par un solveur Satisfaisabilité ModuloThéories (SMT). Les solveurs SMT résolvent le problème en combinant des techniques derecherche et de la propagation de contraintes afin d’attribuer des valeurs aux variables duproblème satisfaisant les contraintes de coût données.Dans les applications de flux de données, l’espace de conception explose avec l’augmentationdu nombre de tâches et de processeurs. Dans cette thèse, nous nous attaquons à ceproblème par l’introduction des techniques de réduction de symétrie et démontrons que larupture de symétrie accélère la recherche dans un solveur SMT, permettant ainsi l’augmentationde la taille du problème qui peut être résolu. Notre algorithme d’exploration de l’espacede conception approxime le front de Pareto du problème et produit des solutions pour différentscompromis de coûts. De plus, nous étendons le problème d’ordonnancement pour lesplate-formes "many-core" qui sont une catégorie de plate-forme multi coeurs où les unités sontconnectés par un réseau sur puce (NoC). Nous fournissons un flot de conception qui réalise leplacement des applications sur de telles plate-formes et insert automatiquement des élémentssupplémentaires pour modéliser la communication à l’aide de mémoires de taille bornée. Nousprésentons des résultats expérimentaux obtenus sur deux plate-formes existantes : la machineKalray à 256 processeurs et les Tilera TILE-64.