[Caml-list] Ephemerons: is this behavior correct ?

[Caml-list] Ephemerons: is this behavior correct ?

[Bertrand Jeannet]

Dear list,

The following piece of code raises an assert false exception (in rare 
cases) with official version 4.03.0:

match Ephemeron.K1.get_data c with
| Some _ ->
   match Ephemeron.K1.get_key c with
   | Some _ -> (* ... *)
   | None -> assert false (* reachable *)

Before I had called the function K1.set_key_data with a key
* that belongs to a weak hashed set
* and that is used after the call
(this may be important or not).

The documentation of the Ephemeron module says:
"When one of the keys is not considered alive anymore by the GC, the 
data is emptied from the ephemeron"

I was expecting this to happen atomically from the programmer point of 
view, but here apparently the key was emptied but the data kept (at 
least temporarily).

Was this behavior anticipated ?

IMHO, synchronized deletion is simpler and safer (in previous versions, 
I encountered the now-solved-bug that the deletion of several weak 
pointers to the same object was not synchronized).

Btw, the Ephemeron module does not appear on this url:
http://caml.inria.fr/pub/docs/manual-ocaml/stdlib.html
one has to go to
http://caml.inria.fr/pub/docs/manual-ocaml/libref/index.html

Best regards

Re: [Caml-list] Ephemerons: is this behavior correct ?

[François Bobot]

Hi Bertrand,

On 10/10/2016 15:14, Bertrand Jeannet wrote:
> The following piece of code raises an assert false exception (in rare
> cases) with official version 4.03.0:
>
> match Ephemeron.K1.get_data c with
> | Some _ ->
>    match Ephemeron.K1.get_key c with
>    | Some _ -> (* ... *)
>    | None -> assert false (* reachable *)
 >
> The documentation of the Ephemeron module says:
> "When one of the keys is not considered alive anymore by the GC, the
> data is emptied from the ephemeron"
>
> I was expecting this to happen atomically from the programmer point of
> view,
Yes, atomicity is the intent.

> but here apparently the key was emptied but the data kept (at
> least temporarily).

I don't deduce that from the example. The cleaning can be done atomically between the return of 
get_data and the return of get_key (indeed get_key does an allocation). An example that would show 
non-atomicity would be:

 > match Ephemeron.K1.get_data c with
 > | None ->
 >    match Ephemeron.K1.get_key c with
 >    | Some _ -> assert false (* non atomic! *)
 >    | None -> ...
 >

or

 > match Ephemeron.K1.get_key c with
 > | None ->
 >    match Ephemeron.K1.get_data c with
 >    | Some _ -> assert false (* non atomic! *)
 >    | None -> ...
 >


>
> Was this behavior anticipated ?

Yes.

>
> IMHO, synchronized deletion is simpler and safer (in previous versions,
> I encountered the now-solved-bug that the deletion of several weak
> pointers to the same object was not synchronized).

Indeed I think it is a better behavior. I'm happy it solved your previous problems.

>
> Btw, the Ephemeron module does not appear on this url:
> http://caml.inria.fr/pub/docs/manual-ocaml/stdlib.html
> one has to go to
> http://caml.inria.fr/pub/docs/manual-ocaml/libref/index.html

I though that GPR#564[1] merged in 4.03 took care of this bug, so I don't understand.


Best,


[1]: https://github.com/ocaml/ocaml/pull/564

-- 
François

Re: [Caml-list] Ephemerons: is this behavior correct ?

[Bertrand Jeannet]

Le 10/10/2016 15:38, François Bobot a écrit :
> Hi Bertrand,
>
> On 10/10/2016 15:14, Bertrand Jeannet wrote:
>> The following piece of code raises an assert false exception (in rare
>> cases) with official version 4.03.0:
>>
>> match Ephemeron.K1.get_data c with
>> | Some _ ->
>>    match Ephemeron.K1.get_key c with
>>    | Some _ -> (* ... *)
>>    | None -> assert false (* reachable *)
>  >
>> The documentation of the Ephemeron module says:
>> "When one of the keys is not considered alive anymore by the GC, the
>> data is emptied from the ephemeron"
>>
>> I was expecting this to happen atomically from the programmer point of
>> view,
> Yes, atomicity is the intent.
>
>> but here apparently the key was emptied but the data kept (at
>> least temporarily).
>
> I don't deduce that from the example. The cleaning can be done
> atomically between the return of get_data and the return of get_key
> (indeed get_key does an allocation).

Hi Francois,

Thank you for the explanation. I missed the point that a reachable data 
value does not prevent the key and the data fields to be emptied (it is 
explicitly mentioned in the documentation).

Best regards
Bertrand