Mapping and scheduling on multi-core processors using SMT solvers

In order to achieve performance gains, computers have evolved to multi-core and many-core platforms abounding with multiple processor cores. However the problem of finding efficient ways to execute parallel software on them is hard. With a large number of processor cores available, the software must orchestrate the communication, synchronization along with the code execution. Communication corresponds to the transport of data between different processors, handled transparently by the hardware or explicitly by the software.Models which represent the algorithms in a structured and formal way expose the available parallelism. Deployment of the software algorithms represented by such models needs a specification of which processor to execute the tasks on (mapping) and when to execute them (scheduling). Mapping and scheduling is a hard combinatorial problem with exponential number of solutions. In addition, the solutions have multiple costs that need to be optimized, such as memory consumption, time to execute, resources used etc. Such a problem with multiple costs is called a multi-criteria optimization problem. The solution to this problem is a set of incomparable solutions called Pareto solutions which need special algorithms to approximate them.We target a class of applications called streaming applications, which process a continuous stream of data. These applications apply similar computation on different data items, can be conveniently expressed by a class of models called dataflow models. We encode mapping and scheduling problem in form of logical constraints and present it to satisfiability modulo theory (SMT) solvers. SMT solvers, solve the encoded problem by using a combination of search techniques and constraint propagation to find an assignment to the problem variables satisfying the given cost constraints.In dataflow applications, the design space explodes with increased number of tasks and processors. In this thesis, we tackle this problem by introduction symmetry reduction techniques and demonstrate that symmetry breaking accelerates search in SMT solver, increasing the size of the problem that can be solved. Our design-space exploration algorithm approximates Pareto front of the problem and produces solutions with different cost trade-offs. Further we extend the scheduling problem to the many-core platforms which are a group of multi-core platforms connected by network-on-chip. We provide a design flow which performs mapping of the applications on such platforms and automatic insertion of additional elements to model the communication using bounded memory. We provide experimental results obtained on the 256-processor Kalray and the Tilera TILE-64 platforms.The multi-core processors have typically a small amount of memory close to the processor, generally insufficient for all application data to fit. We study a class of parallel applications having a regular data access pattern and large amount of data to be processed by a uniform computation. The data must be brought from main memory to local memory, processed and then the results written back to main memory, all in batches. Selecting the proper granularity of the data that is brought into local memory is an optimization problem. We formalize this problem and provide a way to determine the optimal transfer granularity depending on the characteristics of application and the hardware platform.In addition to the scheduling problems and local memory management, we study a part of the problem of runtime management of the applications. Applications in modern embedded systems can start and stop dynamically. In order to execute all the applications efficiently and to optimize global costs such as power consumption, execution time etc., the applications must be reconfigured dynamically at runtime. We present a predictable and composable (executing independently without affecting others) way of migrating tasks according to the reconfiguration decision.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