Skip to Main content Skip to Navigation
Theses

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

https://hal.inria.fr/tel-03173357
Contributor : Damien Doligez <>
Submitted on : Thursday, March 18, 2021 - 2:08:48 PM
Last modification on : Friday, March 19, 2021 - 3:29:59 AM

File

doligez-these.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-03173357, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

16

Files downloads

148