On Tue, 25 Mar 2014, Makarius wrote:
* pointer_eq is not part of SML and requires extra reasoning that it is
correct whenever it is used (normally in certain hot-spots of kernel
operations). See also the surprise caused by some optimizations of
the Poly/ML runtime system concerning object identity, which are
perfectly inside the Standard ML semantics:
http://lists.inf.ed.ac.uk/pipermail/polyml/2014-January/001389.html
Concerning the last point, I did not inspect the actual situation outside of
Isabelle/Pure yet. It probably requires further looking, and more
explanations on either of the mailing lists.
This is still pending, and relevant for the release.
SML semantics works with structural mathematical equality of values.
Pointer equality is provided in the common implementation as a concession
to physical hacking, in order to *peek* at the accidental situation in the
run-time system. According to the SML semantics, the memory menagement is
allowed to:
(1) introduce pointer equality that was not there before, e.g. via
sharing of structurally equal values;
(2) eliminate pointer equality that was there before, e.g. due to
optimizations in lock-free garbage collection on multiple cores.
Both happens in Poly/ML, (1) very often, (2) very rarely.
This means, the ancient programming technique to use pointer_eq to see if
the ML user code has "touched" some value no longer works: the ML run-time
system might have touched it instead.
This means, special care is required to use pointer_eq at all, and it is
often better to avoid it before spending too much time thinking about its
correctness.
Here are some observations on the use of pointer_eq in
Isabelle/dc542b78ef0f (apart from the traditional special tricks in Pure):
* src/HOL/Tools/Lifting/lifting_info.ML
One occurence in theory data managed: some canonical idioms to
merge/join tables. It looks formally OK, but I did not check it
semantically.
* src/HOL/Tools/ATP/atp_problem_generate.ML
Two occurrences that are not immediately clear. Looks like plain
structural equality could do the job.
* src/HOL/Tools/BNF/bnf_def.ML
fun maybe_restore lthy_old lthy =
lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
This looks odd. The normal idiom is to maintain an option value, to
say when a value remains explicitly unchanged (NONE). If this is too
awkward here, one could try comparing the background theories via
Theory.eq_thy instead (which is strictly speaking just another
approximation, but a deterministic one). One could also try to
express the idea behind the uses of maybe_restore differently.
* Metis has various optimizations using the "portable" alias
pointerEqual. Hard to say if there are potential problems coming from
it. A quick experiment with an always false predicate (which is a
correct approximation) makes metis very slow, but in most situations
it still terminates. (Shall we forward this to Joe Hurd? For the
Isabelle release, Metis is better left alone, though.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
