HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Conception, réalisation et certification d'un glaneur de cellules concurrent

Abstract : 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.
Complete list of metadata

Contributor : Damien Doligez Connect in order to contact the contributor
Submitted on : Thursday, March 18, 2021 - 2:08:48 PM
Last modification on : Thursday, February 3, 2022 - 11:18:12 AM
Long-term archiving on: : Monday, June 21, 2021 - 8:44:41 AM


Files produced by the author(s)


  • HAL Id : tel-03173357, version 1



Damien Doligez. Conception, réalisation et certification d'un glaneur de cellules concurrent. Langage de programmation [cs.PL]. Université Paris 7, 1995. Français. ⟨tel-03173357⟩



Record views


Files downloads