Skip to Main content Skip to Navigation
Theses

Verification of a Concurrent Garbage Collector

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

Cited literature [147 references]  Display  Hide  Download

https://hal.inria.fr/tel-01680213
Contributor : Abes Star :  Contact
Submitted on : Monday, March 12, 2018 - 5:56:08 PM
Last modification on : Wednesday, August 5, 2020 - 3:41:59 AM
Long-term archiving on: : Wednesday, June 13, 2018 - 2:32:44 PM

File

ThesisVFinale_ZAKOWSKI.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01680213, version 2

Citation

Yannick Zakowski. Verification of a Concurrent Garbage Collector. Data Structures and Algorithms [cs.DS]. École normale supérieure de Rennes, 2017. English. ⟨NNT : 2017ENSR0010⟩. ⟨tel-01680213v2⟩

Share

Metrics

Record views

733

Files downloads

2910