|
Joseph J. Hallett and Assaf J. Kfoury
A formal semantics for weak
references
Technical Report Hal+Kfo:BUCS-TR-2005-031, Department of Computer
Science, Boston University, May 2005
A weak reference is a reference to an object that is not
followed by the pointer tracer when garbage collection is called. That is,
a weak reference cannot prevent
the object it references from being garbage collected. Weak references
remain a troublesome programming feature largely because there is not an
accepted, precise semantics that describes their behavior (in fact, we
are not aware of any formalization of their semantics). The
trouble is that weak references allow reachable objects to be garbage
collected, therefore allowing garbage collection to influence the
result of a program. Despite this difficulty, weak references continue to be
used in practice for reasons related to efficient storage management, and
are included in many popular programming languages (Standard ML, Haskell,
OCaml, and Java).
We give a formal semantics for a calculus called that includes
weak references and is derived from Morrisett, Felleisen, and Harper's
. formalizes the notion of garbage collection by means of a
rewrite rule. Such a formalization is required to precisely characterize
the semantics of weak references. However, the inclusion of a
garbage-collection rewrite-rule in a language with weak references
introduces non-deterministic evaluation, even if the parameter-passing
mechanism is deterministic (call-by-value in our case). This raises the
question of confluence for our rewrite system. We discuss
natural restrictions under which our rewrite system is confluent,
thus guaranteeing uniqueness of program result. We define conditions
that allow other garbage collection algorithms to co-exist with our
semantics of weak references. We also introduce a polymorphic type system
to prove the absence of erroneous program behavior (i.e., the absence of
“stuck evaluation'') and a corresponding type inference algorithm. We
prove the type system sound and the inference algorithm sound and complete.
[ 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.
|
