DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma;
	h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc
	:content-transfer-encoding:message-id:references:to:x-mailer;
	b=jIFhUlj5SV6pDlNRbr1cmlyicODJ5GWnMHNds8aaRFywgJfMeoN1uAkZom4fdJDLKY
	1aJlfdgAGY/c9KtVzAE2cPFaqHNR9ZD63Y+0c7CZsneM9RRZCWaAx9FFMuxwKKyfciWD
	yku/W7AJWIZ3Y3Drr9NXNzl1J1Dx1EBmdzHbU=
Subject: Re: [Lablgtk] Double free problem using bytecode
Mime-Version: 1.0 (Apple Message framework v1081)
Content-Type: text/plain; charset=iso-8859-1
From: Jacques Garrigue <garrigue at math.nagoya-u.ac.jp>
In-Reply-To: <20101104113045.GA21006 at pirogue.inria.fr>
Date: Fri, 5 Nov 2010 10:53:53 +0900
Content-Transfer-Encoding: quoted-printable
Message-Id: <1B29F5FF-767D-422B-A5D6-0ED2FFCE6A67 at gmail.com>
References: <20101104113045.GA21006 at pirogue.inria.fr>
To: Hugo Herbelin <Hugo.Herbelin at inria.fr>
Cc: lablgtk at yquem.inria.fr, coqdev at inria.fr
Status: U

This problem is quite mysterious, and it might be a bug in ocaml itself.
Since I cannot debug it myself, I can only tell you how lablgtk uses =
threads.

Basically, lablgtk only allows ocaml threads to run, and does not use =
them
for itself. That is, when you use GtkThread.main, you replace the =
standard
main loop of Gtk by a custom loop which, at every iteration, (1) allows =
other
threads to run (Thread.delay 0.0001), and (2) runs the calls queued by
sync/async. Lablgtk itself never release ocaml's lock using =
caml_enter_blocking_section,
or run other threads explicitly.
So I don't see how it can break anything about threads.

Now, if you use sync/async, Gtk will always be called from the same =
thread,
so that callbacks also will always come from the same thread. This may
explain why this is more robust, but normally this should not be =
required
on Unix (Gtk does not require it). Except if there is a restriction I =
don't understand
on bytecode threads. Maybe we should ask thread specialists about that.

	Jacques

On 2010/11/04, at 20:30, Hugo Herbelin wrote:

> Hi,
>=20
> 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].
>=20
> 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?
>=20
> Strangely, the problem is also solved by enforcing some dummy printing
> on stderr from time to time.
>=20
> 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).
>=20
> Does anyone has an idea of what happens and of why using sync/async
> solves the problem?
>=20
> Hugo Herbelin and St=E9phane Glondu
> with the additional help of Vincent Gross
>=20
> [1] http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=3D2062
>=20
> ----------------------------------------------------------------------
> valgrind trace
>=20
> =3D=3D755=3D=3D Command: bin/coqide.byte
> =3D=3D755=3D=3D
> =3D=3D755=3D=3D Thread 3:
> =3D=3D755=3D=3D Invalid free() / delete / delete[]
> =3D=3D755=3D=3D    at 0x4C240FD: free (vg_replace_malloc.c:366)
> =3D=3D755=3D=3D  Address 0x10c3dff0 is 0 bytes inside a block of size =
8,192 free'd
> =3D=3D755=3D=3D    at 0x4C240FD: free (vg_replace_malloc.c:366)
> =3D=3D755=3D=3D    by 0x40AEF1: caml_stat_free (in =
/usr/local/bin/ocamlrun)
> =3D=3D755=3D=3D    by 0x40AD1C: caml_realloc_stack (in =
/usr/local/bin/ocamlrun)
> =3D=3D755=3D=3D    by 0x41B0BD: caml_interprete (in =
/usr/local/bin/ocamlrun)
> =3D=3D755=3D=3D    by 0x41706C: caml_callbackN_exn (in =
/usr/local/bin/ocamlrun)
> =3D=3D755=3D=3D    by 0x417164: caml_callback_exn (in =
/usr/local/bin/ocamlrun)
> =3D=3D755=3D=3D    by 0x69570A8: caml_thread_start (in =
/usr/local/lib/ocaml/stublibs/dllthreads.so)
>=20
> _______________________________________________
> Lablgtk mailing list
> Lablgtk@yquem.inria.fr
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/lablgtk

_______________________________________________
Lablgtk mailing list
Lablgtk@yquem.inria.fr
http://yquem.inria.fr/cgi-bin/mailman/listinfo/lablgtk