Hi,

we've recently run into a class of bugs concerning finalization
functions with custom blocks that is probably not uncommon in OCaml
bindings (e.g. Postgresql-bindings, SSL-bindings, likely others).  It
seems somewhat unintuitive, but finalizers registered from within C do
_not_ behave the same as ones registered from OCaml-code with the
Gc-module.

The OCaml manual explicitly states that custom functions registered
from within C are not allowed to allocate values, perform callbacks,
(de)register roots (I guess global roots, too?), or (as is obviously
also true) release/acquire the OCaml-runtime lock.  Developers
probably often miss this information.  The consequences of bugs
violating any of these constraints are usually rare and hard to
understand segfaults.

This means that people will have to register finalizers from within
OCaml for such values, which is certainly rather inconvenient.  As a
general rule, it seems advisable to never use finalizers that need to
release the runtime lock, e.g. if finalization code can block.  The
reason is that finalizers can be run from any thread, including ones
that should not block for an indefinite amount of time.  This implies
that people who have designed APIs using finalization that way should
consider redesigning it such that users have to "clean up" manually,
thus forcing them to think about when and in which thread this
happens.

Otherwise, it might be helpful if the OCaml-team could consider
whether this situation can be improved.  For example not being allowed
to register/unregister roots to values seems overly restrictive, since
global roots (e.g. for protecting OCaml-callback closures) sometimes
need to be associated with C-values (e.g. for allowing some external
C-library to efficiently perform callbacks into OCaml).  Registering
the finalizer from within C during allocation rather than having to
wrap up the value a second time with an OCaml-finalizer would seem
much simpler.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com