L'avènement des puces multicoeurs repose certaines questions quant aux moyens d'écrire les programmes, qui doivent alors intégrer un degré élevé de parallélisme. Nous abordons cette question par l'intermédiaire de deux points de vue orthogonaux. Premièrement via le paradigme du vol de travail, pour lequel nous effectuons une étude visant d'une part à rechercher quelles sont les caractéristiques architecturales simples donnant les meilleures performances pour une implémentation de ce paradigme ; et d'autre part à montrer que le surcout par rapport à une parallélisation statique est faible tout en permettant des gains en performances grâce à l'équilibrage dynamique des charges. Cette question est néanmoins surtout abordée via le paradigme de programmation à base de transactions -- ensemble d'instructions s'exécutant de manière atomique du point de vue des autres coeurs. Supporter cette abstraction nécessite l'implantation d'un système dit TM, souvent complexe, pouvant être logiciel ou matériel. L'étude porte premièrement sur la comparaison de systèmes TM matériels basés sur des choix architecturaux différents (protocole de cohérence de cache), puis sur l'impact d'un point de vue performances de plusieurs politiques de résolution des conflits, autrement dit des actions à prendre quand deux transactions essaient d'accéder simultanément les mêmes données.

Cette thèse aborde le problème de la vérification automatique de systèmesparamétrés complexes. Cette approche est importante car elle permet de garantircertaines propriétés sans connaître a priori le nombre de composants dusystème. On s'intéresse en particulier à la sûreté de ces systèmes et on traitele côté paramétré du problème avec des méthodes symboliques. Ces travauxs'inscrivent dans le cadre théorique du model checking modulo théories et ontdonné lieu à un nouveau model checker : Cubicle.Une des contributions principale de cette thèse est une nouvelle technique pourinférer des invariants de manière automatique. Le processus de générationd'invariants est intégré à l'algorithme de model checking et permet de vérifieren pratique des systèmes hors de portée des approches symboliquestraditionnelles. Une des applications principales de cet algorithme estl’analyse de sûreté paramétrée de protocoles de cohérence de cache de tailleindustrielle.Enfin, pour répondre au problème de la confiance placée dans le model checker,on présente deux techniques de certification de notre outil Cubicle utilisantla plate-forme Why3. La première consiste à générer des certificats dont lavalidité est évaluée de manière indépendante tandis que la seconde est uneapproche par vérification déductive du cœur de Cubicle. / This thesis tackles the problem of automatically verifying complexparameterized systems. This approach is important because it can guarantee thatsome properties hold without knowing a priori the number of components in thesystem. We focus in particular on the safety of such systems and we handle theparameterized aspect with symbolic methods. This work is set in the theoreticalframework of the model checking modulo theories and resulted in a new modelchecker: Cubicle.One of the main contribution of this thesis is a novel technique forautomatically inferring invariants. The process of invariant generation isintegrated with the model checking algorithm and allows the verification inpractice of systems which are out of reach for traditional symbolicapproaches. One successful application of this algorithm is the safety analysisof industrial size parameterized cache coherence protocols.Finally, to address the problem of trusting the answer given by the modelchecker, we present two techniques for certifying our tool Cubicle based on theframework Why3. The first consists in producing certificates whose validity canbe assessed independently while the second is an approach by deductiveverification of the heart of Cubicle.

Les architectures distribuées sont fréquemment utilisées pour le calcul haute performance (HPC). Afin de réduire la consommation énergétique, certains fabricants de processeurs sont passés d’architectures multi-cœurs en mémoire partagée aux MPSoC. Les MPSoC (Multi-Processor System On Chip) sont des architectures incluant un système distribué dans une puce.La programmation des architectures distribuées est plus difficile que pour les systèmes à mémoire partagée, principalement à cause de la nature distribuée de la mémoire. Une famille d’outils nommée DSM (Distributed Shared Memory) a été développée pour simplifier la programmation des architectures distribuées. Cette famille inclut les architectures NUMA, les langages PGAS, et les supports d’exécution distribués pour graphes de tâches. La stratégie utilisée par les DSM est de créer un espace d’adressage global pour les objets du programme, et de faire automatiquement les transferts réseaux nécessaires lorsque ces objets sont utilisés. Les systèmes DSM sont très variés, que ce soit par l’interface fournie, les fonctionnalités, la sémantique autour des objets globalement adressables, le type de support (matériel ou logiciel), ...Cette thèse présente un nouveau système DSM à support logiciel appelé Givy. Le but de Givy est d’exécuter sur des MPSoC (MPPA) des programmes sous la forme de graphes de tâches dynamiques, avec des dépendances de flot de données (data-flow ). L’espace d’adressage global (GAS) de Givy est indexé par des vrais pointeurs, contrairement à de nombreux autres systèmes DSM à support logiciel : les pointeurs bruts du langage C sont valides sur tout le système distribué. Dans Givy, les objets globaux sont les blocs de mémoire fournis par malloc(). Ces blocs sont répliqués entre les nœuds du système distribué, et sont gérés par un protocole de cohérence de cache logiciel nommé Owner Writable Memory. Le protocole est capable de déplacer ses propres métadonnées, ce qui devrait permettre l’exécution efficace de programmes irréguliers. Le modèle de programmation impose de découper le programme en tâches créées dynamiquement et annotées par leurs accès mémoire. Ces annotations sont utilisées pour générer les requêtes au protocole de cohérence, ainsi que pour fournir des informations à l’ordonnanceur de tâche (spatial et temporel).Le premier résultat de cette thèse est l’organisation globale de Givy. Une deuxième contribution est la formalisation du protocole Owner Writable Memory. Le troisième résultat est la traduction de cette formalisation dans le langage d’un model checker (Cubicle), et les essais de validation du protocole. Le dernier résultat est la réalisation et explication détaillée du sous-système d’allocation mémoire : le choix de pointeurs bruts en tant qu’index globaux nécessite une intégration forte entre l’allocateur mémoire et le protocole de cohérence de cache. / Distributed systems are widely used in HPC (High Performance Computing). Owing to rising energy concerns, some chip manufacturers moved from multi-core CPUs to MPSoC (Multi-Processor System on Chip), which includes a distributed system on one chip.However distributed systems – with distributed memories – are hard to program compared to more friendly shared memory systems. A family of solutions called DSM (Distributed Shared Memory) systems has been developed to simplify the programming of distributed systems. DSM systems include NUMA architectures, PGAS languages, and distributed task runtimes. The common strategy of these systems is to create a global address space of some kind, and automate network transfers on accesses to global objects. DSM systems usually differ in their interfaces, capabilities, semantics on global objects, implementation levels (hardware / software), ...This thesis presents a new software DSM system called Givy. The motivation of Givy is to execute programs modeled as dynamic task graphs with data-flow dependencies on MPSoC architectures (MPPA). Contrary to many software DSM, the global address space of Givy is indexed by real pointers: raw C pointers are made global to the distributed system. Givy global objects are memory blocks returned by malloc(). Data is replicated across nodes, and all these copies are managed by a software cache coherence protocol called Owner Writable Memory. This protocol can relocate coherence metadata, and thus should help execute irregular applications efficiently. The programming model cuts the program into tasks which are annotated with memory accesses, and created dynamically. Memory annotations are used to drive coherence requests, and provide useful information for scheduling and load-balancing.The first contribution of this thesis is the overall design of the Givy runtime. A second contribution is the formalization of the Owner Writable Memory coherence protocol. A third contribution is its translation in a model checker language (Cubicle), and correctness validation attempts. The last contribution is the detailed allocator subsystem implementation: the choice of real pointers for global references requires a tight integration between memory allocator and coherence protocol.