caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
@ 2016-04-29 11:04 Markus Weißmann
  2016-04-29 13:17 ` Gerd Stolpmann
  0 siblings, 1 reply; 10+ messages in thread
From: Markus Weißmann @ 2016-04-29 11:04 UTC (permalink / raw)
  To: caml-list

Hello,

I have a server program that crashes after some time with a very 
strange error:
The (=) comparison of two values returns false, even though they are 
pretty identical.
They are of type { a : int; b : int } and the comparison always fails 
on the second integer.
When printing the compared integers, they are always 0 (as expected) -- 
both of them; but are not equal (=).
I started inspecting the values with the "Obj.tag" and found them to be 
always of type Obj.int_tag -- until the non-equalness strikes:
One of the compared integers then always has Obj.out_of_heap_tag. This 
value surprisingly behaved like an integer unless compared to another:

let (x : int) =
   print_int x; (* "0" *)
   assert (x = 0) (* fails! *)

Can someone explain what this tag means exactly and if this 
works-as-intended or if my heap must have gotten hit by some faulty C 
bindings?
Is this some out-of-memory handling of the minor heap? If I set 
Gc.minor_heap_size to 4 MByte I don't get the Obj.out_of_heap_tag -- or 
at least haven't yet.

This is ocaml 4.02.3 on amd64.

Regards
Markus

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/


^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 11:04 [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption? Markus Weißmann
@ 2016-04-29 13:17 ` Gerd Stolpmann
  2016-04-29 14:14   ` Markus Weißmann
  0 siblings, 1 reply; 10+ messages in thread
From: Gerd Stolpmann @ 2016-04-29 13:17 UTC (permalink / raw)
  To: Markus Weißmann; +Cc: caml-list

[-- Attachment #1: Type: text/plain, Size: 2348 bytes --]

Am Freitag, den 29.04.2016, 13:04 +0200 schrieb Markus Weißmann:
> Hello,
> 
> I have a server program that crashes after some time with a very 
> strange error:
> The (=) comparison of two values returns false, even though they are 
> pretty identical.
> They are of type { a : int; b : int } and the comparison always fails 
> on the second integer.
> When printing the compared integers, they are always 0 (as expected) -- 
> both of them; but are not equal (=).
> I started inspecting the values with the "Obj.tag" and found them to be 
> always of type Obj.int_tag -- until the non-equalness strikes:
> One of the compared integers then always has Obj.out_of_heap_tag. This 
> value surprisingly behaved like an integer unless compared to another:
> 
> let (x : int) =
>    print_int x; (* "0" *)
>    assert (x = 0) (* fails! *)
> 
> Can someone explain what this tag means exactly and if this 
> works-as-intended or if my heap must have gotten hit by some faulty C 
> bindings?

Obj.tag is meaningless for ints.

What could have happened is that a C lib did not set the LSB of the word
(which is required for ints in order to make them distinguishable from
pointers). The C lib MUST use Val_int or Val_long to create the values
(and these macros set the LSB).

Check whether Obj.is_int returns true. If not, something is wrong.

Actually, I wonder what Obj.int_tag=1000 is for. It's not something that
can really occur, because tags are 8 bits wide. Maybe it's a replacement
when Obj.tag is called for non-blocks?

Gerd


> Is this some out-of-memory handling of the minor heap? If I set 
> Gc.minor_heap_size to 4 MByte I don't get the Obj.out_of_heap_tag -- or 
> at least haven't yet.
> 
> This is ocaml 4.02.3 on amd64.
> 
> Regards
> Markus
> 
> -- 
> Markus Weißmann, M.Sc.
> Technische Universität München
> Institut für Informatik
> Boltzmannstr. 3
> D-85748 Garching
> Germany
> http://wwwknoll.in.tum.de/
> 
> 

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 13:17 ` Gerd Stolpmann
@ 2016-04-29 14:14   ` Markus Weißmann
  2016-04-29 14:25     ` Gerd Stolpmann
  2016-04-29 14:57     ` Mark Shinwell
  0 siblings, 2 replies; 10+ messages in thread
From: Markus Weißmann @ 2016-04-29 14:14 UTC (permalink / raw)
  To: caml-list; +Cc: Gerd Stolpmann

On 2016-04-29 15:17, Gerd Stolpmann wrote:
> Am Freitag, den 29.04.2016, 13:04 +0200 schrieb Markus Weißmann:
>> Hello,
>>
>> I have a server program that crashes after some time with a very
>> strange error:
>> The (=) comparison of two values returns false, even though they are
>> pretty identical.
>> They are of type { a : int; b : int } and the comparison always 
>> fails
>> on the second integer.
>> When printing the compared integers, they are always 0 (as expected) 
>> --
>> both of them; but are not equal (=).
>> I started inspecting the values with the "Obj.tag" and found them to 
>> be
>> always of type Obj.int_tag -- until the non-equalness strikes:
>> One of the compared integers then always has Obj.out_of_heap_tag. 
>> This
>> value surprisingly behaved like an integer unless compared to 
>> another:
>>
>> let (x : int) =
>>    print_int x; (* "0" *)
>>    assert (x = 0) (* fails! *)
>>
>> Can someone explain what this tag means exactly and if this
>> works-as-intended or if my heap must have gotten hit by some faulty 
>> C
>> bindings?
>
> Obj.tag is meaningless for ints.
>
> What could have happened is that a C lib did not set the LSB of the 
> word
> (which is required for ints in order to make them distinguishable 
> from
> pointers). The C lib MUST use Val_int or Val_long to create the 
> values
> (and these macros set the LSB).
>
> Check whether Obj.is_int returns true. If not, something is wrong.
>

The value comes from C bindings, but from a string-value via Char.code.
It is then passed through a constructor-function to create the record;
I added a check there to see if the C bindings are to blame:

   type foo = { a : int; b : int }

   let create (a : int) (b : int) =
     assert (Obj.is_int (Obj.repr x)); (* always holds *)
     { a; b }

This assertion never triggered so far.
I replaced the equality check by a function which now also asserts the
is_int property:

   let equal (x : foo) (y : foo) = (* y is a static value living through 
the entire run; x is from a parse/allocate/compare/throw-away cycle *)
     assert (Obj.is_int (Obj.repr x.a));
     assert (Obj.is_int (Obj.repr y.a));
     assert (Obj.is_int (Obj.repr x.b)); (* <- this fails after a while 
*)
     assert (Obj.is_int (Obj.repr y.b));
     x = y

and one of these (always the same) triggers after a while (after some 
10.000 calls).
But only with the standard minor heap size, not with a 4 MB sized one.
There are no other functions working on these values; they are parsed, 
put through
the constructor function, compared and thrown away.

Regards
Markus

--
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 14:14   ` Markus Weißmann
@ 2016-04-29 14:25     ` Gerd Stolpmann
  2016-05-02  8:27       ` Sébastien Hinderer
  2016-04-29 14:57     ` Mark Shinwell
  1 sibling, 1 reply; 10+ messages in thread
From: Gerd Stolpmann @ 2016-04-29 14:25 UTC (permalink / raw)
  To: Markus Weißmann; +Cc: caml-list

[-- Attachment #1: Type: text/plain, Size: 2337 bytes --]

Am Freitag, den 29.04.2016, 16:14 +0200 schrieb Markus Weißmann:
> The value comes from C bindings, but from a string-value via Char.code.
> It is then passed through a constructor-function to create the record;
> I added a check there to see if the C bindings are to blame:

Well, there are other types of errors in C bindings that could also
cause this. Imagine what happens when the C bindings do not properly
handle pointers (e.g. do not declare them as local roots), and an
outdated pointer to an int is followed by the GC because of this.
Because the minor GC moves values to the major heap, this could cause
that the int is overwritten then.

In my experience, it's always the C binding!

Unfortunately, there's no code for investigations.

Gerd


> 
>    type foo = { a : int; b : int }
> 
>    let create (a : int) (b : int) =
>      assert (Obj.is_int (Obj.repr x)); (* always holds *)
>      { a; b }
> 
> This assertion never triggered so far.
> I replaced the equality check by a function which now also asserts the
> is_int property:
> 
>    let equal (x : foo) (y : foo) = (* y is a static value living through 
> the entire run; x is from a parse/allocate/compare/throw-away cycle *)
>      assert (Obj.is_int (Obj.repr x.a));
>      assert (Obj.is_int (Obj.repr y.a));
>      assert (Obj.is_int (Obj.repr x.b)); (* <- this fails after a while 
> *)
>      assert (Obj.is_int (Obj.repr y.b));
>      x = y
> 
> and one of these (always the same) triggers after a while (after some 
> 10.000 calls).
> But only with the standard minor heap size, not with a 4 MB sized one.
> There are no other functions working on these values; they are parsed, 
> put through
> the constructor function, compared and thrown away.
> 
> Regards
> Markus
> 
> --
> Markus Weißmann, M.Sc.
> Technische Universität München
> Institut für Informatik
> Boltzmannstr. 3
> D-85748 Garching
> Germany
> http://wwwknoll.in.tum.de/

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 14:14   ` Markus Weißmann
  2016-04-29 14:25     ` Gerd Stolpmann
@ 2016-04-29 14:57     ` Mark Shinwell
  2016-04-29 15:41       ` Markus Weißmann
  1 sibling, 1 reply; 10+ messages in thread
From: Mark Shinwell @ 2016-04-29 14:57 UTC (permalink / raw)
  To: Markus Weißmann; +Cc: caml-list, Gerd Stolpmann

It may be worth printing the pointer at the time of allocation of this
record, and then at the time just before the assertion fails.  I think
you can just Obj.magic the record to "int" (use printf and %d) and
then when you see the answer on the screen, multiply it by 2 to get
the correct pointer.  Or send it back to a C binding and printf it
from there.  Anyway, this might help to diagnose whether the value was
moved between the allocation and the failure; it seems likely it was.
If so it's probably a missing CAMLlocal or similar.

The thing about it being very sensitive to the heap size is
characteristic of that kind of bug.  You're effectively relying on a
particular allocation triggering a GC, so the heap has to be full at
just the right time.

Another technique that can be useful for diagnosing heap corruption is
gdb watchpoints on the part of the value concerned.

Mark

On 29 April 2016 at 15:14, Markus Weißmann <markus.weissmann@in.tum.de> wrote:
> On 2016-04-29 15:17, Gerd Stolpmann wrote:
>>
>> Am Freitag, den 29.04.2016, 13:04 +0200 schrieb Markus Weißmann:
>>>
>>> Hello,
>>>
>>> I have a server program that crashes after some time with a very
>>> strange error:
>>> The (=) comparison of two values returns false, even though they are
>>> pretty identical.
>>> They are of type { a : int; b : int } and the comparison always fails
>>> on the second integer.
>>> When printing the compared integers, they are always 0 (as expected) --
>>> both of them; but are not equal (=).
>>> I started inspecting the values with the "Obj.tag" and found them to be
>>> always of type Obj.int_tag -- until the non-equalness strikes:
>>> One of the compared integers then always has Obj.out_of_heap_tag. This
>>> value surprisingly behaved like an integer unless compared to another:
>>>
>>> let (x : int) =
>>>    print_int x; (* "0" *)
>>>    assert (x = 0) (* fails! *)
>>>
>>> Can someone explain what this tag means exactly and if this
>>> works-as-intended or if my heap must have gotten hit by some faulty C
>>> bindings?
>>
>>
>> Obj.tag is meaningless for ints.
>>
>> What could have happened is that a C lib did not set the LSB of the word
>> (which is required for ints in order to make them distinguishable from
>> pointers). The C lib MUST use Val_int or Val_long to create the values
>> (and these macros set the LSB).
>>
>> Check whether Obj.is_int returns true. If not, something is wrong.
>>
>
> The value comes from C bindings, but from a string-value via Char.code.
> It is then passed through a constructor-function to create the record;
> I added a check there to see if the C bindings are to blame:
>
>   type foo = { a : int; b : int }
>
>   let create (a : int) (b : int) =
>     assert (Obj.is_int (Obj.repr x)); (* always holds *)
>     { a; b }
>
> This assertion never triggered so far.
> I replaced the equality check by a function which now also asserts the
> is_int property:
>
>   let equal (x : foo) (y : foo) = (* y is a static value living through the
> entire run; x is from a parse/allocate/compare/throw-away cycle *)
>     assert (Obj.is_int (Obj.repr x.a));
>     assert (Obj.is_int (Obj.repr y.a));
>     assert (Obj.is_int (Obj.repr x.b)); (* <- this fails after a while *)
>     assert (Obj.is_int (Obj.repr y.b));
>     x = y
>
> and one of these (always the same) triggers after a while (after some 10.000
> calls).
> But only with the standard minor heap size, not with a 4 MB sized one.
> There are no other functions working on these values; they are parsed, put
> through
> the constructor function, compared and thrown away.
>
> Regards
> Markus
>
> --
> Markus Weißmann, M.Sc.
> Technische Universität München
> Institut für Informatik
> Boltzmannstr. 3
> D-85748 Garching
> Germany
> http://wwwknoll.in.tum.de/
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 14:57     ` Mark Shinwell
@ 2016-04-29 15:41       ` Markus Weißmann
  2016-04-29 16:41         ` Adrien Nader
  0 siblings, 1 reply; 10+ messages in thread
From: Markus Weißmann @ 2016-04-29 15:41 UTC (permalink / raw)
  To: caml-list; +Cc: Gerd Stolpmann, Mark Shinwell

Thanks a lot Gerd and Mark: It was in the C code: A missing 
CAMLlocal(). =)

The funny thing was: It had _nothing_ to do with the piece of code the 
bug surfaced around.
So for anyone reading this thread in the future, tearing your hair out 
in frustration:
Check your C code.

I hereby confirm the Stolpmann-Theorem: "Its always the C code."

regards
Markus

On 2016-04-29 16:57, Mark Shinwell wrote:
> It may be worth printing the pointer at the time of allocation of 
> this
> record, and then at the time just before the assertion fails.  I 
> think
> you can just Obj.magic the record to "int" (use printf and %d) and
> then when you see the answer on the screen, multiply it by 2 to get
> the correct pointer.  Or send it back to a C binding and printf it
> from there.  Anyway, this might help to diagnose whether the value 
> was
> moved between the allocation and the failure; it seems likely it was.
> If so it's probably a missing CAMLlocal or similar.
>
> The thing about it being very sensitive to the heap size is
> characteristic of that kind of bug.  You're effectively relying on a
> particular allocation triggering a GC, so the heap has to be full at
> just the right time.
>
> Another technique that can be useful for diagnosing heap corruption 
> is
> gdb watchpoints on the part of the value concerned.
>
> Mark
>
> On 29 April 2016 at 15:14, Markus Weißmann 
> <markus.weissmann@in.tum.de> wrote:
>> On 2016-04-29 15:17, Gerd Stolpmann wrote:
>>>
>>> Am Freitag, den 29.04.2016, 13:04 +0200 schrieb Markus Weißmann:
>>>>
>>>> Hello,
>>>>
>>>> I have a server program that crashes after some time with a very
>>>> strange error:
>>>> The (=) comparison of two values returns false, even though they 
>>>> are
>>>> pretty identical.
>>>> They are of type { a : int; b : int } and the comparison always 
>>>> fails
>>>> on the second integer.
>>>> When printing the compared integers, they are always 0 (as 
>>>> expected) --
>>>> both of them; but are not equal (=).
>>>> I started inspecting the values with the "Obj.tag" and found them 
>>>> to be
>>>> always of type Obj.int_tag -- until the non-equalness strikes:
>>>> One of the compared integers then always has Obj.out_of_heap_tag. 
>>>> This
>>>> value surprisingly behaved like an integer unless compared to 
>>>> another:
>>>>
>>>> let (x : int) =
>>>>    print_int x; (* "0" *)
>>>>    assert (x = 0) (* fails! *)
>>>>
>>>> Can someone explain what this tag means exactly and if this
>>>> works-as-intended or if my heap must have gotten hit by some 
>>>> faulty C
>>>> bindings?
>>>
>>>
>>> Obj.tag is meaningless for ints.
>>>
>>> What could have happened is that a C lib did not set the LSB of the 
>>> word
>>> (which is required for ints in order to make them distinguishable 
>>> from
>>> pointers). The C lib MUST use Val_int or Val_long to create the 
>>> values
>>> (and these macros set the LSB).
>>>
>>> Check whether Obj.is_int returns true. If not, something is wrong.
>>>
>>
>> The value comes from C bindings, but from a string-value via 
>> Char.code.
>> It is then passed through a constructor-function to create the 
>> record;
>> I added a check there to see if the C bindings are to blame:
>>
>>   type foo = { a : int; b : int }
>>
>>   let create (a : int) (b : int) =
>>     assert (Obj.is_int (Obj.repr x)); (* always holds *)
>>     { a; b }
>>
>> This assertion never triggered so far.
>> I replaced the equality check by a function which now also asserts 
>> the
>> is_int property:
>>
>>   let equal (x : foo) (y : foo) = (* y is a static value living 
>> through the
>> entire run; x is from a parse/allocate/compare/throw-away cycle *)
>>     assert (Obj.is_int (Obj.repr x.a));
>>     assert (Obj.is_int (Obj.repr y.a));
>>     assert (Obj.is_int (Obj.repr x.b)); (* <- this fails after a 
>> while *)
>>     assert (Obj.is_int (Obj.repr y.b));
>>     x = y
>>
>> and one of these (always the same) triggers after a while (after 
>> some 10.000
>> calls).
>> But only with the standard minor heap size, not with a 4 MB sized 
>> one.
>> There are no other functions working on these values; they are 
>> parsed, put
>> through
>> the constructor function, compared and thrown away.
>>
>> Regards
>> Markus
>>
>> --
>> Markus Weißmann, M.Sc.
>> Technische Universität München
>> Institut für Informatik
>> Boltzmannstr. 3
>> D-85748 Garching
>> Germany
>> http://wwwknoll.in.tum.de/
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 15:41       ` Markus Weißmann
@ 2016-04-29 16:41         ` Adrien Nader
  0 siblings, 0 replies; 10+ messages in thread
From: Adrien Nader @ 2016-04-29 16:41 UTC (permalink / raw)
  To: Markus Weißmann; +Cc: caml-list, Gerd Stolpmann, Mark Shinwell

On Fri, Apr 29, 2016, Markus Weißmann wrote:
> Thanks a lot Gerd and Mark: It was in the C code: A missing
> CAMLlocal(). =)
> 
> The funny thing was: It had _nothing_ to do with the piece of code
> the bug surfaced around.

This is why calling Gc.collect can help trigger such issues: it can act
as a checker for the ocaml memory.

> So for anyone reading this thread in the future, tearing your hair
> out in frustration:
> Check your C code.
> 
> I hereby confirm the Stolpmann-Theorem: "Its always the C code."

Well, not always. The runtime is very good but not perfect. Still the
most likely culprit however.

-- 
Adrien Nader

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-04-29 14:25     ` Gerd Stolpmann
@ 2016-05-02  8:27       ` Sébastien Hinderer
  2016-05-02 14:30         ` Gabriel Scherer
  0 siblings, 1 reply; 10+ messages in thread
From: Sébastien Hinderer @ 2016-05-02  8:27 UTC (permalink / raw)
  To: caml-list

Hi,

Gerd Stolpmann (2016/04/29 16:25 +0200):
> Am Freitag, den 29.04.2016, 16:14 +0200 schrieb Markus Weißmann:
> > The value comes from C bindings, but from a string-value via Char.code.
> > It is then passed through a constructor-function to create the record;
> > I added a check there to see if the C bindings are to blame:
> 
> Well, there are other types of errors in C bindings that could also
> cause this. Imagine what happens when the C bindings do not properly
> handle pointers (e.g. do not declare them as local roots), and an
> outdated pointer to an int is followed by the GC because of this.
> Because the minor GC moves values to the major heap, this could cause
> that the int is overwritten then.
> 
> In my experience, it's always the C binding!
> 
> Unfortunately, there's no code for investigations.

Do you think there is room for improvement at this level?

Do you already have a bit more precise ideas about the kind of tools that
coould be helpful?

Cheers,

Sébastien.

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-05-02  8:27       ` Sébastien Hinderer
@ 2016-05-02 14:30         ` Gabriel Scherer
  2016-05-03 15:59           ` Boris Yakobowski
  0 siblings, 1 reply; 10+ messages in thread
From: Gabriel Scherer @ 2016-05-02 14:30 UTC (permalink / raw)
  To: Sébastien Hinderer, caml users

In 2006 there was work on a static analysis tool to check OCaml C
stubs called "Saffire", which you can read about in detail here:
  http://www.cs.umd.edu/~jfoster/papers/cs-tr-4845.html

Adrien Nader extracted the implementation and loaded it on the OCaml
Forge in 2012, anyone interested in fixing/updating the project should
probably get in touch with him:
  https://forge.ocamlcore.org/projects/saffire/

I have always been curious about how it would fare on the C bindings
in the wild -- my guess is that it may have bitrotten a bit but that
it would find a few issues, and also be very helpful during the
development phase (where you iteratively hunt for segfaults), if it
was an "opam install" away and easy to run.

I have been trying to motivate the Frama-C people to find an excellent
intern to write a specification of the OCaml memory model in ACSL
(their specification language for C, http://frama-c.com/acsl.html );
the dream is that one may then be able to use Frama-C to check for
safety of the C stubs, and even possibly verify some parts of the C
codebase in the compiler distribution (probably not the runtime
implementation itself, which precisely breaks the abstraction of the
memory model, but at least large parts of C implementation of
primitives, otherlibs/, etc.). I think they are interested as well,
but I'm not sure they have found the time and people to work on this.

Finally, note that Jeremy Yallop's Ctypes (
https://github.com/ocamllabs/ocaml-ctypes ) may be the better solution
to write correct C bindings. I think that it is complementary with the
above-mentioned efforts:
- Saffire could be used to check legacy C stubs, of which there are many
- A more precise model of the OCaml value representation and exposed
runtime interface could help verify Ctypes itself and other future
projects interacting with the runtime at a lower level.

Ctypes is slightly more restricted than general C stubs, but
substantially more safe (and more convenient). In my experience the
unsafety of C bindings is a huge time sink, so starting with a Ctypes
binding is almost certainly the most productive choice.

On Mon, May 2, 2016 at 4:27 AM, Sébastien Hinderer
<Sebastien.Hinderer@inria.fr> wrote:
> Hi,
>
> Gerd Stolpmann (2016/04/29 16:25 +0200):
>> Am Freitag, den 29.04.2016, 16:14 +0200 schrieb Markus Weißmann:
>> > The value comes from C bindings, but from a string-value via Char.code.
>> > It is then passed through a constructor-function to create the record;
>> > I added a check there to see if the C bindings are to blame:
>>
>> Well, there are other types of errors in C bindings that could also
>> cause this. Imagine what happens when the C bindings do not properly
>> handle pointers (e.g. do not declare them as local roots), and an
>> outdated pointer to an int is followed by the GC because of this.
>> Because the minor GC moves values to the major heap, this could cause
>> that the int is overwritten then.
>>
>> In my experience, it's always the C binding!
>>
>> Unfortunately, there's no code for investigations.
>
> Do you think there is room for improvement at this level?
>
> Do you already have a bit more precise ideas about the kind of tools that
> coould be helpful?
>
> Cheers,
>
> Sébastien.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

^ permalink raw reply	[flat|nested] 10+ messages in thread

* Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption?
  2016-05-02 14:30         ` Gabriel Scherer
@ 2016-05-03 15:59           ` Boris Yakobowski
  0 siblings, 0 replies; 10+ messages in thread
From: Boris Yakobowski @ 2016-05-03 15:59 UTC (permalink / raw)
  To: Gabriel Scherer; +Cc: Sébastien Hinderer, caml users

[-- Attachment #1: Type: text/plain, Size: 1172 bytes --]

On Mon, May 2, 2016 at 4:30 PM, Gabriel Scherer <gabriel.scherer@gmail.com>
wrote:

> I have been trying to motivate the Frama-C people to find an excellent
> intern to write a specification of the OCaml memory model in ACSL
> (their specification language for C, http://frama-c.com/acsl.html );
> the dream is that one may then be able to use Frama-C to check for
> safety of the C stubs, and even possibly verify some parts of the C
> codebase in the compiler distribution (probably not the runtime
> implementation itself, which precisely breaks the abstraction of the
> memory model, but at least large parts of C implementation of
> primitives, otherlibs/, etc.). I think they are interested as well,
> but I'm not sure they have found the time and people to work on this.
>
>
We're still very much interested in this, although I think the challenges
are more important than what you expect. The duality pointer/integer in
OCaml's runtime is a major pitfall. Triaging between both by looking at the
least significant bit won't be easy to handle.

In any case, if somebody looking for an internship is interested by this
topic, you're more than welcome to contact me!

[-- Attachment #2: Type: text/html, Size: 1657 bytes --]

^ permalink raw reply	[flat|nested] 10+ messages in thread

end of thread, other threads:[~2016-05-03 15:59 UTC | newest]

Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-04-29 11:04 [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption? Markus Weißmann
2016-04-29 13:17 ` Gerd Stolpmann
2016-04-29 14:14   ` Markus Weißmann
2016-04-29 14:25     ` Gerd Stolpmann
2016-05-02  8:27       ` Sébastien Hinderer
2016-05-02 14:30         ` Gabriel Scherer
2016-05-03 15:59           ` Boris Yakobowski
2016-04-29 14:57     ` Mark Shinwell
2016-04-29 15:41       ` Markus Weißmann
2016-04-29 16:41         ` Adrien Nader

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).