Design, implementation and certification of a concurrent garbage collector
Conception, réalisation et certification d'un glaneur de cellules concurrent
Résumé
Manual memory management is an endless source of errors that are easy to make and hard to debug. Automatic memory management frees the programmer from these errors, and all modern high-level languages are designed to use it. In the case of a multicore processor, memory management becomes even harder, which makes automatic memory management and garbage collection (GC) even more useful.
This dissertation describes the design, proof of correctness, and implementation of a GC for a high-level language featuring multi-thread execution with shared memory parallelism. This is a concurrent GC that strives to minimize the use of expensive synchronization primitives. As for any parallel algorithm, it is hard to trust it without a formal proof of correctness. We give such a proof here, using the TLA framework.
We also give an generational GC extension of this algorithm, which gives an important performance boost. This extension makes orignal use of the strong static typing of the ML language in order to cooperate with the GC. This generational GC could also be adapted to other parallel or concurrent garbage collectors.
La gestion manuelle de la mémoire est une source inépuisable d'erreurs faciles à commettre et difficiles à repérer. La gestion automatique de la mémoire libère le programmeur de ces erreurs, et un langage de haut niveau ne se conçoit plus sans gestion automatique de la mémoire.
Dans le cas d'une machine parallèle, la gestion de la mémoire devient un problème délicat. Cette difficulté augmente encore l'intérêt d'un
gestionnaire de mémoire automatique (GC).
Cette thèse est consacrée à la conception, la preuve et l'implémentation d'un GC destiné à être utilisé avec des programmes écrits dans un langage de haut niveau autorisant l'exécution parallèle avec un modèle à mémoire partagée. C'est un GC concurrent qui utilise au minimum les primitives de synchronisation coûteuses. Comme pour tout algorithme parallèle, il est difficile d'avoir confiance dans cet algorithme si on ne dispose pas d'une preuve formelle de sa correction. Nous donnons une telle preuve, en utilisant le formalisme TLA.
Nous donnons aussi une extension de cet algorithme par un système de générations, qui permet d'obtenir des performances très satisfaisantes.
Cette extension utilise de façon originale le typage statique fort du langage ML pour faire coopérer le programme avec le GC. Cette extension pourrait aussi s'adapter à d'autres GC concurrents ou parallèles.
Origine : Fichiers produits par l'(les) auteur(s)