Brian,
The intention of PolyML.pointerEq is that if pointerEq(x, y) is true then x = y will be true, assuming the type of x and y admits equality. It is really intended for use where a user function wants to test for equality in some general sense and knowing that actually the values are the same pointer can short circuit the process.

Poly/ML only guarantees to maintain the ML equality property i.e. pointer equality for mutable values (refs and arrays) and value equality for immutable data. For example, the compiler may optimise tuple creation so it is quite likely that what may appear to be a single value with a clear point of creation is actually optimised away or results in more than one piece of memory being allocated.

The present garbage collector has two different operations that may affect pointer equality. The minor collector copies cells out of the allocation area. For mutable data it uses an atomic test-and-set that guarantees that if two different GC threads copy the cell only one copy will be made. This is not used for immutable data to reduce the need for bus locking and so there is a finite chance that a cell will be duplicated. Also the major collection can activate a sharing pass that merges cells with the same contents resulting in pointer equality being true where it previously wasn't.

The only safe way to maintain identity of cells is to use a counter or a ref. An alternative to a ref is to use a locally generated exception and this may be more efficient than a ref. As a work-around to avoid the problem with duplication in the multi-threaded collector you could force it to be single-threaded with --gcthreads=1.

David

On 29/01/2014 15:51, Brian Campbell wrote:
What semantics, if any, does PolyML.pointerEq have?  In particular, is
it supposed to be guaranteed that if pointerEq (x,y) is true, then it
will remain true after GC?

My reason for asking is that I've been having trouble with assertion
failures in HOL when reducing large terms.  The assertions check that
the left hand side of the conclusions of two theorem objects are equal
according to pointerEq, because this allows a fast comparison that
"should" always be true if the theorem is manipulated carefully.

I'm fairly certain the assertion failures are related to GC:  they are
non-deterministic on code that ought to be deterministic, and vary in
frequency across different machines.  (I haven't seen it at all on a 4GB
32-bit machine, rarely on 4GB 64-bit, often on the 8GB I normally use
and infrequently on a compute server with much more.)  There's no sign
of any data corruption, however.

   Brian
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Reply via email to