Modern compilers are complex programs, performing several heuristic-based optimisations. As such, and despite extensive testing, they may contain bugs leading to the introduction of new behaviours in the compiled program.To address this issue, we are nowadays able to prove correct, in proof assistants such as Coq, optimising compilers for languages such as C or ML. To date, a similar result for high-level languages such as Java nonetheless remain out of reach. Such languages indeed possess two essential characteristics: concurrency and a particularly complex runtime.This thesis aims at reducing the gap toward the implementation of such a verified compiler. To do so, we focus more specifically on a state-of-the-art concurrent garbage collector. This component of the runtime takes care of automatically reclaiming memory during the execution to remove this burden from the developer side. In order to keep the induced overhead as low as possible, the garbage collector needs to be extremely efficient. More specifically, the algorithm considered is said to be “on the fly”: by relying on fine-grained concurrency, the user-threads are never caused to actively wait. The key property we establish is the functional correctness of this garbage collector, i.e. that a cell that a user thread may still access is never reclaimed.We present in a first phase the algorithm considered and its formalisation in Coq by implementing it in a dedicated intermediate representation. We introduce the proof system we used to conduct the proof, a variant based on the well-established Rely-Guarantee logic, and prove the algorithm correct.Reasoning simultaneously over both the garbage collection algorithm itself and the implementation of the concurrent data-structures it uses would entail an undesired additional complexity. The proof is therefore conducted with respect to abstract operations: they take place instantaneously. To justify this simplification, we introduce in a second phase a methodology inspired by the work of Vafeiadis and dedicated to the proof of observational refinement for so-called “linearisable” concurrent data-structures. We provide the approach with solid semantic foundations, formalised in Coq. This methodology is instantiated to soundly implement the main data-structure used in our garbage collector.

Les compilateurs modernes constituent des programmes complexes, rĂ©alisant de nombreuses optimisations afin d’amĂ©liorer la performance du code gĂ©nĂ©rĂ©. Du fait de cette complexitĂ©, des bugs y sont rĂ©gulièrement dĂ©tectĂ©, conduisant Ă  l’introduction de nouveau comportement dans le programme compilĂ©. En rĂ©action, il est aujourd’hui possible de prouver correct, dans des assistants de preuve tels que Coq, des compilateurs optimisants pour des langages tels que le C ou ML. Transporter un tel rĂ©sultat pour des langages haut-niveau tels que Java est nĂ©anmoins encore hors de portĂ©e de l’Ă©tat de l’art. Ceux-ci possèdent en effet deux caractĂ©ristiques essentielles: la concurrence et un environnement d’exĂ©cution particulièrement complexe.Nous proposons dans cette thèse de rĂ©duire la distance vers la conception d’un tel compilateur vĂ©rifiĂ© en nous concentrant plus spĂ©cifiquement sur la preuve de correction d’un glaneur de cellules concurrent performant. Ce composant de l’environnement d’exĂ©cution prend soin de collecter de manière automatique la mĂ©moire, en lieu et place du programmeur. Afin de ne pas gĂ©nĂ©rer un ralentissement trop Ă©levĂ© Ă  l’exĂ©cution, le glaneur de cellules doit ĂŞtre extrĂŞmement performant. Plus spĂ©cifiquement, l’algorithme considĂ©rĂ© est dit «au vol»: grâce Ă  l’usage de concurrence très fine, il ne cause jamais d’attente active au sein d’un fil utilisateur. La preuve de correction Ă©tablit par consĂ©quent que malgrĂ© l’intrication complexe des fils utilisateurs et du collecteur, ce dernier ne collecte jamais une cellule encore accessible par les premiers. Nous prĂ©sentons dans un premier temps l’algorithme considĂ©rĂ© et sa formalisation en Coq dans une reprĂ©sentation intermĂ©diaire conçue pour l’occasion. Nous introduisons le système de preuve que nous avons employĂ©, une variante issue de la logique «Rely-Guarantee», et prouvons l’algorithme correct. Raisonner simultanĂ©ment sur l’algorithme de collection et sur l’implantation des structures de donnĂ©es concurrentes manipulĂ©es gĂ©nĂ©rerait une complexitĂ© additionnelle indĂ©sirable. Nous considĂ©rons donc durant la preuve des opĂ©rations abstraites: elles ont lieu instantanĂ©ment. Pour lĂ©gitimer cette simplification, nous introduisons une mĂ©thode inspirĂ©e par les travaux de Vafeiadis et permettant la preuve de raffinement de structures de donnĂ©es concurrentes dites «linĂ©arisables». Nous formalisons l’approche en Coq et la dotons de solides fondations sĂ©mantiques. Cette mĂ©thode est finalement instanciĂ©e sur la principale structure de donnĂ©es utilisĂ©e par le glaneur de cellules.