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
