The Revenge of Finalizers

[George Russell]

Alastair Reid wrote:
> 
> > However in general I think we can hide some of the horribleness from
> > the user:
> 
> > modify2IORefs :: IORef a -> IORef b -> (a -> b -> (a,b,c)) -> IO c
> > [horrible code deleted]
> 
> And if they need to update 3 IORefs or a list of IORefs?
It would be a fairly trivial matter to generalise the code I posted to
such cases.  But in my own experience three-way or multi-way
synchronisations are only required very rarely.  I have yet to come across
a case where we needed them here at Bremen, and we do use concurrency an
awful lot.
> 
> Writing code like that yourself and getting it right and portable
> between compilers seems to be ludicrously hard.
> 
> I can't tell if that code is right (my gut says no). 
Well I'm afraid my gut disagrees.  Also I think I've adequately
addressed all the specific concerns raised so far.
> Worse though, I
> don't even know what semantic framework to use to reason about it if
> we want to be sure the code will work in the presence of strictness
> analyzers, eager evaluation, parallel evaluation, fully-lazy
> evaluation, etc.  Operational reasoning and reasoning by example
> struggle with such a task.
Well I don't think we have a theoretical semantic framework for reasoning
about most of the FFI, including especially unsafePerformIO.  However
the main assumption that is being made by the code I gave is that
the thunks containing the unsafePerformIO's do not get multiply evaluated.
I think this is a reasonable assumption to make.  I am not scared
by any of the buzzwords you give.  For example, a strictness analyzer
which wrongly attempted to evaluate the unsafePerformIO "inside the lock"
and got into trouble as a result would in my opinion only have itself to
blame.  The same would apply to eager evaluation.  For example, such
methods might also get into trouble with the perfectly reasonable code:

x <- takeMVar y
let
   z = seq x (error "Not to be evaluated")
putMVar y z

seq z

since it would presumably raise an error prematurely when the MVar was
empty.  This is of course without any use of unsafePerformIO; one would
expect eager evaluators/strictness evaluators to be especially careful
about going round unsafePerformIO, if they did it at all.  As for
parallel evaluation I just don't see the problem, provided precautions
are taken to make sure unsafePerformIO's are not multiply evaluated.
I don't know what "fully-lazy evaluation" is, and how it differs from the
normally lazy variety.