[MLton] adding synchronous finalizers

[Stephen Weeks]

I recently read Hans Boehm's POPL 2003 paper "Destructors, Finalizers,
and Synchronization".

	http://citeseer.ist.psu.edu/640926.html
	http://www.hpl.hp.com/personal/Hans_Boehm/popl03/web/

It was an interesting paper, and it draws many of the same conclusions
about finalizers that we did when we built MLton.Finalizable.  A few
quotes from his conclusion:

   The language specification must provide the programmer with a way
   to ensure that objects remain reachable long enough to prevent
   premature finalization.

   Finalizers naturally constitute a separate asynchronous thread of
   control.

   Finalization effectively introduces an additional thread of
   control, and thus concurrency issues must be considered, even for
   otherwise single-threaded applications.

   It must be guaranteed that finalizers will run in a thread in which
   no locks are held.  Typically this means that either finalizers are
   run in their own thread(s), or that finalization-ready objects are
   enqueued and then run explicitly from programmer-initiated threads

   In purely single-threaded environments, the programmer must be
   given explicit control over when to run finalizers.  Typically this
   will be accomplished by explicitly enqueuing finalization-ready
   objects.

I think MLton.Finalizable does fine on all of these, except for
providing a way for single-threaded applications to use finalizers
synchronously.  I propose that we add something like the following to
MLton.Finalizable.

   val runSynchronously: bool ref
   val runFinalizers: unit -> unit

The idea is that if !runSynchronously = true, then after a gc, enabled
finalizers are queued instead of run.  It is then up to the programmer
to call runFinalizers at appropriate times.  We need a little bit of
synchronization to implement this, but all in all it should only be a
few lines of code.

Obviously, we don't want to force programmers to use synchronous
finalizers, but it does seem nice to let single-threaded programs that
want to use finalizers have a way to do so without worrying about
threads.  I think this is in fact what the mgtk guys do.