[Haskell-cafe] safe code to run in finalizers: ACIO revisited

[Robert Dockins]

On Sat, 2004-12-18 at 21:19 +0100, Marcin 'Qrczak' Kowalczyk wrote:
> Robert Dockins <robdockins at fastmail.fm> writes:
> 
> > So, to be safe, the action of a finalizer must commute with every
> > other finalizer (they must be central).
> 
> What does "should" mean? 

I am suggesting that being "affine central" is a sufficent condition for
being safe to run in a finalizer.

It is likely that a weaker condition would also be sufficent.  Trying to
characterize this weaker condition seems important; unfortunatly,
specifying exactily what actions are safe inside a finalizer would
probably require analyzing the exact formal semantics of finalizers in
Haskell.  This sounds pretty complicated (especially given concurrency).
I am not sure I have the skills, and I am not completely certain that
the formal semantics of haskell finalizers has ever been spelled out.
(anyone know?)

> There are useful finalizers which don't have
> this property.

Some of them are broken, but happen to mostly work.  In my mind "mostly
works" is the same as "contins hard to find bugs."

>  E.g. a finalizer can remove an entry from a weak
> dictionary, 

Interacting with weak pointers is one of those areas where I think you
might be able to get away with something weaker than "affine central".
I also think that some patterns of interacting with MVars are OK as
well. 'tryPutMVar' seems pretty safe, as does 'modifyMVar'.

> call a C function which will free some foreign object,

I think we can safely consider foreign calls which only release memory
affine central.

> or send a message over a network that a particular object is no longer
> needed. 

Sending a network packet inside a finalizer sounds like a bad idea to
me.  I think that's exactily the kind of thing we want to keep people
from doing.  I would rather see a long running thread that is woken up
by a finalizer that performs such actions.  This has the advantage of
allowing you to explicitly tell the thread to release all resources at
program end.  

Even better, make sure to use bracket style allocations and avoid
finalizers altogether (this seems like a must to me for remote or
hardware resources).

> > So a separate ACIO monad for affine central IO actions would be the
> > appropriate context for finalizers.
> 
> It would not be enough without unsafeIOtoACIO.

Fair enough.  That at least flags the user that they have incurred a
proof obligation.