|
Kevin Donnelly, Joseph J. Hallett, and Assaf J. Kfoury
Formal semantics for weak
references
Technical Report Don+Hal+Kfo:BUCS-TR-2005-X, Department of Computer
Science, Boston University, July 2005
Weak references are references that do not prevent
the object they point to from being garbage
collected. Many realistic languages, including Java,
SML/NJ, and Haskell to name a few, support weak
references. However, there is no generally accepted
formal semantics for weak references. Without such a
formal semantics it becomes impossible to formally
prove properties of such a language and the programs
written in it.
We give a formal semantics for a calculus called
lambda-weak that includes weak references and is
derived from Morrisett, Felleisen, and Harper's
lambda-gc. The semantics is used to examine several
issues involving weak references. We use the
framework to formalize the semantics for the
key/value weak references found in
Haskell. Furthermore, we consider a type system for
the language and show how to extend the earlier
result that type inference can be used to collect
reachable garbage. In addition we show how to allow
collection of weakly referenced garbage without
incurring the computational overhead often
associated with collecting a weak reference which
may be later used. Lastly, we address the
non-determinism of the semantics by providing both
an effectively decidable syntactic restriction and a
more general semantic criterion, which guarantee a
unique result of evaluation.
[ bib |
.ps.gz |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
