[Caml-list] Weak array semantics with mutually recursive values.

[Caml-list] Weak array semantics with mutually recursive values.

[Christophe Raffalli]

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


Hello,

Consider two mutually recursive values:

let rec x = (1,y) and y = (2,x)

for instance. They will become unreachable by the GC at the same cycle.
However,
if they are both added in a weak array, it seems that they may not be
removed at the same time from the array.

I have some code that seems to show that most of the time they are
removed at the same times, but very rarely this fails.

The description in weak.mli does not imply this, because it just says
"may be removed" and not "must be removed".

What do you think about this ?

Regards,
Christophe




[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 259 bytes --]

Re: [Caml-list] Weak array semantics with mutually recursive values.

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 1645 bytes --]

Le 22/01/11 18:56, Andrew a écrit :
>> let rec x = (1,y) and y = (2,x)

This was just a silly example, but -rectypes works in that case.

My real example is a type for hashconsed propositional formula
each formula pointing to its negation like this (ignoring hashconsing):

this is untested ...

type form =
Lit(bool * string*form)
| Conj(form*form*form)
| Disj(form*form*form)

let mkNot = function
  Lit(_,_,f) | Conj(_,_,f) | Disj(_,_,f) -> f

let mkLit v =
  let rec v1 = Lit(true,v,v2) and v2 = Lit(false,v,v1) in v1

let mkConj f1 f2 =
  let rec v1 = Conj(f1,f2,v2) and v2 = Disj(mkNot f1, mkNot f2, v1) in v1

So the real question is what is the best way to hashcons this ?

> Might be naïve curiosity, but how do you manage to build this? What's the
> type of x and y?
>
> My Ocaml toplevel returns 
>     # let rec x = (1,y) and y = (2,x);;
>     Characters 26-31:
>       let rec x = (1,y) and y = (2,x);;
>                                 ^^^^^
>     Error: This expression has type int * (int * (int * 'a))
>            but is here used with type int * 'a
>
> Andrew.
>
>


-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #1.2: Christophe_Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 250 bytes --]

Re: [Caml-list] Weak array semantics with mutually recursive values.

[Damien Doligez]

On 2011-01-22, at 17:29, Christophe Raffalli wrote:

> for instance. They will become unreachable by the GC at the same cycle.
> However,
> if they are both added in a weak array, it seems that they may not be
> removed at the same time from the array.
> 
> I have some code that seems to show that most of the time they are
> removed at the same times, but very rarely this fails.

As far as I can tell, it should never happen.  Do you have a good
repro case?

-- Damien

Re: [Caml-list] Weak array semantics with mutually recursive values.

[Christophe Raffalli]

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

Le 24/01/11 13:45, Damien Doligez a écrit :
> On 2011-01-22, at 17:29, Christophe Raffalli wrote:
>
>> for instance. They will become unreachable by the GC at the same cycle.
>> However,
>> if they are both added in a weak array, it seems that they may not be
>> removed at the same time from the array.
>>
>> I have some code that seems to show that most of the time they are
>> removed at the same times, but very rarely this fails.
> As far as I can tell, it should never happen.  Do you have a good
> repro case?
Hello,

I will try to investigate further my example to make sure it is not
another problem. If I get
a simple repro case, I will post it.

What I was considering recently (after my second post) is the following
scenario:

t and u are two inaccessible mutually recursive values, but one is still
in the minor heap (t) while the other (u) has been promoted (if a minor
cycle just ended between the allocation of both values, this seems
possible even if unlikely). In this case, the finalisation of t and its
removal from a weak array might occur long before the finalisation of u ?

Cheers,
Christophe



[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 259 bytes --]

Re: [Caml-list] Weak array semantics with mutually recursive values.

[Damien Doligez]

On 2011-01-24, at 22:41, Christophe Raffalli wrote:

> t and u are two inaccessible mutually recursive values, but one is still
> in the minor heap (t) while the other (u) has been promoted (if a minor
> cycle just ended between the allocation of both values, this seems
> possible even if unlikely). In this case, the finalisation of t and its
> removal from a weak array might occur long before the finalisation of u ?


That's correct.

-- Damien