Delivered-To: garrigue at math.nagoya-u.ac.jp Delivered-To: lablgtk at yquem.inria.fr Date: Thu, 4 Nov 2010 12:30:45 +0100 From: Hugo Herbelin To: lablgtk at yquem.inria.fr Message-ID: <20101104113045.GA21006 at pirogue.inria.fr> Mail-Followup-To: lablgtk at yquem.inria.fr, coqdev at inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit Cc: coqdev at inria.fr Subject: [Lablgtk] Double free problem using bytecode Status: U 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) _______________________________________________ Lablgtk mailing list Lablgtk@yquem.inria.fr http://yquem.inria.fr/cgi-bin/mailman/listinfo/lablgtk