Title: A Formal Semantics For Weak Refenences

Presented by Joe Hallett

Abstract:
Generally speaking, a weak reference is a reference to an object that is
not followed by the garbage collector.  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, there 
have been few attempts to treat their semantics formally at all).  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 $\weak$ that includes
weak references and is derived from Morrisett, Harper, and Felleisen's
$\gc$.  $\gc$ 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 prevents the 
confluence of the rewrite system.  As a result, we discuss methods in 
which we can recover unique results from the evaluation of our programs.
We define conditions that allow other garbage collection algorithms 
to co-exists with our semantics of weak references.  We also introduce a 
type system and a corresponding type inference algorithm.  We prove the
type system sound and the inference algorithm sound and complete.

References:
1.	Abstract Models of Memory Management
    	by Greg Morrisett and Matthias Felleisen and Robert Harper
	Conference on Functional Programming Languages and Computer Architecture 1995
	http://www.eecs.harvard.edu/~greg/papers/index.html

2.	Stretching the storage manager: weak pointers and stable names in Haskell	
	by Simon Peyton Jones and Simon Marlow and Conal Elliott
	Proceedings of the Workshop on Implementing Functional Languages 1999
	http://research.microsoft.com/Users/simonpj/Papers/weak.htm