© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Birrell's distributed reference listing revisited
Luc Moreau, Peter Dickman, and Richard Jones
ACM Transactions on Programming Languages and Systems (TOPLAS), 27(6):182-196, November 2005.Abstract
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
@article{1993,
author = {Luc Moreau and Peter Dickman and Richard Jones},
title = {Birrell's Distributed Reference Listing Revisited},
month = {November},
year = {2005},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2005/1993},
ISSN = {0164-0925},
publication_type = {article},
submission_id = {940_1098458446},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
publisher = {ACM},
volume = {27},
number = {6},
}