Double free problem using bytecode

Hi,

We use lablgtk for the CoqIDE interface to Coq and we have "double
free" problems on Linux with the bytecode version of the interface [1].

The problem is solved by ensuring that any call to gtk from the
non-main thread are made using the sync/async functions. Is this then
a discipline that is recommended not only for Windows but also for
bytecode on Unix?

Strangely, the problem is also solved by enforcing some dummy printing
on stderr from time to time.

Using valgrind, we could somehow trace the "double free" problem (see
bottom of message). It shows that what is asked twice to be released
is the pointer to the block used as a stack by the bytecode runtime,
namely caml_stack_low: at some time an extension of the stack is done,
a new bigger stack is allocated and the old caml_stack_low pointer is
released. However, it looks like the updating of the caml_stack_low
using the address of new stack gets broken when using gtk in threads
since a second request for releasing the (old) value of the
caml_stack_low pointer happens later on (unfortunately, but that may
be also a hint, valgrind has no information on the call stack of the
second call to free).

Does anyone has an idea of what happens and of why using sync/async
solves the problem?

Hugo Herbelin and Stéphane Glondu
with the additional help of Vincent Gross

[1] http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2062

----------------------------------------------------------------------
valgrind trace

==755== Command: bin/coqide.byte
==755==
==755== Thread 3:
==755== Invalid free() / delete / delete[]
==755==    at 0x4C240FD: free (vg_replace_malloc.c:366)
==755==  Address 0x10c3dff0 is 0 bytes inside a block of size 8,192 free'd
==755==    at 0x4C240FD: free (vg_replace_malloc.c:366)
==755==    by 0x40AEF1: caml_stat_free (in /usr/local/bin/ocamlrun)
==755==    by 0x40AD1C: caml_realloc_stack (in /usr/local/bin/ocamlrun)
==755==    by 0x41B0BD: caml_interprete (in /usr/local/bin/ocamlrun)
==755==    by 0x41706C: caml_callbackN_exn (in /usr/local/bin/ocamlrun)
==755==    by 0x417164: caml_callback_exn (in /usr/local/bin/ocamlrun)
==755==    by 0x69570A8: caml_thread_start (in /usr/local/lib/ocaml/stublibs/dllthreads.so)