School of Computing

Birrell's distributed reference listing revisited

Luc Moreau, Peter Dickman, and Richard Jones

Technical Report 8-03, University of Kent, Computing Laboratory, Canterbury, July 2003.


The Java RMI collector is arguably the most widely used distributed garbage collector. Its distributed reference listing algorithm was introduced by Birrell in the context of Network Objects, where the description was informal and heavily biased toward implementation. In this paper, we formalise this algorithm in an implementation-independent manner, which allows us to clarify weaknesses of the initial presentation. In particular, we discover cases critical to the correctness of the algorithm that are not accounted for by Birrell. We use our formalisation to derive an invariant-based proof of correctness of the algorithm that avoids notoriously difficult temporal reasoning. Furthermore, we offer a novel graphical representation of the state transition diagram, which we use to provide intuitive explanations of the algorithm and to investigate its tolerance to faults in a systematic manner. Finally, we examine how the algorithm may be optimised, either by placing constraints on message channels or by tightening the coupling between application program and distributed garbage collector.

Download publication 553 kbytes (PDF)

Bibtex Record

author = {Luc Moreau and Peter Dickman and Richard Jones},
title = {Birrell's Distributed Reference Listing Revisited},
month = {July},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    publication_type = {techreport},
    submission_id = {14448_1057852099},
    type = {Technical Report},
    number = {8--03},
    address = {Canterbury},
    institution = {University of Kent, Computing Laboratory},

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014