Le sujet central de cette thèse est le développement d'une méthode dédiée à la preuve de structures de données sans verrou. La motivation première vient du constat que les programmes concurrents sont devenu monnaie courante. Ceci a été possible par l'apparition de nouvelles primitives de synchronisation dans les nouvelles architectures matérielles. La seconde motivation est la quête de logiciel prouvé et donc correct. La sûreté des logiciels est en effet devenue primordiale de par la diffusion des systèmes embarqués et enfouis. La méthode proposée est basée sur le raffinement et dédiée à la conception et la vérification d'algorithme non-bloquant, en particulier ceux sans verrou. La méthode a été formalisée et sa correction prouvée en Isabelle/HOL. Un outil a par ailleurs été développé afin de générer des obligations de preuves à destination des solveurs SMT et des prouveurs de théorèmes du premier ordre. Nous l'avons utilisé afin de vérifier certains de ces algorithmes. / The central topic of this thesis is the proof-based development of lock-free data-structure algorithms. First motivation comes from new computer architectures that come with new synchronisation features. Those features enable concurrent algorithms that do not use locks and are thus more efficient. The second motivation is the search for proved correct program. Nowadays embedded software are used everywhere included in systems where safety is central. We propose a refinement-based method for designing and verifying non-blocking, and in particular lock-free, implementations of data structures. The entire method has been formalised in Isabelle/HOL. An associated prototype tool generates verification conditions that can be solved by SMT solvers or automatic theorem provers for first-order logic, and we have used this approach to verify a number of such algorithms.

Le passage à l'échelle des applications multi-fil sur les systèmes multi-cœuractuels est limité par la performance des algorithmes de verrou, à cause descoûts d'accès à la mémoire sous forte congestion et des défauts de cache. Lacontribution principale présentée dans cette thèse est un nouvel algorithme,Remote Core Locking (RCL), qui a pour objectif d'améliorer la vitessed'exécution des sections critiques des applications patrimoniales sur lesarchitectures multi-cœur. L'idée de RCL est de remplacer les acquisitions deverrou par des appels de fonction distants (RPC) optimisés vers un fild'exécution matériel dédié appelé serveur. RCL réduit l'effondrement desperformances observé avec d'autres algorithmes de verrou lorsque de nombreuxfils d'exécution essaient d'obtenir un verrou de façon concurrente, et supprimele besoin de transférer les données partagées protégées par le verrou vers lefil d'exécution matériel qui l'acquiert car ces données peuvent souventdemeurer dans les caches du serveur.D'autres contributions sont présentées dans cette thèse, notamment un profilerpermettant d'identifier les verrous qui sont des goulots d'étranglement dansles applications multi-fil et qui peuvent par conséquent être remplacés par RCLafin d'améliorer les performances, ainsi qu'un outil de réécriture de codedéveloppé avec l'aide de Julia Lawall. Cet outil transforme les acquisitions deverrou POSIX en acquisitions RCL. L'évaluation de RCL a porté sur dix-huitapplications: les neuf applications des benchmarks SPLASH-2, les septapplications des benchmarks Phoenix 2, Memcached, ainsi que Berkeley DB avec unclient TPC-C. Huit de ces applications sont incapables de passer à l'échelle àcause de leurs verrous et leur performance est améliorée par RCL sur unemachine x86 avec quatre processeurs AMD Opteron et 48 fils d'exécutionmatériels. Utiliser RCL permet de multiplier les performances par 2.5 parrapport aux verrous POSIX sur Memcached, et par 11.6 fois sur Berkeley DB avecle client TPC-C. Sur une machine SPARC avec deux processeurs Sun Ultrasparc T2+et 128 fils d'exécution matériels, les performances de trois applications sontaméliorées par RCL: les performances sont multipliées par 1.3 par rapport auxverrous POSIX sur Memcached et par 7.9 fois sur Berkeley DB avec le clientTPC-C. / The scalability of multithreaded applications on current multicore systems is hampered by the performance of lock algorithms, due to the costs of access contention and cache misses. The main contribution presented in this thesis is a new lock algorithm, Remote Core Locking (RCL), that aims to improve the performance of critical sections in legacy applications on multicore architectures. The idea of RCL is to replace lock acquisitions by optimized remote procedure calls to a dedicated hardware thread, which is referred to as the server. RCL limits the performance collapse observed with other lock algorithms when many threads try to acquire a lock concurrently and removes the need to transfer lock-protected shared data to the hardware thread acquiring the lock because such data can typically remain in the server's cache. Other contributions presented in this thesis include a profiler that identifies the locks that are the bottlenecks in multithreaded applications and that can thus benefit from RCL, and a reengineering tool developed with Julia Lawall that transforms POSIX locks into RCL locks. Eighteen applications were used to evaluate RCL: the nine applications of the SPLASH-2 benchmark suite, the seven applications of the Phoenix 2 benchmark suite, Memcached, and Berkeley DB with a TPC-C client. Eight of these applications are unable to scale because of locks and benefit from RCL on an x86 machine with four AMD Opteron processors and 48 hardware threads. Using RCL locks, performance is improved by up to 2.5 times with respect to POSIX locks on Memcached, and up to 11.6 times with respect to Berkeley DB with the TPC-C client. On an SPARC machine with two Sun Ultrasparc T2+ processors and 128 hardware threads, three applications benefit from RCL. In particular, performance is improved by up to 1.3 times with respect to POSIX locks on Memcached, and up to 7.9 times with respect to Berkeley DB with the TPC-C client.

Cette thèse introduit deux outils pour l'accès performant aux données d'un algorithme à front d'onde dans un contexte d'exécution out-of-core. Ces algorithmes sont facilement parallélisables en utilisant des techniques de macro-pipelining, qui permettent un recouvrement des calculs et des communications. Le premier outil part du constat que les performances des opérations de lecture/écriture dans une telle situation sont désastreuses: les données sont éclatées sur disque et leur rapatriement en mémoire est long et coûteux. Le nouvel agencement de données sur disque proposé permet de résoudre ces problèmes en accédant aux données uniquement de manière contiguë. Si ce premier outil décrit comment accéder aux données, le deuxième est un modèle de synchronisation qui décrit quand y accéder. En effet, l'exécution parallèle et concurrente des algorithmes à front d'onde nécessite un contrôle strict des temps d'accès et des temps d'attente. Le modèle présenté dans cette thèse remplit ce rôle, tout en donnant des garanties de propriétés intéressantes pour les applications itératives: verrouillage pro-actif, évolution sans interblocages, progression homogène des tâches. L'utilisation de ces deux outils a été intensivement testée sur un benchmark de référence et expérimentée sur des machines de la plate-forme Grid'5000.

Aujourd’hui, le traitement de grands jeux de données est généralement parallélisé et effectué sur des machines multi-cœurs. Cependant, les verrous peuvent sérialiser l'exécution de ces coeurs et dégrader la latence et le débit du traitement. Détecter ces problèmes de contention de verrous in-vitro (i.e. pendant le développement du logiciel) est complexe car il est difficile de reproduire un environnement de production, de créer une charge de travail réaliste représentative du contexte d’utilisation du logiciel et de tester toutes les configurations de déploiement possibles où s'exécutera le logiciel. Cette thèse présente Free Lunch, un profiler permettant d'identifier les phases de contention dues aux verrous in-vivo (i.e. en production). Free Lunch intègre une nouvelle métrique appelée Critical Section Pressure (CSP) évaluant avec précision l'impact de la synchronisation sur le progrès des threads. Free Lunch est directement intégré dans la JVM Hotspot pour minimiser le surcoût d'exécution et reporte régulièrement la CSP afin de pouvoir détecter les problèmes transitoires dus aux verrous. Free Lunch est évalué sur 31 benchmarks issus de Dacapo 9.12, SpecJVM08 et SpecJBB2005, ainsi que sur la base de données Cassandra. Nous avons identifié des phases de contention dans 6 applications dont certaines n'étaient pas détectées par les profilers actuels. Grâce à ces informations, nous avons amélioré la performance de Xalan de 15% en modifiant une seule ligne de code et identifié une phase de haute contention dans Cassandra. Free Lunch n’a jamais dégradé les performances de plus de 6% ce qui le rend approprié pour être déployé continuellement dans un environnement de production. / Today, the processing of large dataset is generally parallelised and performed on computers with many cores. However, locks can serialize the execution of these cores and hurt the latency and the processing throughput. Spotting theses lock contention issues in-vitro (i.e. during the development phase) is complex because it is difficult to reproduce a production environment, to create a realistic workload representative of the context of use of the software and to test every possible configuration of deployment where will be executed the software. This thesis introduces Free Lunch, a lock profiler that diagnoses phases of high lock contention due to locks in-vivo (i.e. during the operational phase). Free Lunch is designed around a new metric, the Critical Section Pressure (CSP), which aims to evaluate the impact of lock contention on overall thread progress. Free Lunch is integrated in Hotpost in order to minimize the overhead and regularly reports the CSP during the execution in order to detect temporary issues due to locks. Free Lunch is evaluated over 31 benchmarks from Dacapo 9.12, SpecJVM08 and SpecJBB2005, and over the Cassandra database. We were able to pinpoint the phases of lock contention in 6 applications for which some of these were not detected by existing profilers. With this information, we have improved the performance of Xalan by 15% just by rewriting one line of code and identified a phase of high lock contention in Cassandra during the replay of transactions after a crash of a node. Free Lunch has never degraded performance by more than 6%, which makes it suitable to be deployed continuously in an operational environment.

Une multitude d'algorithmes d'exclusion mutuelle ont été conçus au cours des vingt cinq dernières années, dans le but d'améliorer les performances liées à l'exécution de sections critiques et aux verrous.Malheureusement, il n'existe actuellement pas d'étude générale et complète au sujet du comportement de ces algorithmes d'exclusion mutuelle sur des applications réalistes (par opposition à des applications synthétiques) qui considère plusieurs métriques de performances, telles que l'efficacité énergétique ou la latence.Dans cette thèse, nous effectuons une analyse pragmatique des mécanismes d'exclusion mutuelle, dans le but de proposer aux développeurs logiciels assez d'informations pour leur permettre de concevoir et/ou d'utiliser des mécanismes rapides, qui passent à l'échelle et efficaces énergétiquement.Premièrement, nous effectuons une étude de performances de 28 algorithmes d'exclusion mutuelle faisant partie de l'état de l'art, en considérant 40 applications et quatre machines multicœurs différentes.Nous considérons non seulement le débit (la métrique de performance traditionnellement considérée), mais aussi l'efficacité énergétique et la latence, deux facteurs qui deviennent de plus en plus importants.Deuxièmement, nous présentons une analyse en profondeur de nos résultats.Plus particulièrement, nous décrivons neufs problèmes de performance liés aux verrous et proposons six recommandations aidant les développeurs logiciels dans le choix d'un algorithme d'exclusion mutuelle, se basant sur les caractéristiques de leur application ainsi que les propriétés des différents algorithmes.A partir de notre analyse détaillée, nous faisons plusieurs observations relatives à l'interaction des verrous et des applications, dont plusieurs d'entre elles sont à notre connaissance originales:(i) les applications sollicitent fortement les primitives lock/unlock mais aussi l'ensemble des primitives de synchronisation liées à l'exclusion mutuelle (ex. trylocks, variables de conditions),(ii) l'empreinte mémoire d'un verrou peut directement impacter les performances de l'application,(iii) pour beaucoup d'applications, l'interaction entre les verrous et l'ordonnanceur du système d'exploitation est un facteur primordial de performance,(iv) la latence d'acquisition d'un verrou a un impact très variable sur la latence d'une application,(v) aucun verrou n'est systématiquement le meilleur,(vi) choisir le meilleur verrou est difficile, et(vii) l'efficacité énergétique et le débit vont de pair dans le contexte des algorithmes d'exclusion mutuelle.Ces découvertes mettent en avant le fait que la synchronisation à base de verrou ne se résume pas seulement à la simple interface "lock - unlock".En conséquence, ces résultats appellent à plus de recherche dans le but de concevoir des algorithmes d'exclusion mutuelle avec une empreinte mémoire faible, adaptatifs et qui implémentent l'ensemble des primitives de synchronisation liées à l'exclusion mutuelle.De plus, ces algorithmes ne doivent pas seulement avoir de bonnes performances d'un point de vue du débit, mais aussi considérer la latence ainsi que l'efficacité énergétique. / A plethora of optimized mutual exclusion lock algorithms have been designed over the past 25 years to mitigate performance bottlenecks related to critical sections and synchronization.Unfortunately, there is currently no broad study of the behavior of these optimized lock algorithms on realistic applications that consider different performance metrics, such as energy efficiency and tail latency.In this thesis, we perform a thorough and practical analysis, with the goal of providing software developers with enough information to achieve fast, scalable and energy-efficient synchronization in their systems.First, we provide a performance study of 28 state-of-the-art mutex lock algorithms, on 40 applications, and four different multicore machines.We not only consider throughput (traditionally the main performance metric), but also energy efficiency and tail latency, which are becoming increasingly important.Second, we present an in-depth analysis in which we summarize our findings for all the studied applications.In particular, we describe nine different lock-related performance bottlenecks, and propose six guidelines helping software developers with their choice of a lock algorithm according to the different lock properties and the application characteristics.From our detailed analysis, we make a number of observations regarding locking algorithms and application behaviors, several of which have not been previously discovered:(i) applications not only stress the lock/unlock interface, but also the full locking API (e.g., trylocks, condition variables),(ii) the memory footprint of a lock can directly affect the application performance,(iii) for many applications, the interaction between locks and scheduling is an important application performance factor,(iv) lock tail latencies may or may not affect application tail latency,(v) no single lock is systematically the best,(vi) choosing the best lock is difficult (as it depends on many factors such as the workload and the machine), and(vii) energy efficiency and throughput go hand in hand in the context of lock algorithms.These findings highlight that locking involves more considerations than the simple "lock - unlock" interface and call for further research on designing low-memory footprint adaptive locks that fully and efficiently support the full lock interface, and consider all performance metrics.

Le sujet central de cette thèse est le développement d'une méthode dédiée à la preuve de structures de données sans verrou. La motivation première vient du constat que les programmes concurrents sont devenu monnaie courante. Ceci a été possible par l'apparition de nouvelles primitives de synchronisation dans les nouvelles architectures matérielles. La seconde motivation est la quête de logiciel prouvé et donc correct. La sûreté des logiciels est en effet devenue primordiale de par la diffusion des systèmes embarqués et enfouis. La méthode proposée est basée sur le raffinement et dédiée à la conception et la vérification d'algorithme non-bloquant, en particulier ceux sans verrou. La méthode a été formalisée et sa correction prouvée en Isabelle/HOL. Un outil a par ailleurs été développé afin de générer des obligations de preuves à destination des solveurs SMT et des prouveurs de théorèmes du premier ordre. Nous l'avons utilisé afin de vérifier certains de ces algorithmes.

La mémoire transactionnelle est un mécanisme de plus en plus populaire pour la programmation parallèle et concurrente. Dans la plupart des implantations, l’emboîtement de transactions n’est pas possible ce qui pénalise la modularité. Plutôt que les transactions, qui sont un choix possible d’implantation, nous considérons directement la notion de section atomique. Dans un objectif d’améliorer la modularité et l’expressivité, nous considérons un langage impératif simple étendu avec des instructions de parallélisme avec lancement et attente de processus légers et une instruction de section atomique à portée syntaxique, depuis laquelle des processus légers peuvent s’échapper. Dans ce contexte notre première contribution est la définition précise de l’atomicité et de la bonne synchronisation. Nous prouvons que pour des traces bien formées, la dernière implique la forme forte de la première. Ceci est fait sur des traces d’exécution abstraites dans le sens où nous ne définissons par précisément la syntaxe et la sémantique opérationnelle d’un langage de programmation. Cette première partie de notre travail peut être considérée comme une spécification pour un tel langage. Nous avons utilisé l’assistant de preuve Coq pour modéliser et prouver nos résultats. Notre deuxième contribution est la définition formelle du langage Atomic Fork Join (AFJ). Nous montrons que les traces de sa sémantique opérationnelle vérifient effectivement les conditions de bonne formation définies précédemment. La troisième contribution est la compilation de programmes AFJ en programmes Lock Unlock Fork Join (LUFJ) un langage avec processus léger et verrous mais sans sections atomiques. Nous étudions la correction de la compilation de AFJ vers LUFJ. / Transactions are becoming a popular mechanism for parallel and concurrent programming. In most implementations the nesting of transactions is not supported which hinders modularity. Rather than transactions, which are an implementation choice, we consider directly the notion of atomic section. For the sake of modularity with we consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our first contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. This is done on execution traces without being specific to a language syntax and operational semantics. This first part of our work could be considered as a specification for the design and implementation of such a parallel language. A formalisation of our results in the Coq proof assistant is also available. Our second contribution is a formal definition of the Atomic Fork Join (AFJ) language and its operational semantics. We show that it indeed satisfies the conditions previously defined. The third contribution of our work is a compilation procedure of AFJ programs to programs another language with threads and locks but without atomic sections, named Lock Unlock Fork Join (LUFJ). We study the correctness of the compilation from AFJ to LUFJ.