A construction of distributed reference counting

Citation
L. Moreau et J. Duprat, A construction of distributed reference counting, ACT INFORM, 37(8), 2001, pp. 563-595
Citations number
41
Language
INGLESE
art.tipo
Article
Categorie Soggetti
Information Tecnology & Communication Systems
Journal title
ACTA INFORMATICA
ISSN journal
0001-5903 → ACNP
Volume
37
Issue
8
Year of publication
2001
Pages
563 - 595
Database
ISI
SICI code
0001-5903(200105)37:8<563:ACODRC>2.0.ZU;2-F
Abstract
Distributed reference counting is a general purpose technique, which may be used, e.g., to detect termination of distributed programs or to implement distributed garbage collection. We present a distributed reference counting algorithm and a mechanical proof of correctness carried out using the proo f assistant Cog. The algorithm is formalised by an abstract machine, and it s correctness has two different facets. The safety property ensures that if there exists a reference to a resource, then its reference counter will be strictly positive. Liveness guarantees that if all references to a resourc e are deleted, its reference counter will eventually become null.