A Separation Logic for Heap Space under Garbage Collection - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2022

A Separation Logic for Heap Space under Garbage Collection

Résumé

We present SL⋄, a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. A user of the logic works with space credits, a resource that is consumed when an object is allocated and produced when a group of objects is logically deallocated, that is, when the user is able to prove that it has become unreachable and therefore can be collected. To prove such a fact, the user maintains pointed-by assertions that record the immediate predecessors of every object. Our calculus, SpaceLang, has mutable state, shared-memory concurrency, and code pointers. We prove that SL⋄ is sound and present several simple examples of its use.
Fichier principal
Vignette du fichier
madiot-pottier-diamonds-2022.pdf (634.02 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03478162 , version 1 (13-12-2021)

Identifiants

Citer

Jean-Marie Madiot, François Pottier. A Separation Logic for Heap Space under Garbage Collection. Proceedings of the ACM on Programming Languages, 2022, ⟨10.1145/3498672⟩. ⟨hal-03478162⟩
50 Consultations
46 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More